-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem truncate_eq_of_agree {n : ℕ} (x : CofixA F n) (y : CofixA F (succ n)) (h : Agree x y) :
    truncate y = x

Proof state:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝³ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : F.B a✝² → CofixA F n✝
x'✝ : F.B a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : F.B a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ truncate (CofixA.intro a✝² x'✝) = CofixA.intro a✝² a✝¹

Tactic:
simp only [truncate, Function.comp_def, eq_self_iff_true, heq_iff_eq]

Result:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝³ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : F.B a✝² → CofixA F n✝
x'✝ : F.B a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : F.B a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ (CofixA.intro a✝² fun x => truncate (x'✝ x)) = CofixA.intro a✝² a✝¹

Proof state:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ (CofixA.intro a fun x => truncate (y x)) = CofixA.intro a f

Tactic:
suffices (fun x => truncate (y x)) = f
  by simp [this]

Result:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ (fun x => truncate (y x)) = f

Proof state:
case succ.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝⁴ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝³ : F.A
a✝² : F.B a✝³ → CofixA F n✝
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F (n✝ + 1)
h : Agree (CofixA.intro a✝³ a✝²) (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.intro a✝³ a✝²

Tactic:
cases h

Result:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝³ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : F.B a✝² → CofixA F n✝
x'✝ : F.B a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : F.B a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ truncate (CofixA.intro a✝² x'✝) = CofixA.intro a✝² a✝¹

Proof state:
F : PFunctor.{u}
n : ℕ
x : CofixA F n
y : CofixA F n.succ
h : Agree x y
⊢ truncate y = x

Tactic:
induction n <;> cases x <;> cases y

Result:
case zero.continue.intro
F : PFunctor.{u}
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F 0
h : Agree CofixA.continue (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.continue

case succ.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝⁴ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝³ : F.A
a✝² : F.B a✝³ → CofixA F n✝
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F (n✝ + 1)
h : Agree (CofixA.intro a✝³ a✝²) (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.intro a✝³ a✝²

Proof state:
case succ.intro.intro.intro.h
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y✝ : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y✝ i)
y : F.B a
⊢ truncate (y✝ y) = f y

Tactic:
apply n_ih

Result:
case succ.intro.intro.intro.h.h
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y✝ : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y✝ i)
y : F.B a
⊢ Agree (f y) (y✝ y)

Proof state:
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
this : (fun x => truncate (y x)) = f
⊢ (CofixA.intro a fun x => truncate (y x)) = CofixA.intro a f

Tactic:
simp [this]

Result:
no goals

Proof state:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
a✝³ : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : F.B a✝² → CofixA F n✝
x'✝ : F.B a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : F.B a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ (CofixA.intro a✝² fun x => truncate (x'✝ x)) = CofixA.intro a✝² a✝¹

Tactic:
rename_i n_ih a f y h₁

Result:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ (CofixA.intro a fun x => truncate (y x)) = CofixA.intro a f

Proof state:
case succ.intro.intro.intro
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ (fun x => truncate (y x)) = f

Tactic:
funext y

Result:
case succ.intro.intro.intro.h
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y✝ : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y✝ i)
y : F.B a
⊢ truncate (y✝ y) = f y

Proof state:
case zero.continue.intro
F : PFunctor.{u}
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F 0
h : Agree CofixA.continue (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.continue

Tactic:
rfl

Result:
no goals

Proof state:
case succ.intro.intro.intro.h.h
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F n✝.succ), Agree x y → truncate y = x
a : F.A
f : F.B a → CofixA F n✝
y✝ : F.B a → CofixA F (n✝ + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y✝ i)
y : F.B a
⊢ Agree (f y) (y✝ y)

Tactic:
apply h₁

Result:
no goals