[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
⊢ WPath P (WType.mk a f) ⟹ α
[PROOFSTEP]
intro i x
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a f) i
⊢ α i
[PROOFSTEP]
match x with
| WPath.root _ _ i c => exact g' i c
| WPath.child _ _ i j c => exact g j i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i✝ : Fin2 n
x : WPath P (WType.mk a f) i✝
i : Fin2 n
c : B (drop P) a i
⊢ α i
[PROOFSTEP]
exact g' i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i✝ : Fin2 n
x : WPath P (WType.mk a f) i✝
i : Fin2 n
j : PFunctor.B (last P) a
c : WPath P (f j) i
⊢ α i
[PROOFSTEP]
exact g j i c
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) = h
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i x = h i x
[PROOFSTEP]
cases x
[GOAL]
case a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
c✝ : B (drop P) a i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i (WPath.root a (fun j => f j) i c✝) =
    h i (WPath.root a (fun j => f j) i c✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
j✝ : PFunctor.B (last P) a
c✝ : WPath P ((fun j => f j) j✝) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i (WPath.child a (fun j => f j) i j✝ c✝) =
    h i (WPath.child a (fun j => f j) i j✝ c✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
⊢ h ⊚ wPathCasesOn P g' g = wPathCasesOn P (h ⊚ g') fun i => h ⊚ g i
[PROOFSTEP]
ext i x
[GOAL]
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ (h ⊚ wPathCasesOn P g' g) i x = wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i x
[PROOFSTEP]
cases x
[GOAL]
case a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
c✝ : B (drop P) a i
⊢ (h ⊚ wPathCasesOn P g' g) i (WPath.root a (fun j => f j) i c✝) =
    wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i (WPath.root a (fun j => f j) i c✝)
[PROOFSTEP]
rfl
[GOAL]
case a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : TypeVec n
h : α ⟹ β
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
g' : B (drop P) a ⟹ α
g : (j : PFunctor.B (last P) a) → WPath P (f j) ⟹ α
i : Fin2 n
j✝ : PFunctor.B (last P) a
c✝ : WPath P ((fun j => f j) j✝) i
⊢ (h ⊚ wPathCasesOn P g' g) i (WPath.child a (fun j => f j) i j✝ c✝) =
    wPathCasesOn P (h ⊚ g') (fun i => h ⊚ g i) i (WPath.child a (fun j => f j) i j✝ c✝)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor (W P)
[PROOFSTEP]
delta MvPFunctor.W
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor fun α => Obj (wp P) α
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wRec P g (wMk P a f' f) = g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
rw [wMk, wRec]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (match
      let g := fun i => (f i).fst;
      let g' := wPathCasesOn P f' fun i => (f i).snd;
      { fst := WType.mk a g, snd := g' } with
    | { fst := a, snd := f' } =>
      let g' := fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h';
      wpRec P g' a f') =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
      (WType.mk a fun i => (f i).fst) (wPathCasesOn P f' fun i => (f i).snd) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
rw [wpRec_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a (wPathDestLeft P (wPathCasesOn P f' fun i => (f i).snd))
      (fun i => { fst := (f i).fst, snd := wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (wPathDestRight P (wPathCasesOn P f' fun i => (f i).snd) i)) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
dsimp only [wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : Type u_1
g : (a : P.A) → B (drop P) a ⟹ α → (PFunctor.B (last P) a → W P α) → (PFunctor.B (last P) a → C) → C
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g a f' (fun i => { fst := (f i).fst, snd := (f i).snd }) fun i =>
      wpRec P (fun a f h h' => g a (wPathDestLeft P h) (fun i => { fst := f i, snd := wPathDestRight P h i }) h')
        (f i).fst (f i).snd) =
    g a f' f fun i => wRec P g (f i)
[PROOFSTEP]
congr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
⊢ ∀ (x : W P α), C x
[PROOFSTEP]
intro x
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
x : W P α
⊢ C x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ C { fst := a, snd := f }
[PROOFSTEP]
apply @wp_ind n P α fun a f => C ⟨a, f⟩
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a : (wp P).A
f : B (wp P) a ⟹ α
⊢ ∀ (a : P.A) (f : PFunctor.B (last P) a → PFunctor.W (last P)) (f' : WPath P (WType.mk a f) ⟹ α),
    (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
      C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
intro a f f' ih'
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) → C (wMk P a f' f)
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
dsimp [wMk] at ih 
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C
    { fst := WType.mk a fun i => { fst := f i, snd := wPathDestRight P f' i }.fst,
      snd := wPathCasesOn P (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }.snd } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
dsimp at ih'' 
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' : (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
  C { fst := WType.mk a fun i => f i, snd := wPathCasesOn P (wPathDestLeft P f') fun i => wPathDestRight P f' i } :=
  ih a (wPathDestLeft P f') fun i => { fst := f i, snd := wPathDestRight P f' i }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
rw [wPathCasesOn_eta] at ih'' 
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ C { fst := WType.mk a f, snd := f' }
[PROOFSTEP]
apply ih''
[GOAL]
case mk.ih
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
C : W P α → Prop
ih :
  ∀ (a : P.A) (f' : B (drop P) a ⟹ α) (f : PFunctor.B (last P) a → W P α),
    (∀ (i : PFunctor.B (last P) a), C (f i)) →
      C { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd }
a✝ : (wp P).A
f✝ : B (wp P) a✝ ⟹ α
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
f' : WPath P (WType.mk a f) ⟹ α
ih' : ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
ih'' :
  (∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }) →
    C { fst := WType.mk a fun i => f i, snd := f' }
⊢ ∀ (i : PFunctor.B (last P) a), C { fst := f i, snd := wPathDestRight P f' i }
[PROOFSTEP]
apply ih'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => g <$$> f i
[PROOFSTEP]
show _ = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') (MvFunctor.map g ∘ f)
[PROOFSTEP]
have : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩ :=
  by
  ext i : 1
  dsimp [Function.comp]
  cases f i
  rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
ext i : 1
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
⊢ (MvFunctor.map g ∘ f) i = { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
dsimp [Function.comp]
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
⊢ g <$$> f i = { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
cases f i
[GOAL]
case h.mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
i : PFunctor.B (last P) a
fst✝ : (wp P).A
snd✝ : B (wp P) fst✝ ⟹ α
⊢ g <$$> { fst := fst✝, snd := snd✝ } =
    { fst := { fst := fst✝, snd := snd✝ }.fst, snd := g ⊚ { fst := fst✝, snd := snd✝ }.snd }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') (MvFunctor.map g ∘ f)
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
  ext1 x
  cases f x
  rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
⊢ f = fun i => { fst := (f i).fst, snd := (f i).snd }
[PROOFSTEP]
ext1 x
[GOAL]
case h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
x : PFunctor.B (last P) a
⊢ f x = { fst := (f x).fst, snd := (f x).snd }
[PROOFSTEP]
cases f x
[GOAL]
case h.mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
x : PFunctor.B (last P) a
fst✝ : (wp P).A
snd✝ : B (wp P) fst✝ ⟹ α
⊢ { fst := fst✝, snd := snd✝ } = { fst := { fst := fst✝, snd := snd✝ }.fst, snd := { fst := fst✝, snd := snd✝ }.snd }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ g <$$> wMk P a f' f = wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ (g <$$> wMk P a f' fun i => { fst := (f i).fst, snd := (f i).snd }) =
    wMk P a (g ⊚ f') fun i =>
      { fst := ((fun i => { fst := (f i).fst, snd := (f i).snd }) i).fst,
        snd := g ⊚ ((fun i => { fst := (f i).fst, snd := (f i).snd }) i).snd }
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ (g <$$> wMk P a f' fun i => { fst := (f i).fst, snd := (f i).snd }) =
    wMk P a (g ⊚ f') fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
[PROOFSTEP]
rw [wMk_eq, wMk_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
⊢ g <$$> { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd } =
    { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P (g ⊚ f') fun i => g ⊚ (f i).snd }
[PROOFSTEP]
have h := MvPFunctor.map_eq P.wp g
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
this✝ : MvFunctor.map g ∘ f = fun i => { fst := (f i).fst, snd := g ⊚ (f i).snd }
this : f = fun i => { fst := (f i).fst, snd := (f i).snd }
h : ∀ (a : (wp P).A) (f : B (wp P) a ⟹ α), g <$$> { fst := a, snd := f } = { fst := a, snd := g ⊚ f }
⊢ g <$$> { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P f' fun i => (f i).snd } =
    { fst := WType.mk a fun i => (f i).fst, snd := wPathCasesOn P (g ⊚ f') fun i => g ⊚ (f i).snd }
[PROOFSTEP]
rw [h, comp_wPathCasesOn]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ (g ::: wMap P g) <$$> objAppend1 P a f' f = objAppend1 P a (g ⊚ f') fun x => wMap P g (f x)
[PROOFSTEP]
rw [objAppend1, objAppend1, map_eq, appendFun, ← splitFun_comp]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α γ : TypeVec n
g : α ⟹ γ
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ { fst := a, snd := splitFun (g ⊚ f') (wMap P g ∘ f) } = { fst := a, snd := splitFun (g ⊚ f') fun x => wMap P g (f x) }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f' : B (drop P) a ⟹ α
f : PFunctor.B (last P) a → W P α
⊢ wDest' P (wMk P a f' f) = { fst := a, snd := splitFun f' f }
[PROOFSTEP]
rw [wDest', wRec_eq]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : Obj P (α ::: W P α)
⊢ wDest' P (wMk' P x) = x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : B P a ⟹ α ::: W P α
⊢ wDest' P (wMk' P { fst := a, snd := f }) = { fst := a, snd := f }
[PROOFSTEP]
rw [wMk', wDest'_wMk, split_dropFun_lastFun]
