α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none
dsimp [assert, none]
case h.e_2
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False

case h.e_3
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom)) fun t => False.rec (fun x => α) t
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ h, (f h).Dom, get := fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom) } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }
congr
no goals
case h.e_2
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
simp only [h, not_false_iff, exists_prop_of_false]
case h.e_3.hα
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False

case h.e_3.h
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : False),
    HEq a a' → HEq (get (f (_ : p)) (_ : (f (_ : p)).Dom)) (False.rec (fun x => α) a')
case h.e_3
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => get (f (_ : p)) (_ : (f (_ : p)).Dom)) fun t => False.rec (fun x => α) t
apply Function.hfunext
no goals
case h.e_3.h
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ h, (f h).Dom) (a' : False),
    HEq a a' → HEq (get (f (_ : p)) (_ : (f (_ : p)).Dom)) (False.rec (fun x => α) a')
simp at *
no goals
case h.e_3.hα
α : Type u_1
β : Type ?u.17198
γ : Type ?u.17201
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ h, (f h).Dom) = False
simp only [h, not_false_iff, exists_prop_of_false]