n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)
rw [M.dest_map]
case e_a
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x
congr
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x
case e_a
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)
apply eq_of_drop_last_eq <;> simp
case e_a.h₁.h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
x✝ : TypeVec.last (α ::: M P α)
⊢ lastFun g x✝ = dropFun g <$$> x✝
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x
ext1
no goals
case e_a.h₁.h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
x✝ : TypeVec.last (α ::: M P α)
⊢ lastFun g x✝ = dropFun g <$$> x✝
apply h