-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem corec_def {X} (f : X → F X) (x₀ : X) : M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

Proof state:
case e_approx.h.succ.mk
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : F.B fst✝ → X
⊢ (CofixA.intro fst✝ fun i => sCorec f (snd✝ i) n) = CofixA.intro fst✝ fun i => ((M.corec f ∘ snd✝) i).approx n

Tactic:
congr

Result:
no goals

Proof state:
case e_approx.h.succ
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ (CofixA.intro (f x₀).fst fun i => sCorec f ((f x₀).snd i) n) =
    CofixA.intro (F.map (M.corec f) (f x₀)).fst fun i => ((F.map (M.corec f) (f x₀)).snd i).approx n

Tactic:
cases f x₀

Result:
case e_approx.h.succ.mk
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : F.B fst✝ → X
⊢ (CofixA.intro ⟨fst✝, snd✝⟩.fst fun i => sCorec f (⟨fst✝, snd✝⟩.snd i) n) =
    CofixA.intro (F.map (M.corec f) ⟨fst✝, snd✝⟩).fst fun i => ((F.map (M.corec f) ⟨fst✝, snd✝⟩).snd i).approx n

Proof state:
case e_approx.h
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n

Tactic:
rcases n with - | n

Result:
case e_approx.h.zero
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ sCorec f x₀ 0 = Approx.sMk (F.map (M.corec f) (f x₀)) 0

case e_approx.h.succ
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ (n + 1) = Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1)

Proof state:
case e_approx.h.succ.mk
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : F.B fst✝ → X
⊢ (CofixA.intro ⟨fst✝, snd✝⟩.fst fun i => sCorec f (⟨fst✝, snd✝⟩.snd i) n) =
    CofixA.intro (F.map (M.corec f) ⟨fst✝, snd✝⟩).fst fun i => ((F.map (M.corec f) ⟨fst✝, snd✝⟩).snd i).approx n

Tactic:
dsimp only [PFunctor.map]

Result:
case e_approx.h.succ.mk
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : F.B fst✝ → X
⊢ (CofixA.intro fst✝ fun i => sCorec f (snd✝ i) n) = CofixA.intro fst✝ fun i => ((M.corec f ∘ snd✝) i).approx n

Proof state:
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := ⋯ } = { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }

Tactic:
congr with n

Result:
case e_approx.h
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n

Proof state:
case e_approx.h.succ
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ (n + 1) = Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1)

Tactic:
dsimp only [sCorec, Approx.sMk]

Result:
case e_approx.h.succ
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
n : ℕ
⊢ (CofixA.intro (f x₀).fst fun i => sCorec f ((f x₀).snd i) n) =
    CofixA.intro (F.map (M.corec f) (f x₀)).fst fun i => ((F.map (M.corec f) (f x₀)).snd i).approx n

Proof state:
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ M.corec f x₀ = M.mk (F.map (M.corec f) (f x₀))

Tactic:
dsimp only [M.corec, M.mk]

Result:
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := ⋯ } = { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }

Proof state:
case e_approx.h.zero
F : PFunctor.{u}
X : Type u_2
f : X → ↑F X
x₀ : X
⊢ sCorec f x₀ 0 = Approx.sMk (F.map (M.corec f) (f x₀)) 0

Tactic:
dsimp only [sCorec, Approx.sMk]

Result:
no goals