-- Mathlib/Data/PFunctor/Univariate/M.lean
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)

Proof state:
case succ.step.step.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
z : F.M
a✝⁹ : F.A
x✝¹ y✝¹ : F.B a✝⁹ → F.M
a✝⁸ : ∀ (i : F.B a✝⁹), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁷ : z = M.mk ⟨a✝⁹, x✝¹⟩
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : z = M.mk ⟨a✝⁶, x✝⟩
a✝³ : F.A
f✝¹ : F.B a✝³ → F.M
a✝² : M.mk ⟨a✝³, f✝¹⟩ = M.mk ⟨a✝⁹, y✝¹⟩
a✝¹ : F.A
f✝ : F.B a✝¹ → F.M
a✝ : M.mk ⟨a✝¹, f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝³, f✝¹⟩) = iselect ps (M.mk ⟨a✝¹, f✝⟩)
⊢ (M.mk ⟨a✝³, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝¹, f✝⟩).approx (n + 1 + 1)

Tactic:
subst z

Result:
case succ.step.step.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : F.B a✝⁸ → F.M
a✝⁷ : ∀ (i : F.B a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : F.B a✝⁶ → F.M
a✝⁵ : ∀ (i : F.B a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : F.B a✝⁴ → F.M
a✝³ : M.mk ⟨a✝⁴, f✝¹⟩ = M.mk ⟨a✝⁸, y✝¹⟩
a✝² : F.A
f✝ : F.B a✝² → F.M
a✝¹ : M.mk ⟨a✝², f✝⟩ = M.mk ⟨a✝⁶, y✝⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁴, f✝¹⟩) = iselect ps (M.mk ⟨a✝², f✝⟩)
a✝ : M.mk ⟨a✝⁸, x✝¹⟩ = M.mk ⟨a✝⁶, x✝⟩
⊢ (M.mk ⟨a✝⁴, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝², f✝⟩).approx (n + 1 + 1)

Proof state:
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
⊢ (f₂ i).approx (n + 1) = (f₁ i).approx (n + 1)

Tactic:
apply n_ih

Result:
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hx
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
⊢ Agree' n ?succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.z (f₂ i)

case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hy
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
⊢ Agree' n ?succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.z (f₁ i)

case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
⊢ ∀ (ps : Path F), n = length ps → iselect ps (f₂ i) = iselect ps (f₁ i)

case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.z
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
i : F.B a
⊢ F.M

Proof state:
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
h₂ : M.mk ⟨a, f₂⟩ = M.mk ⟨a, f₂⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a fun j => (f₂ j).approx (n + 1)) = CofixA.intro a fun j => (f₁ j).approx (n + 1)

Tactic:
clear h₂

Result:
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a, f₂⟩) = iselect ps (M.mk ⟨a, f₁⟩)
⊢ (CofixA.intro a fun j => (f₂ j).approx (n + 1)) = CofixA.intro a fun j => (f₁ j).approx (n + 1)