English
The relation Agree between x.approx n and y.approx (n+1) is equivalent to Agree' n x y.
Русский
Отношение Agree между x.approx n и y.approx (n+1) эквивалентно Agree' n x y.
LaTeX
$$$\\operatorname{Agree} (x.approx\\ n) (y.approx\\ (n+1)) \\;\\iff\\; \\operatorname{Agree'} n x y$$$
Lean4
theorem agree_iff_agree' {n : ℕ} (x y : M F) : Agree (x.approx n) (y.approx <| n + 1) ↔ Agree' n x y :=
by
constructor <;> intro h
·
induction n generalizing x y with
| zero => constructor
| succ _ n_ih =>
induction x using PFunctor.M.casesOn'
induction y using PFunctor.M.casesOn'
simp only [approx_mk] at h
obtain - | ⟨_, _, hagree⟩ := h
constructor <;> try rfl
intro i
apply n_ih
apply hagree
·
induction n generalizing x y with
| zero => constructor
| succ _ n_ih =>
obtain - | @⟨_, a, x', y'⟩ := h
induction x using PFunctor.M.casesOn' with
| _ x_a x_f
induction y using PFunctor.M.casesOn' with
| _ y_a y_f
simp only [approx_mk]
have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
cases h_a_1
replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
cases h_a_2
constructor
intro i
apply n_ih
simp [*]
