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

Tactic:
induction' x using PFunctor.M.casesOn' with x_a x_f

Result:
case mpr.succ.step.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
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✝¹ : y = M.mk ⟨a, y'⟩
x_a : F.A
x_f : F.B x_a → F.M
a✝ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Proof state:
F : PFunctor.{u}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
constructor <;> intro h

Result:
case mp
F : PFunctor.{u}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
⊢ Agree' n x y

case mpr
F : PFunctor.{u}
n : ℕ
x y : F.M
h : Agree' n x y
⊢ Agree (x.approx n) (y.approx (n + 1))

Proof state:
case mp.succ.f.f
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
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree (CofixA.intro a✝¹ fun j => (f✝¹ j).approx n✝) (CofixA.intro a✝ fun j => (f✝ j).approx (n✝ + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝¹, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)

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

Result:
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✝⟩)

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)
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨a✝, ?mp.succ.f.f.intro.y⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mp.zero
F : PFunctor.{u}
x y : F.M
h : Agree (x.approx 0) (y.approx (0 + 1))
⊢ Agree' 0 x y

Tactic:
constructor

Result:
no goals

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

Tactic:
induction' n with _ n_ih generalizing x y

Result:
case mpr.zero
F : PFunctor.{u}
x y : F.M
h : Agree' 0 x y
⊢ Agree (x.approx 0) (y.approx (0 + 1))

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

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

Tactic:
induction' n with _ n_ih generalizing x y

Result:
case mp.zero
F : PFunctor.{u}
x y : F.M
h : Agree (x.approx 0) (y.approx (0 + 1))
⊢ Agree' 0 x y

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

Proof state:
case mpr.succ.step.f
F : PFunctor.{u}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
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✝¹ : y = M.mk ⟨a, y'⟩
x_a : F.A
x_f : F.B x_a → F.M
a✝ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
induction' y using PFunctor.M.casesOn' with y_a y_f

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 ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))

Proof state:
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)

Tactic:
simp [*]

Result:
no goals

Proof state:
case mp.succ.f.f.intro.a.h
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 ((f✝¹ i).approx n✝) ((f✝ i).approx (n✝ + 1))

Tactic:
apply hagree

Result:
no goals

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:
apply n_ih

Result:
case mp.succ.f.f.intro.a.h
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 ((f✝¹ i).approx n✝) ((f✝ i).approx (n✝ + 1))

Proof state:
case mp.succ.f.f
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
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree ((M.mk ⟨a✝¹, f✝¹⟩).approx (n✝ + 1)) ((M.mk ⟨a✝, f✝⟩).approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝¹, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)

Tactic:
simp only [approx_mk] at h

Result:
case mp.succ.f.f
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
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree (CofixA.intro a✝¹ fun j => (f✝¹ j).approx n✝) (CofixA.intro a✝ fun j => (f✝ j).approx (n✝ + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝¹, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)

Proof state:
case mpr.zero
F : PFunctor.{u}
x y : F.M
h : Agree' 0 x y
⊢ Agree (x.approx 0) (y.approx (0 + 1))

Tactic:
constructor

Result:
no goals

Proof state:
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

Tactic:
induction y using PFunctor.M.casesOn'

Result:
case mp.succ.f.f
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
a✝ : F.A
f✝ : F.B a✝ → F.M
h : Agree ((M.mk ⟨a✝¹, f✝¹⟩).approx (n✝ + 1)) ((M.mk ⟨a✝, f✝⟩).approx (n✝ + 1 + 1))
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝¹, f✝¹⟩) (M.mk ⟨a✝, f✝⟩)