no goals
α : Type u_1
β : Type ?u.6173
γ : Type ?u.6176
a : Part α
ha : a.Dom
b : α
h : get a ha = b
⊢ a = some b
simp [h.symm]
no goals
α : Type u_1
β : Type ?u.6173
γ : Type ?u.6176
a : Part α
ha : a.Dom
b : α
h : a = some b
⊢ get a ha = b
simp [h]