case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { toInhabited := { default := x }, uniq := h } = { toInhabited := { default := y }, uniq := uniq✝ }
congr
no goals
case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
rw [h x, h y]