α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = f h
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h
dsimp [assert]
case mk
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = { Dom := Dom✝, get := get✝ }
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = f h
cases h' : f h
case mk
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) get✝
case mk
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } = { Dom := Dom✝, get := get✝ }
simp [h', mk.injEq, h, exists_prop_of_true, true_and]
case mk.hα
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ h, (f h).Dom) = Dom✝

case mk.h
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) (get✝ a')
case mk
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) get✝
apply Function.hfunext
no goals
case mk.hα
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ h, (f h).Dom) = Dom✝
simp only [h, h', exists_prop_of_true]
no goals
case mk.h
α : Type u_1
β : Type ?u.15915
γ : Type ?u.15918
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ (_ : { Dom := Dom✝, get := get✝ }.Dom)) (get✝ a')
aesop