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)
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
show _ = P.wMk a (g ⊚ f') (MvFunctor.map g ∘ f)
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)
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)
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
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 }
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)
rw [this]
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 }
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 }
have : f = fun i => ⟨(f i).fst, (f i).snd⟩ := by
  ext1 x
  cases f x
  rfl
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 }
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 }
rw [this]
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 }
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 }
dsimp
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 }
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 }
rw [wMk_eq, wMk_eq]
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 }
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 }
have h := MvPFunctor.map_eq P.wp g
no goals
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 }
rw [h, comp_wPathCasesOn]
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 }
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 }
ext i : 1
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 }
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 }
dsimp [Function.comp]
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 }
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 }
cases f i
no goals
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 }
rfl
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 }
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 }
ext1 x
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 }
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 }
cases f x
no goals
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 }
rfl