English
A second presentation of ext_aux same as item 105511, giving an equality of approximations under coherent hypotheses.
Русский
Вторая формулировка ext_aux; повторяет условия и выводит то же равенство аппроксимаций при согласованных гипотезах.
LaTeX
$$$\\operatorname{ext\\_aux} [Inhabited (M F)] [DecidableEq F.A] {n : \\mathbb{N}} (x y z : M F) (hx : Agree' n z x) (hy : Agree' n z y) (hrec : \\forall ps : Path F, n = ps.length → iselect ps x = iselect ps y) : x.approx (n + 1) = y.approx (n + 1)$$$
Lean4
theorem ext_aux [Inhabited (M F)] [DecidableEq F.A] {n : ℕ} (x y z : M F) (hx : Agree' n z x) (hy : Agree' n z y)
(hrec : ∀ ps : Path F, n = ps.length → iselect ps x = iselect ps y) : x.approx (n + 1) = y.approx (n + 1) := by
induction n generalizing x y z with
| zero =>
specialize hrec [] rfl
induction x using PFunctor.M.casesOn'
induction y using PFunctor.M.casesOn'
simp only [iselect_nil] at hrec
subst hrec
simp only [approx_mk, heq_iff_eq, CofixA.intro.injEq, eq_iff_true_of_subsingleton, and_self]
| succ n n_ih =>
cases hx
cases hy
induction x using PFunctor.M.casesOn'
induction y using PFunctor.M.casesOn'
subst z
iterate 3 (have := mk_inj ‹_›; cases this)
rename_i n_ih a f₃ f₂ hAgree₂ _ _ h₂ _ _ f₁ h₁ hAgree₁ clr
simp only [approx_mk]
have := mk_inj h₁
cases this; clear h₁
have := mk_inj h₂
cases this; clear h₂
congr
ext i
apply n_ih
· solve_by_elim
· solve_by_elim
introv h
specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
simp only [iselect_cons] at hrec
exact hrec
