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

Tactic:
have H := Hconsistent (succ n)

Result:
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₀
H : Agree (x n.succ) (x n.succ.succ)
⊢ (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
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)

Tactic:
cases h₁ : x 1

Result:
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✝
⊢ head' (CofixA.intro a✝² f₀) = head' (CofixA.intro a✝¹ a✝)

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

Tactic:
simp [this]

Result:
no goals

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✝
⊢ head' (CofixA.intro a✝² f₀) = head' (CofixA.intro a✝¹ a✝)

Tactic:
dsimp only [head']

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

Proof state:
case intro.intro.succ.intro.intro.e_a.h.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✝³
⊢ Agree (a✝ j) (f₀ j)

Tactic:
apply hagree

Result:
no goals

Proof state:
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₀
H : Agree (x n.succ) (x n.succ.succ)
⊢ (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:
cases h₂ : x (succ n)

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

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✝
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro a✝⁴ (truncate ∘ f₀)

Tactic:
obtain - | ⟨_, _, hagree⟩ := H

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

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:
rw [truncate_eq_of_agree]

Result:
case intro.intro.succ.intro.intro.e_a.h.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✝³
⊢ Agree (a✝ j) (f₀ j)