-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem agree_iff_agree' {n : ℕ} (x y : M F) :
    Agree (x.approx n) (y.approx <| n + 1) ↔ Agree' n x y

Proof state:
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Tactic:
apply n_ih

Result:
case mpr.succ.step.f.f.refl.refl.a.h
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree' n✝ (x' i) (y' i)

Proof state:
case mpr.succ.step.f.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro x_a fun j => (x_f j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Tactic:
have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›

Result:
case mpr.succ.step.f.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
h_a_1 : ⟨x_a, x_f⟩ = ⟨a, x'⟩
⊢ Agree (CofixA.intro x_a fun j => (x_f j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Proof state:
case mp.succ.f.f.intro
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j => (f✝¹ j).approx n✝) i) ((fun j => (f✝ j).approx (n✝ + 1)) i)
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
constructor <;> try rfl

Result:
case mp.succ.f.f.intro.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j => (f✝¹ j).approx n✝) i) ((fun j => (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)

Proof state:
case mp.succ.f.f.intro.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j => (f✝¹ j).approx n✝) i) ((fun j => (f✝ j).approx (n✝ + 1)) i)
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝¹ i) (f✝ i)

Tactic:
intro i

Result:
case mp.succ.f.f.intro.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j => (f✝¹ j).approx n✝) i) ((fun j => (f✝ j).approx (n✝ + 1)) i)
i : F.B a✝
⊢ Agree' n✝ (f✝¹ i) (f✝ i)

Proof state:
case mpr.succ
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
h : Agree' (n✝ + 1) x y
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
obtain - | @⟨_, a, x', y'⟩ := h

Result:
case mpr.succ.step
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
x y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : x = M.mk ⟨a, x'⟩
a✝ : y = M.mk ⟨a, y'⟩
⊢ Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Proof state:
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ ∀ (i : F.B a), Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Tactic:
intro i

Result:
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
i : F.B a
⊢ Agree ((x' i).approx n✝) ((y' i).approx (n✝ + 1))

Proof state:
case mpr.succ.step.f.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))

Tactic:
simp only [approx_mk]

Result:
case mpr.succ.step.f.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro x_a fun j => (x_f j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Proof state:
case mpr.succ.step.f.f.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
h_a_2 : ⟨y_a, y_f⟩ = ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Tactic:
cases h_a_2

Result:
case mpr.succ.step.f.f.refl.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
a✝ : M.mk ⟨a, y'⟩ = M.mk ⟨a, y'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro a fun j => (y' j).approx (n✝ + 1))

Proof state:
case mpr.succ.step.f.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
h_a_1 : ⟨x_a, x_f⟩ = ⟨a, x'⟩
⊢ Agree (CofixA.intro x_a fun j => (x_f j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Tactic:
cases h_a_1

Result:
case mpr.succ.step.f.f.refl
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
y_a : F.A
y_f : F.B y_a → F.M
a✝¹ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
a✝ : M.mk ⟨a, x'⟩ = M.mk ⟨a, x'⟩
⊢ Agree (CofixA.intro a fun j => (x' j).approx n✝) (CofixA.intro y_a fun j => (y_f j).approx (n✝ + 1))

Proof state:
case mp.succ
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
x y : F.M
h : Agree (x.approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) x y

Tactic:
induction x using PFunctor.M.casesOn'

Result:
case mp.succ.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
y : F.M
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree ((M.mk ⟨a✝, f✝⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) y