-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.dest_corec {α : TypeVec n} {β : Type u} (g : β → P (α.append1 β)) (x : β) :
    M.dest P (M.corec P g x) = appendFun id (M.corec P g) <$$> g x

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ ⟨(g x).fst,
      splitFun (dropFun (g x).snd)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun (g x).snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> g x

Tactic:
obtain ⟨a, f⟩ := g x

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨⟨a, f⟩.fst,
      splitFun (dropFun ⟨a, f⟩.snd)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
          lastFun ⟨a, f⟩.snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨⟨a, f⟩.fst,
      splitFun (dropFun ⟨a, f⟩.snd)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
          lastFun ⟨a, f⟩.snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Tactic:
dsimp

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Tactic:
rw [MvPFunctor.map_eq]

Result:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f)⟩ =
    ⟨a, (TypeVec.id ::: corec P g) ⊚ f⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f)⟩ =
    ⟨a, (TypeVec.id ::: corec P g) ⊚ f⟩

Tactic:
congr

Result:
case mk.e_snd
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f

Proof state:
case mk.e_snd
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f

Tactic:
conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]

Result:
case mk.e_snd
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ dest P (corec P g x) = (TypeVec.id ::: corec P g) <$$> g x

Tactic:
trans

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.10951

n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ ?m.10951 = (TypeVec.id ::: corec P g) <$$> g x

n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ ↑P (α ::: P.M α)

Proof state:
case mk.e_snd
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    splitFun (TypeVec.id ⊚ dropFun f) (corec P g ∘ lastFun f)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.10951

Tactic:
apply M.dest_corec'

Result:
no goals