-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem head_succ' (n m : ℕ) (x : ∀ n, CofixA F n) (Hconsistent : AllAgree x) :
    head' (x (succ n)) = head' (x (succ m))

Proof state:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
H : Agree (CofixA.intro a✝¹ a✝) (CofixA.intro a✝⁴ f₀)
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ x n.succ = CofixA.intro a✝⁴ (truncate ∘ f₀)

Tactic:
rw [h₂]

Result:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
H : Agree (CofixA.intro a✝¹ a✝) (CofixA.intro a✝⁴ f₀)
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro a✝⁴ (truncate ∘ f₀)

Proof state:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
H : Agree (CofixA.intro a✝¹ a✝) (CofixA.intro a✝⁴ f₀)
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ (match n + 1, CofixA.intro a✝⁴ f₀ with
    | x, CofixA.intro i a => i) =
    match 0, CofixA.intro a✝³ a✝² with
    | x, CofixA.intro i a => i

Tactic:
apply n_ih (truncate ∘ f₀)

Result:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
H : Agree (CofixA.intro a✝¹ a✝) (CofixA.intro a✝⁴ f₀)
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ x n.succ = CofixA.intro a✝⁴ (truncate ∘ f₀)

Proof state:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
H : Agree (x n.succ) (x n.succ.succ)
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ (match n + 1, CofixA.intro a✝⁴ f₀ with
    | x, CofixA.intro i a => i) =
    match 0, CofixA.intro a✝³ a✝² with
    | x, CofixA.intro i a => i

Tactic:
rw [h₀, h₂] at H

Result:
case intro.intro.succ.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝⁴ a✝³ : F.A
a✝² : F.B a✝³ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝³ a✝²
n : ℕ
n_ih :
  ∀ (f₀ : F.B a✝⁴ → CofixA F n),
    x n.succ = CofixA.intro a✝⁴ f₀ →
      (match n, CofixA.intro a✝⁴ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝³ a✝² with
        | x, CofixA.intro i a => i
f₀ : F.B a✝⁴ → CofixA F (n + 1)
h₀ : x (n + 1).succ = CofixA.intro a✝⁴ f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
H : Agree (CofixA.intro a✝¹ a✝) (CofixA.intro a✝⁴ f₀)
h₂ : x n.succ = CofixA.intro a✝¹ a✝
⊢ (match n + 1, CofixA.intro a✝⁴ f₀ with
    | x, CofixA.intro i a => i) =
    match 0, CofixA.intro a✝³ a✝² with
    | x, CofixA.intro i a => i

Proof state:
case intro.intro.zero.refl
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝ : F.A
f₀ : F.B a✝ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝ f₀
⊢ (match 0, CofixA.intro a✝ f₀ with
    | x, CofixA.intro i a => i) =
    match 0, CofixA.intro a✝ f₀ with
    | x, CofixA.intro i a => i

Tactic:
trivial

Result:
no goals

Proof state:
case intro.intro.succ.intro.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝³ a✝² : F.A
a✝¹ : F.B a✝² → CofixA F 0
h₁ : x 1 = CofixA.intro a✝² a✝¹
n✝ : ℕ
n_ih :
  ∀ (f₀ : F.B a✝³ → CofixA F n✝),
    x n✝.succ = CofixA.intro a✝³ f₀ →
      (match n✝, CofixA.intro a✝³ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝² a✝¹ with
        | x, CofixA.intro i a => i
f₀ : F.B a✝³ → CofixA F (n✝ + 1)
h₀ : x (n✝ + 1).succ = CofixA.intro a✝³ f₀
n : ℕ
a✝ : F.B a✝³ → CofixA F n✝
h₂ : x n✝.succ = CofixA.intro a✝³ a✝
hagree : ∀ (i : F.B a✝³), Agree (a✝ i) (f₀ i)
⊢ CofixA.intro a✝³ a✝ = CofixA.intro a✝³ (truncate ∘ f₀)

Tactic:
congr

Result:
case intro.intro.succ.intro.intro.e_a
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝³ a✝² : F.A
a✝¹ : F.B a✝² → CofixA F 0
h₁ : x 1 = CofixA.intro a✝² a✝¹
n✝ : ℕ
n_ih :
  ∀ (f₀ : F.B a✝³ → CofixA F n✝),
    x n✝.succ = CofixA.intro a✝³ f₀ →
      (match n✝, CofixA.intro a✝³ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝² a✝¹ with
        | x, CofixA.intro i a => i
f₀ : F.B a✝³ → CofixA F (n✝ + 1)
h₀ : x (n✝ + 1).succ = CofixA.intro a✝³ f₀
n : ℕ
a✝ : F.B a✝³ → CofixA F n✝
h₂ : x n✝.succ = CofixA.intro a✝³ a✝
hagree : ∀ (i : F.B a✝³), Agree (a✝ i) (f₀ i)
⊢ a✝ = truncate ∘ f₀

Proof state:
case intro.intro.succ.intro.intro.e_a
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝³ a✝² : F.A
a✝¹ : F.B a✝² → CofixA F 0
h₁ : x 1 = CofixA.intro a✝² a✝¹
n✝ : ℕ
n_ih :
  ∀ (f₀ : F.B a✝³ → CofixA F n✝),
    x n✝.succ = CofixA.intro a✝³ f₀ →
      (match n✝, CofixA.intro a✝³ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝² a✝¹ with
        | x, CofixA.intro i a => i
f₀ : F.B a✝³ → CofixA F (n✝ + 1)
h₀ : x (n✝ + 1).succ = CofixA.intro a✝³ f₀
n : ℕ
a✝ : F.B a✝³ → CofixA F n✝
h₂ : x n✝.succ = CofixA.intro a✝³ a✝
hagree : ∀ (i : F.B a✝³), Agree (a✝ i) (f₀ i)
⊢ a✝ = truncate ∘ f₀

Tactic:
funext j

Result:
case intro.intro.succ.intro.intro.e_a.h
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
a✝³ a✝² : F.A
a✝¹ : F.B a✝² → CofixA F 0
h₁ : x 1 = CofixA.intro a✝² a✝¹
n✝ : ℕ
n_ih :
  ∀ (f₀ : F.B a✝³ → CofixA F n✝),
    x n✝.succ = CofixA.intro a✝³ f₀ →
      (match n✝, CofixA.intro a✝³ f₀ with
        | x, CofixA.intro i a => i) =
        match 0, CofixA.intro a✝² a✝¹ with
        | x, CofixA.intro i a => i
f₀ : F.B a✝³ → CofixA F (n✝ + 1)
h₀ : x (n✝ + 1).succ = CofixA.intro a✝³ f₀
n : ℕ
a✝ : F.B a✝³ → CofixA F n✝
h₂ : x n✝.succ = CofixA.intro a✝³ a✝
hagree : ∀ (i : F.B a✝³), Agree (a✝ i) (f₀ i)
j : F.B a✝³
⊢ a✝ j = (truncate ∘ f₀) j

Proof state:
F : PFunctor.{u}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (x n.succ) = head' (x m.succ)

Tactic:
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]

Result:
F : PFunctor.{u}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ ∀ (n : ℕ), head' (x n.succ) = head' (x 1)