-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem cases_mk {r : M F → Sort*} (x : F (M F)) (f : ∀ x : F (M F), r (M.mk x)) :
    PFunctor.M.cases f (M.mk x) = f x

Proof state:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro ⟨fst✝, snd✝⟩.fst fun i => (⟨fst✝, snd✝⟩.snd i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩) =
    f ⟨fst✝, snd✝⟩

Tactic:
dsimp only [Approx.sMk]

Result:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro fst✝ fun i => (snd✝ i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩) =
    f ⟨fst✝, snd✝⟩

Proof state:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ f
      ⟨match 0, CofixA.intro fst✝ fun i => (snd✝ i).approx 0 with
        | x, CofixA.intro i a => i,
        fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩ =
    f ⟨fst✝, snd✝⟩

Tactic:
apply congrFun

Result:
case mk.h
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ f = f

Proof state:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro fst✝ fun i => (snd✝ i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩) =
    f ⟨fst✝, snd✝⟩

Tactic:
simp only [Eq.mpr]

Result:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ f
      ⟨match 0, CofixA.intro fst✝ fun i => (snd✝ i).approx 0 with
        | x, CofixA.intro i a => i,
        fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩ =
    f ⟨fst✝, snd✝⟩

Proof state:
F : PFunctor.{u}
r : F.M → Sort u_2
x : ↑F F.M
f : (x : ↑F F.M) → r (M.mk x)
⊢ M.cases f (M.mk x) = f x

Tactic:
dsimp only [M.mk, PFunctor.M.cases, dest, head, Approx.sMk, head']

Result:
F : PFunctor.{u}
r : F.M → Sort u_2
x : ↑F F.M
f : (x : ↑F F.M) → r (M.mk x)
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro x.fst fun i => (x.snd i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk x, consistent := ⋯ } i⟩) =
    f x

Proof state:
F : PFunctor.{u}
r : F.M → Sort u_2
x : ↑F F.M
f : (x : ↑F F.M) → r (M.mk x)
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro x.fst fun i => (x.snd i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk x, consistent := ⋯ } i⟩) =
    f x

Tactic:
cases x

Result:
case mk
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ ⋯.mpr
      (f
        ⟨match 0, CofixA.intro ⟨fst✝, snd✝⟩.fst fun i => (⟨fst✝, snd✝⟩.snd i).approx 0 with
          | x, CofixA.intro i a => i,
          fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩) =
    f ⟨fst✝, snd✝⟩

Proof state:
case mk.h
F : PFunctor.{u}
r : F.M → Sort u_2
f : (x : ↑F F.M) → r (M.mk x)
fst✝ : F.A
snd✝ : F.B fst✝ → F.M
⊢ f = f

Tactic:
rfl

Result:
no goals