English
Given a Prop p and a function f : p → Part α, Part.assert p f equals f h for any proof h of p.
Русский
Для данного утверждения p и функции f : p → Part α, Part.assert p f равно f h для любого доказательства h p.
LaTeX
$$$ \forall {p} {f : p \rightarrow \mathrm{Part}(\alpha)} (h : p), \mathrm{Part.assert}(p,f) = f(h)$$$
Lean4
theorem assert_pos {p : Prop} {f : p → Part α} (h : p) : assert p f = f h :=
by
dsimp [assert]
cases h' : f h
simp only [h', mk.injEq, h, exists_prop_of_true, true_and]
apply Function.hfunext
· simp only [h, h', exists_prop_of_true]
· simp