-- 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)
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)

Tactic:
iterate 3 (have := mk_inj ‹_›; cases this)

Result:
case succ.step.step.f.f.refl.refl.refl
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
f✝¹ : F.B a✝⁵ → F.M
a✝⁴ : M.mk ⟨a✝⁵, f✝¹⟩ = M.mk ⟨a✝⁷, y✝¹⟩
a✝³ : F.A
f✝ : F.B a✝³ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝⁵, f✝¹⟩) = iselect ps (M.mk ⟨a✝³, f✝⟩)
y✝ : F.B a✝⁷ → F.M
a✝² : M.mk ⟨a✝³, f✝⟩ = M.mk ⟨a✝⁷, y✝⟩
a✝¹ : ∀ (i : F.B a✝⁷), Agree' n (x✝ i) (y✝ i)
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 : 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)
y 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✝² : y = M.mk ⟨a✝⁵, y✝⟩
a✝¹ : F.A
f✝ : F.B a✝¹ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝¹, f✝⟩) = iselect ps y
a✝ : M.mk ⟨a✝¹, f✝⟩ = M.mk ⟨a✝⁸, y✝¹⟩
⊢ (M.mk ⟨a✝¹, f✝⟩).approx (n + 1 + 1) = y.approx (n + 1 + 1)

Tactic:
induction y using PFunctor.M.casesOn'

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)
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)

Proof state:
case zero.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
hx : Agree' 0 z (M.mk ⟨a✝¹, f✝¹⟩)
a✝ : F.A
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : iselect [] (M.mk ⟨a✝¹, f✝¹⟩) = iselect [] (M.mk ⟨a✝, f✝⟩)
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Tactic:
simp only [iselect_nil] at hrec

Result:
case zero.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
hx : Agree' 0 z (M.mk ⟨a✝¹, f✝¹⟩)
a✝ : F.A
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : a✝¹ = a✝
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Proof state:
case zero.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝¹ : F.A
f✝¹ : F.B a✝¹ → F.M
hx : Agree' 0 z (M.mk ⟨a✝¹, f✝¹⟩)
a✝ : F.A
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
hrec : a✝¹ = a✝
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Tactic:
subst hrec

Result:
case zero.f.f
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝ : F.A
f✝¹ : F.B a✝ → F.M
hx : Agree' 0 z (M.mk ⟨a✝, f✝¹⟩)
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
⊢ (M.mk ⟨a✝, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Proof state:
case succ.step.step
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)
x y z : F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
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✝⁴ : x = M.mk ⟨a✝⁷, y✝¹⟩
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✝ : y = M.mk ⟨a✝³, y✝⟩
⊢ x.approx (n + 1 + 1) = y.approx (n + 1 + 1)

Tactic:
induction x using PFunctor.M.casesOn'

Result:
case succ.step.step.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)
y 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✝² : y = M.mk ⟨a✝⁵, y✝⟩
a✝¹ : F.A
f✝ : F.B a✝¹ → F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps (M.mk ⟨a✝¹, f✝⟩) = iselect ps y
a✝ : M.mk ⟨a✝¹, f✝⟩ = M.mk ⟨a✝⁸, y✝¹⟩
⊢ (M.mk ⟨a✝¹, f✝⟩).approx (n + 1 + 1) = y.approx (n + 1 + 1)

Proof state:
case succ.step.step.f.f.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)
a✝ : F.A
f✝ : F.B a✝ → F.M
h₂ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₂⟩
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₁⟩)
this : ⟨a✝, f✝⟩ = ⟨a, f₂⟩
⊢ (CofixA.intro a✝ fun j => (f✝ j).approx (n + 1)) = CofixA.intro a fun j => (f₁ j).approx (n + 1)

Tactic:
cases this

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₃⟩
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)