n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
⊢ abs (MvPFunctor.wDest' (P F) x) = abs (MvPFunctor.wDest' (P F) y) → WEquiv x y
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
h : abs (MvPFunctor.wDest' (P F) x) = abs (MvPFunctor.wDest' (P F) y)
⊢ WEquiv x y
revert h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α),
    abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)) = abs (MvPFunctor.wDest' (P F) y) →
      WEquiv (MvPFunctor.wMk (P F) a f' f) y
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
⊢ abs (MvPFunctor.wDest' (P F) x) = abs (MvPFunctor.wDest' (P F) y) → WEquiv x y
apply q.P.w_cases _ x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α
⊢ abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) = abs (MvPFunctor.wDest' (P F) y) →
    WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) y
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α),
    abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)) = abs (MvPFunctor.wDest' (P F) y) →
      WEquiv (MvPFunctor.wMk (P F) a f' f) y
intro a₀ f'₀ f₀
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) =
        abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)) →
      WEquiv (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 y : 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) α
⊢ abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) = abs (MvPFunctor.wDest' (P F) y) →
    WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) y
apply q.P.w_cases _ y
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α
a₁ : (P F).A
f'₁ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁ ⟹ α
f₁ : PFunctor.B (MvPFunctor.last (P F)) a₁ → MvPFunctor.W (P F) α
⊢ abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) =
      abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)) →
    WEquiv (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 y : 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) α
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α),
    abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) =
        abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)) →
      WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a f' f)
intro a₁ f'₁ f₁
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : 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) α
a₁ : (P F).A
f'₁ : MvPFunctor.B (MvPFunctor.drop (P F)) a₁ ⟹ α
f₁ : PFunctor.B (MvPFunctor.last (P F)) a₁ → MvPFunctor.W (P F) α
⊢ abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)) =
      abs (MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)) →
    WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
apply WEquiv.abs