lean4#1829

Stream: lean4

[Scott Morrison]

We encountered a strange issue (reported as lean4#1829) in mathlib4:

theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
  ⟨fun _ => ⟨⟩, fun _ => (Subsingleton.elim ..)⟩

/- comment out following `attribute [simp]` to make the example below work -/
attribute [simp] eq_iff_true_of_subsingleton in
example : True := trivial

structure Func' (α : Sort _) (β : Sort _) :=
(toFun    : α → β)

def r : Func' α α := ⟨id⟩

@[simp] theorem r_toFun {α : Sort u_1} (a : α) : Func'.toFun r a = id a := rfl

example (x y : α) (h : x = y) : r.toFun x = y := by simp <;> rw [h]
/-
in the presence of `attribute [simp] eq_iff_true_of_subsingleton in`, one gets

application type mismatch
  Eq
argument has type
  Sort u_1
but function has type
  {α : Prop} → α → α → Prop
-/

-- If we change `example` to `theorem`, it doesn't care about the `attribute [simp]`.
theorem noissue (x y : α) (h : x = y) : r.toFun x = y := by simp <;> rw [h]

If anyone knows whats going on here, that would be great. This is holding up an important file in the mathlib4 port.

[Leonardo de Moura]

It has been fixed.