n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)) →
      WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f)) (MvPFunctor.wMk (P F) a f' f)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
⊢ WEquiv (wrepr x) x
apply q.P.w_ind _ x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f)) (MvPFunctor.wMk (P F) a f' f)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    (∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)) →
      WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f)) (MvPFunctor.wMk (P F) a f' f)
intro a f' f ih
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f))
    (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f }))

case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f }))
    (MvPFunctor.wMk (P F) a f' f)
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f)) (MvPFunctor.wMk (P F) a f' f)
apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv
    (match { fst := a, snd := splitFun f' (wrepr ∘ f) } with
    | { fst := a, snd := f } => MvPFunctor.wMk (P F) a (dropFun f) (lastFun f))
    (MvPFunctor.wMk (P F) a f' f)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f }))
    (MvPFunctor.wMk (P F) a f' f)
rw [q.P.map_eq, MvPFunctor.wMk', appendFun_comp_splitFun, id_comp]
case a.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (lastFun (splitFun f' (wrepr ∘ f)) x) (f x)
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv
    (match { fst := a, snd := splitFun f' (wrepr ∘ f) } with
    | { fst := a, snd := f } => MvPFunctor.wMk (P F) a (dropFun f) (lastFun f))
    (MvPFunctor.wMk (P F) a f' f)
apply WEquiv.ind
no goals
case a.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (lastFun (splitFun f' (wrepr ∘ f)) x) (f x)
exact ih
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f))) =
    abs
      (MvPFunctor.wDest' (P F)
        (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ WEquiv (wrepr (MvPFunctor.wMk (P F) a f' f))
    (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f }))
apply wEquiv.abs'
no goals
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
ih : ∀ (i : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (wrepr (f i)) (f i)
⊢ abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f))) =
    abs
      (MvPFunctor.wDest' (P F)
        (MvPFunctor.wMk' (P F) ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]