-- 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.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₂⟩
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✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
⊢ (M.mk ⟨a✝¹, f✝¹⟩).approx (n + 1 + 1) = (M.mk ⟨a✝, f✝⟩).approx (n + 1 + 1)

Tactic:
simp only [approx_mk, eq_self_iff_true, heq_iff_eq]

Result:
case succ.step.step.f.f.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₂⟩
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✝⟩)
f₁ : F.B a → F.M
h₁ : M.mk ⟨a✝, f✝⟩ = M.mk ⟨a, f₁⟩
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
⊢ (CofixA.intro a✝¹ fun j => (f✝¹ j).approx (n + 1)) = CofixA.intro a✝ fun j => (f✝ j).approx (n + 1)

Proof state:
case zero
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : iselect [] x = iselect [] y
⊢ x.approx (0 + 1) = y.approx (0 + 1)

Tactic:
induction x using PFunctor.M.casesOn'

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

Proof state:
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)

Tactic:
solve_by_elim

Result:
no goals

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

Proof state:
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
n : ℕ
x y z : F.M
hx : Agree' n z x
hy : Agree' n z y
hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1) = y.approx (n + 1)

Tactic:
induction' n with n n_ih generalizing x y z

Result:
case zero
F : PFunctor.{u}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : ∀ (ps : Path F), 0 = length ps → iselect ps x = iselect ps y
⊢ x.approx (0 + 1) = y.approx (0 + 1)

case succ
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
hx : Agree' (n + 1) z x
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
⊢ x.approx (n + 1 + 1) = y.approx (n + 1 + 1)

Proof state:
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₃⟩
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₂⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f₁⟩)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
simp only [iselect_cons] at hrec

Result:
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₃⟩
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)