English
If a certain path ps is not an actual path for x, then iselect ps x equals head default (under decidable equality).
Русский
Если ps не является действительным путем для x, то iselect ps x равно head default (при конечном равенстве).
LaTeX
$$$\\textit{iselect\_eq\_default} [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) (x : M F) (h : \\neg IsPath ps x) : \\ iselect ps x = head default$$$
Lean4
theorem iselect_eq_default [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) (x : M F) (h : ¬IsPath ps x) :
iselect ps x = head default := by
induction ps generalizing x with
| nil =>
exfalso
apply h
constructor
| cons ps_hd ps_tail ps_ih =>
obtain ⟨a, i⟩ := ps_hd
induction x using PFunctor.M.casesOn' with
| _ x_a x_f
simp only [iselect, isubtree] at ps_ih ⊢
by_cases h'' : a = x_a
· subst x_a
simp only [dif_pos, casesOn_mk']
rw [ps_ih]
intro h'
apply h
constructor <;> try rfl
apply h'
· simp [*]
