n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.38931

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

n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ Obj P (α ::: M P α)
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = (TypeVec.id ::: corec P g) <$$> g x
trans
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ { fst := (g x).fst,
      snd :=
        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
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.38931

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

n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ Obj P (α ::: M P α)
apply M.dest_corec'
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := { fst := a, snd := f }.fst,
      snd :=
        splitFun (dropFun { fst := a, snd := f }.snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun { fst := a, snd := f }.snd) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ { fst := (g x).fst,
      snd :=
        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
cases' g x with a f
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        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) <$$> { fst := a, snd := f }
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := { fst := a, snd := f }.fst,
      snd :=
        splitFun (dropFun { fst := a, snd := f }.snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun { fst := a, snd := f }.snd) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
dsimp
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    { fst := a, snd := (TypeVec.id ::: corec P g) ⊚ f }
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        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) <$$> { fst := a, snd := f }
rw [MvPFunctor.map_eq]
case mk.e_snd
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P 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
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    { fst := a, snd := (TypeVec.id ::: corec P g) ⊚ f }
congr
no goals
case mk.e_snd
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P 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
conv =>
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]