case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P (g <$$> { fst := a, snd := f }) = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
x : M P α
⊢ dest P (g <$$> x) = (g ::: fun x => g <$$> x) <$$> dest P x
cases' x with a f
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P (g <$$> { fst := a, snd := f }) = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
rw [map_eq]
no goals
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
conv =>
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]