-- 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.zero
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✝
f₀ : F.B a✝² → CofixA F 0
h₀ : x (succ 0) = CofixA.intro a✝² f₀
⊢ (match 0, 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₁] at h₀

Result:
case intro.intro.zero
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✝
f₀ : F.B a✝² → CofixA F 0
h₀ : CofixA.intro a✝¹ a✝ = CofixA.intro a✝² f₀
⊢ (match 0, 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.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

Tactic:
dsimp only [comp_apply]

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
⊢ ∀ (n : ℕ), head' (x n.succ) = head' (x 1)

Tactic:
clear m n

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

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

Tactic:
intro n

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

Proof state:
case intro.intro.zero
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✝
f₀ : F.B a✝² → CofixA F 0
h₀ : CofixA.intro a✝¹ a✝ = CofixA.intro a✝² f₀
⊢ (match 0, 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:
cases h₀

Result:
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

Proof state:
case intro.intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
a✝² : F.A
f₀ : F.B a✝² → CofixA F n
h₀ : x n.succ = CofixA.intro a✝² f₀
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F 0
h₁ : x 1 = CofixA.intro a✝¹ a✝
⊢ (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

Tactic:
induction' n with n n_ih

Result:
case intro.intro.zero
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✝
f₀ : F.B a✝² → CofixA F 0
h₀ : x (succ 0) = CofixA.intro a✝² f₀
⊢ (match 0, CofixA.intro a✝² f₀ with
    | x, CofixA.intro i a => i) =
    match 0, CofixA.intro a✝¹ a✝ with
    | x, CofixA.intro i a => i

case intro.intro.succ
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₀
⊢ (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:
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
⊢ head' (x n.succ) = head' (x 1)

Tactic:
rcases h₀ : x (succ n) with - | ⟨_, f₀⟩

Result:
case intro
F : PFunctor.{u}
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
a✝ : F.A
f₀ : F.B a✝ → CofixA F n
h₀ : x n.succ = CofixA.intro a✝ f₀
⊢ head' (CofixA.intro a✝ f₀) = head' (x 1)