[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : 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) α
⊢ recF g (MvPFunctor.wMk (P F) a f' f) = g (abs { fst := a, snd := splitFun f' (recF g ∘ f) })
[PROOFSTEP]
rw [recF, MvPFunctor.wRec_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : 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) α
⊢ g
      (abs
        { fst := a,
          snd :=
            splitFun f' fun i =>
              MvPFunctor.wRec (P F) (fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) (f i) }) =
    g
      (abs
        { fst := a,
          snd :=
            splitFun f' ((MvPFunctor.wRec (P F) fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) ∘ f) })
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P F) α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) x))
[PROOFSTEP]
apply q.P.w_cases _ x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
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) α),
    recF g (MvPFunctor.wMk (P F) a f' f) =
      g (abs ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
intro a f' f
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
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) α
⊢ recF g (MvPFunctor.wMk (P F) a f' f) =
    g (abs ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
x y : MvPFunctor.W (P F) α
⊢ WEquiv x y → recF u x = recF u y
[PROOFSTEP]
apply q.P.w_cases _ x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α),
    WEquiv (MvPFunctor.wMk (P F) a f' f) y → recF u (MvPFunctor.wMk (P F) a f' f) = recF u y
[PROOFSTEP]
intro a₀ f'₀ f₀
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
⊢ WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) y → recF u (MvPFunctor.wMk (P F) a₀ f'₀ f₀) = recF u y
[PROOFSTEP]
apply q.P.w_cases _ y
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α),
    WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a f' f) →
      recF u (MvPFunctor.wMk (P F) a₀ f'₀ f₀) = recF u (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
intro a₁ f'₁ f₁
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
⊢ WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁) →
    recF u (MvPFunctor.wMk (P F) a₀ f'₀ f₀) = recF u (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
⊢ recF u (MvPFunctor.wMk (P F) a₀ f'₀ f₀) = recF u (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
[PROOFSTEP]
refine' @WEquiv.recOn _ _ _ _ _ (λ a a' _ => recF u a = recF u a') _ _ h _ _ _
[GOAL]
case refine'_1
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
⊢ ∀ (a : (P F).A) (f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α)
    (f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α)
    (a_1 : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)),
    (∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
        (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))) →
      (fun a a' x => recF u a = recF u a') (MvPFunctor.wMk (P F) a f' f₀) (MvPFunctor.wMk (P F) a f' f₁)
        (_ : WEquiv (MvPFunctor.wMk (P F) a f' f₀) (MvPFunctor.wMk (P F) a f' f₁))
[PROOFSTEP]
intros a f' f₀ f₁ _h ih
[GOAL]
case refine'_1
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
⊢ recF u (MvPFunctor.wMk (P F) a f' f₀) = recF u (MvPFunctor.wMk (P F) a f' f₁)
[PROOFSTEP]
simp only [recF_eq, Function.comp]
[GOAL]
case refine'_1
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
⊢ u (abs { fst := a, snd := splitFun f' fun x => recF u (f₀ x) }) =
    u (abs { fst := a, snd := splitFun f' fun x => recF u (f₁ x) })
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
⊢ (splitFun f' fun x => recF u (f₀ x)) = splitFun f' fun x => recF u (f₁ x)
[PROOFSTEP]
funext
[GOAL]
case refine'_1.e_a.e_a.e_snd.h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
x✝¹ : Fin2 (n + 1)
x✝ : MvPFunctor.B (P F) a x✝¹
⊢ splitFun f' (fun x => recF u (f₀ x)) x✝¹ x✝ = splitFun f' (fun x => recF u (f₁ x)) x✝¹ x✝
[PROOFSTEP]
congr
[GOAL]
case refine'_1.e_a.e_a.e_snd.h.h.e_g
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
x✝¹ : Fin2 (n + 1)
x✝ : MvPFunctor.B (P F) a x✝¹
⊢ (fun x => recF u (f₀ x)) = fun x => recF u (f₁ x)
[PROOFSTEP]
funext
[GOAL]
case refine'_1.e_a.e_a.e_snd.h.h.e_g.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀✝) (MvPFunctor.wMk (P F) a₁ f'₁ f₁✝)
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih :
  ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a),
    (fun a a' x => recF u a = recF u a') (f₀ x) (f₁ x) (_ : WEquiv (f₀ x) (f₁ x))
x✝² : Fin2 (n + 1)
x✝¹ : MvPFunctor.B (P F) a x✝²
x✝ : last (MvPFunctor.B (P F) a)
⊢ recF u (f₀ x✝) = recF u (f₁ x✝)
[PROOFSTEP]
apply ih
[GOAL]
case refine'_2
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ 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) α)
    (a :
      abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
        abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }),
    (fun a a' x => recF u a = recF u a') (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
      (_ : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁))
[PROOFSTEP]
intros a₀ f'₀ f₀ a₁ f'₁ f₁ h
[GOAL]
case refine'_2
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h✝ : WEquiv (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝) (MvPFunctor.wMk (P F) a₁✝ f'₁✝ 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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ recF u (MvPFunctor.wMk (P F) a₀ f'₀ f₀) = recF u (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
[PROOFSTEP]
simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]
[GOAL]
case refine'_3
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
⊢ ∀ (u_1 v w : MvPFunctor.W (P F) α) (a : WEquiv u_1 v) (a_1 : WEquiv v w),
    (fun a a' x => recF u a = recF u a') u_1 v a →
      (fun a a' x => recF u a = recF u a') v w a_1 → (fun a a' x => recF u a = recF u a') u_1 w (_ : WEquiv u_1 w)
[PROOFSTEP]
intros x y z _e₁ _e₂ ih₁ ih₂
[GOAL]
case refine'_3
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
u : F (α ::: β) → β
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) α
h : WEquiv (MvPFunctor.wMk (P F) a₀ f'₀ f₀) (MvPFunctor.wMk (P F) a₁ f'₁ f₁)
x y z : MvPFunctor.W (P F) α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z
[PROOFSTEP]
exact Eq.trans ih₁ ih₂
[GOAL]
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
[PROOFSTEP]
revert h
[GOAL]
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
[PROOFSTEP]
apply q.P.w_cases _ x
[GOAL]
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
[PROOFSTEP]
intro a₀ f'₀ f₀
[GOAL]
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
[PROOFSTEP]
apply q.P.w_cases _ y
[GOAL]
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)
[PROOFSTEP]
intro a₁ f'₁ f₁
[GOAL]
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₁)
[PROOFSTEP]
apply WEquiv.abs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
⊢ WEquiv x x
[PROOFSTEP]
apply q.P.w_cases _ x
[GOAL]
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) α),
    WEquiv (MvPFunctor.wMk (P F) a f' f) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
intro a f' f
[GOAL]
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) α
⊢ WEquiv (MvPFunctor.wMk (P F) a f' f) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
exact WEquiv.abs a f' f a f' f rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
⊢ WEquiv x y → WEquiv y x
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y : MvPFunctor.W (P F) α
h : WEquiv x y
⊢ WEquiv y x
[PROOFSTEP]
induction h
[GOAL]
case ind
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₀✝ f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a✝¹ → MvPFunctor.W (P F) α
a✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₀✝ x) (f₁✝ x)
a_ih✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₁✝ x) (f₀✝ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a✝¹ f'✝ f₁✝) (MvPFunctor.wMk (P F) a✝¹ f'✝ f₀✝)
case abs
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) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
[PROOFSTEP]
case ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
[GOAL]
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₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₁ x) (f₀ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a f' f₁) (MvPFunctor.wMk (P F) a f' f₀)
[PROOFSTEP]
case ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
[GOAL]
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₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
_h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₁ x) (f₀ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a f' f₁) (MvPFunctor.wMk (P F) a f' f₀)
[PROOFSTEP]
exact WEquiv.ind _ _ _ _ ih
[GOAL]
case abs
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) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝) (MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝)
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
[PROOFSTEP]
case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
[GOAL]
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁ f'₁ f₁) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)
[PROOFSTEP]
case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
[GOAL]
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₁ f'₁ f₁) (MvPFunctor.wMk (P F) a₀ f'₀ f₀)
[PROOFSTEP]
exact WEquiv.abs _ _ _ _ _ _ h.symm
[GOAL]
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv v✝ u✝
a_ih✝ : WEquiv w✝ v✝
⊢ WEquiv w✝ u✝
[PROOFSTEP]
case trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ y✝ x y z : MvPFunctor.W (P F) α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : WEquiv y x
ih₂ : WEquiv z y
⊢ WEquiv z x
[PROOFSTEP]
case trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ y✝ x y z : MvPFunctor.W (P F) α
_e₁ : WEquiv x y
_e₂ : WEquiv y z
ih₁ : WEquiv y x
ih₂ : WEquiv z y
⊢ WEquiv z x
[PROOFSTEP]
exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ wrepr (MvPFunctor.wMk (P F) a f' f) =
    MvPFunctor.wMk' (P F)
      (repr (abs ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
[PROOFSTEP]
rw [wrepr, recF_eq', q.P.wDest'_wMk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ (MvPFunctor.wMk' (P F) ∘ repr)
      (abs ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$> { fst := a, snd := splitFun f' f })) =
    MvPFunctor.wMk' (P F)
      (repr
        (abs
          ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$>
            { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : MvPFunctor.W (P F) α
⊢ WEquiv (wrepr x) x
[PROOFSTEP]
apply q.P.w_ind _ x
[GOAL]
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)
[PROOFSTEP]
intro a f' f ih
[GOAL]
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)
[PROOFSTEP]
apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))
[GOAL]
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 }))
[PROOFSTEP]
apply wEquiv.abs'
[GOAL]
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 })))
[PROOFSTEP]
rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]
[GOAL]
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)
[PROOFSTEP]
rw [q.P.map_eq, MvPFunctor.wMk', appendFun_comp_splitFun, id_comp]
[GOAL]
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)
[PROOFSTEP]
apply WEquiv.ind
[GOAL]
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)
[PROOFSTEP]
exact ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
⊢ WEquiv x y → WEquiv (g <$$> x) (g <$$> y)
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
h : WEquiv x y
⊢ WEquiv (g <$$> x) (g <$$> y)
[PROOFSTEP]
induction h
[GOAL]
case ind
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
a✝¹ : (P F).A
f'✝ : MvPFunctor.B (MvPFunctor.drop (P F)) a✝¹ ⟹ α
f₀✝ f₁✝ : PFunctor.B (MvPFunctor.last (P F)) a✝¹ → MvPFunctor.W (P F) α
a✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (f₀✝ x) (f₁✝ x)
a_ih✝ : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a✝¹), WEquiv (g <$$> f₀✝ x) (g <$$> f₁✝ x)
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a✝¹ f'✝ f₀✝) (g <$$> MvPFunctor.wMk (P F) a✝¹ f'✝ f₁✝)
case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝) (g <$$> MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝)
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv (g <$$> u✝) (g <$$> v✝)
a_ih✝ : WEquiv (g <$$> v✝) (g <$$> w✝)
⊢ WEquiv (g <$$> u✝) (g <$$> w✝)
[PROOFSTEP]
case ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a f' f₀) (g <$$> MvPFunctor.wMk (P F) a f' f₁)
[PROOFSTEP]
case ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a f' f₀) (g <$$> MvPFunctor.wMk (P F) a f' f₁)
[PROOFSTEP]
rw [q.P.w_map_wMk, q.P.w_map_wMk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ WEquiv (MvPFunctor.wMk (P F) a (g ⊚ f') fun i => g <$$> f₀ i) (MvPFunctor.wMk (P F) a (g ⊚ f') fun i => g <$$> f₁ i)
[PROOFSTEP]
apply WEquiv.ind
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y : MvPFunctor.W (P F) α
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f₀ f₁ : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
h : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
⊢ ∀ (x : PFunctor.B (MvPFunctor.last (P F)) a), WEquiv (g <$$> f₀ x) (g <$$> f₁ x)
[PROOFSTEP]
exact ih
[GOAL]
case abs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
a✝ :
  abs { fst := a₀✝, snd := MvPFunctor.appendContents (P F) f'₀✝ f₀✝ } =
    abs { fst := a₁✝, snd := MvPFunctor.appendContents (P F) f'₁✝ f₁✝ }
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a₀✝ f'₀✝ f₀✝) (g <$$> MvPFunctor.wMk (P F) a₁✝ f'₁✝ f₁✝)
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv (g <$$> u✝) (g <$$> v✝)
a_ih✝ : WEquiv (g <$$> v✝) (g <$$> w✝)
⊢ WEquiv (g <$$> u✝) (g <$$> w✝)
[PROOFSTEP]
case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
  rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
  show
    abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
      abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
  rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a₀ f'₀ f₀) (g <$$> MvPFunctor.wMk (P F) a₁ f'₁ f₁)
[PROOFSTEP]
case abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
  rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
  show
    abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
      abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
  rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (g <$$> MvPFunctor.wMk (P F) a₀ f'₀ f₀) (g <$$> MvPFunctor.wMk (P F) a₁ f'₁ f₁)
[PROOFSTEP]
rw [q.P.w_map_wMk, q.P.w_map_wMk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ WEquiv (MvPFunctor.wMk (P F) a₀ (g ⊚ f'₀) fun i => g <$$> f₀ i)
    (MvPFunctor.wMk (P F) a₁ (g ⊚ f'₁) fun i => g <$$> f₁ i)
[PROOFSTEP]
apply WEquiv.abs
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ abs { fst := a₀, snd := MvPFunctor.appendContents (P F) (g ⊚ f'₀) fun i => g <$$> f₀ i } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) (g ⊚ f'₁) fun i => g <$$> f₁ i }
[PROOFSTEP]
show
  abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
    abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
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) α
h :
  abs { fst := a₀, snd := MvPFunctor.appendContents (P F) f'₀ f₀ } =
    abs { fst := a₁, snd := MvPFunctor.appendContents (P F) f'₁ f₁ }
⊢ abs (MvPFunctor.objAppend1 (P F) a₀ (g ⊚ f'₀) fun x => MvPFunctor.wMap (P F) g (f₀ x)) =
    abs (MvPFunctor.objAppend1 (P F) a₁ (g ⊚ f'₁) fun x => MvPFunctor.wMap (P F) g (f₁ x))
[PROOFSTEP]
rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
[GOAL]
case trans
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x y u✝ v✝ w✝ : MvPFunctor.W (P F) α
a✝¹ : WEquiv u✝ v✝
a✝ : WEquiv v✝ w✝
a_ih✝¹ : WEquiv (g <$$> u✝) (g <$$> v✝)
a_ih✝ : WEquiv (g <$$> v✝) (g <$$> w✝)
⊢ WEquiv (g <$$> u✝) (g <$$> w✝)
[PROOFSTEP]
case trans x y z _ _ ih₁ ih₂ => apply MvQPF.WEquiv.trans; apply ih₁; apply ih₂
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv (g <$$> x) (g <$$> z)
[PROOFSTEP]
case trans x y z _ _ ih₁ ih₂ => apply MvQPF.WEquiv.trans; apply ih₁; apply ih₂
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv (g <$$> x) (g <$$> z)
[PROOFSTEP]
apply MvQPF.WEquiv.trans
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv (g <$$> x) ?v
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv ?v (g <$$> z)
case v
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ MvPFunctor.W (P F) β
[PROOFSTEP]
apply ih₁
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α β : TypeVec n
g : α ⟹ β
x✝ y✝ x y z : MvPFunctor.W (P F) α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv (g <$$> y) (g <$$> z)
[PROOFSTEP]
apply ih₂
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
have : recF g ∘ fixToW = Fix.rec g := by
  apply funext
  apply Quotient.ind
  intro x
  apply recF_eq_of_wEquiv
  apply wrepr_equiv
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ recF g ∘ fixToW = rec g
[PROOFSTEP]
apply funext
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (x : Fix F α), (recF g ∘ fixToW) x = rec g x
[PROOFSTEP]
apply Quotient.ind
[GOAL]
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ ∀ (a : MvPFunctor.W (P F) α), (recF g ∘ fixToW) (Quotient.mk (wSetoid α) a) = rec g (Quotient.mk (wSetoid α) a)
[PROOFSTEP]
intro x
[GOAL]
case h.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ (recF g ∘ fixToW) (Quotient.mk (wSetoid α) x) = rec g (Quotient.mk (wSetoid α) x)
[PROOFSTEP]
apply recF_eq_of_wEquiv
[GOAL]
case h.a.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x✝ : F (α ::: Fix F α)
x : MvPFunctor.W (P F) α
⊢ WEquiv (fixToW (Quotient.mk (wSetoid α) x)) x
[PROOFSTEP]
apply wrepr_equiv
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
conv =>
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
  lhs
  rw [Fix.rec, Fix.mk]
  dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
lhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| rec g (mk x)
[PROOFSTEP]
rw [Fix.rec, Fix.mk]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
| Quot.lift (recF g) (_ : ∀ (x y : MvPFunctor.W (P F) α), WEquiv x y → recF g x = recF g y)
    (Quot.mk Setoid.r (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> repr x)))
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> repr x)) = g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
cases' h : repr x with a f
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ recF g (MvPFunctor.wMk' (P F) ((TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : F (α ::: Fix F α)
this : recF g ∘ fixToW = rec g
a : (P F).A
f : MvPFunctor.B (P F) a ⟹ α ::: Fix F α
h : repr x = { fst := a, snd := f }
⊢ g (abs ((TypeVec.id ::: recF g) <$$> (TypeVec.id ::: fixToW) <$$> { fst := a, snd := f })) =
    g ((TypeVec.id ::: rec g) <$$> x)
[PROOFSTEP]
rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
have : Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr (q.P.wMk a f' f)⟧ :=
  by
  apply Quot.sound; apply wEquiv.abs'
  rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
  conv =>
    rhs
    rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
  congr 2; rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
  rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
  rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (wrepr (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ Setoid.r
    (MvPFunctor.wMk' (P F)
      ((TypeVec.id ::: fixToW) <$$>
        repr (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })))
    (wrepr (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
apply wEquiv.abs'
[GOAL]
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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)
          ((TypeVec.id ::: fixToW) <$$>
            repr
              (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })))) =
    abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
[GOAL]
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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
      { fst := a,
        snd := (TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
conv =>
  rhs
  rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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
      { fst := a,
        snd := (TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
  rhs
  rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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
      { fst := a,
        snd := (TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
  rhs
  rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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
      { fst := a,
        snd := (TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs (MvPFunctor.wDest' (P F) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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) (wrepr (MvPFunctor.wMk (P F) a f' f)))
[PROOFSTEP]
rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
[GOAL]
case a.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
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
      { fst := a,
        snd := (TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs { fst := a, snd := (TypeVec.id ::: wrepr) ⊚ MvPFunctor.appendContents (P F) f' f }
[PROOFSTEP]
congr 2
[GOAL]
case a.h.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ ((TypeVec.id ::: fixToW) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)) =
    (TypeVec.id ::: wrepr) ⊚ MvPFunctor.appendContents (P F) f' f
[PROOFSTEP]
rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
[GOAL]
case a.h.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ ((TypeVec.id ::: fixToW) ⊚ splitFun f' fun x => Quotient.mk (wSetoid α) (f x)) =
    (TypeVec.id ::: wrepr) ⊚ splitFun f' f
[PROOFSTEP]
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
[GOAL]
case a.h.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x => Quotient.mk (wSetoid α) (f x)) = splitFun (TypeVec.id ⊚ f') (wrepr ∘ f)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
this :
  mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (wrepr (MvPFunctor.wMk (P F) a f' f))
⊢ mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
this :
  mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (wrepr (MvPFunctor.wMk (P F) a f' f))
⊢ Quotient.mk (wSetoid α) (wrepr (MvPFunctor.wMk (P F) a f' f)) = Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
apply Quot.sound
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
this :
  mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }) =
    Quotient.mk (wSetoid α) (wrepr (MvPFunctor.wMk (P F) a f' f))
⊢ Setoid.r (wrepr (MvPFunctor.wMk (P F) a f' f)) (MvPFunctor.wMk (P F) a f' f)
[PROOFSTEP]
apply wrepr_equiv
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x
[PROOFSTEP]
apply Quot.ind
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), g₁ (Quot.mk Setoid.r a) = g₂ (Quot.mk Setoid.r a)
[PROOFSTEP]
intro x
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
x : MvPFunctor.W (P F) α
⊢ g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
[PROOFSTEP]
apply q.P.w_ind _ x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))) →
      g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
intro a f' f ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f)) = g₂ (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
show g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f)) =
    g₂ (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
rw [← Fix.ind_aux a f' f]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ g₁ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })) =
    g₂ (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
[PROOFSTEP]
apply h
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ (TypeVec.id ::: g₁) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    (TypeVec.id ::: g₂) <$$>
      abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
[PROOFSTEP]
rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ abs
      { fst := a,
        snd := (TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
    abs
      { fst := a,
        snd := (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }
[PROOFSTEP]
congr 2
[GOAL]
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ ((TypeVec.id ::: g₁) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)) =
    (TypeVec.id ::: g₂) ⊚ MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x)
[PROOFSTEP]
rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
[GOAL]
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
[PROOFSTEP]
have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
  ext x
  exact ih x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
⊢ (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) = g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)
[PROOFSTEP]
ext x
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
x : PFunctor.B (MvPFunctor.last (P F)) a
⊢ (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x = (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)) x
[PROOFSTEP]
exact ih x
[GOAL]
case a.e_a.e_snd
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g₁ g₂ : Fix F α → β
h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)
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), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))
this : (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) = g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x)
⊢ splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => Quotient.mk (wSetoid α) (f x)) =
    splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => Quotient.mk (wSetoid α) (f x))
[PROOFSTEP]
rw [this]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
⊢ rec g = h
[PROOFSTEP]
ext x
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ rec g x = h x
[PROOFSTEP]
apply Fix.ind_rec
[GOAL]
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x → rec g (mk x) = h (mk x)
[PROOFSTEP]
intro x hyp'
[GOAL]
case h.h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: fun x => h x) <$$> x
⊢ rec g (mk x) = h (mk x)
[PROOFSTEP]
rw [hyp, ← hyp', Fix.rec_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Fix F α
⊢ mk (dest x) = x
[PROOFSTEP]
change (Fix.mk ∘ Fix.dest) x = x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Fix F α
⊢ (mk ∘ dest) x = x
[PROOFSTEP]
apply Fix.ind_rec
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : Fix F α
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → (mk ∘ dest) (mk x) = mk x
[PROOFSTEP]
intro x
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → (mk ∘ dest) (mk x) = mk x
[PROOFSTEP]
dsimp
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = (TypeVec.id ::: fun x => x) <$$> x → mk (dest (mk x)) = mk x
[PROOFSTEP]
rw [Fix.dest, Fix.rec_eq, ← comp_map, ← appendFun_comp, id_comp]
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x →
    mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x
[PROOFSTEP]
intro h
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x
⊢ mk ((TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x) = mk x
[PROOFSTEP]
rw [h]
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x
⊢ mk ((TypeVec.id ::: fun x => x) <$$> x) = mk x
[PROOFSTEP]
show Fix.mk (appendFun id id <$$> x) = Fix.mk x
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x => x) <$$> x
⊢ mk ((TypeVec.id ::: _root_.id) <$$> x) = mk x
[PROOFSTEP]
rw [appendFun_id_id, MvFunctor.id_map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ dest (mk x) = x
[PROOFSTEP]
unfold Fix.dest
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x
[PROOFSTEP]
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
[PROOFSTEP]
conv =>
  rhs
  rw [← MvFunctor.id_map x]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
| ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
[PROOFSTEP]
  rhs
  rw [← MvFunctor.id_map x]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
| ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
[PROOFSTEP]
  rhs
  rw [← MvFunctor.id_map x]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
| ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
| x
[PROOFSTEP]
rw [← MvFunctor.id_map x]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ ((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x
[PROOFSTEP]
rw [← appendFun_comp, id_comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
[PROOFSTEP]
have : Fix.mk ∘ Fix.dest = _root_.id := by
  ext (x : Fix F α)
  apply Fix.mk_dest
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
⊢ mk ∘ dest = _root_.id
[PROOFSTEP]
ext (x : Fix F α)
[GOAL]
case h
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x✝ : F (α ::: Fix F α)
x : Fix F α
⊢ (mk ∘ dest) x = _root_.id x
[PROOFSTEP]
apply Fix.mk_dest
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
x : F (α ::: Fix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
[PROOFSTEP]
rw [this, appendFun_id_id]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
⊢ ∀ (x : Fix F α), p x
[PROOFSTEP]
apply Quot.ind
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
⊢ ∀ (a : MvPFunctor.W (P F) α), p (Quot.mk Setoid.r a)
[PROOFSTEP]
intro x
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
x : MvPFunctor.W (P F) α
⊢ p (Quot.mk Setoid.r x)
[PROOFSTEP]
apply q.P.w_ind _ x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))) →
      p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
intro a f' f ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ p (Quot.mk Setoid.r (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
change p ⟦q.P.wMk a f' f⟧
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ p (Quotient.mk (wSetoid α) (MvPFunctor.wMk (P F) a f' f))
[PROOFSTEP]
rw [← Fix.ind_aux a f' f]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ p (mk (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) }))
[PROOFSTEP]
apply h
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ LiftP (PredLast α p)
    (abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) })
[PROOFSTEP]
rw [MvQPF.liftP_iff]
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ ∃ a_1 f_1,
    abs { fst := a, snd := MvPFunctor.appendContents (P F) f' fun x => Quotient.mk (wSetoid α) (f x) } =
        abs { fst := a_1, snd := f_1 } ∧
      ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a_1 i), PredLast α p (f_1 i j)
[PROOFSTEP]
refine' ⟨_, _, rfl, _⟩
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
⊢ ∀ (i : Fin2 (n + 1)) (j : MvPFunctor.B (P F) a i),
    PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
[PROOFSTEP]
intro i j
[GOAL]
case a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
i : Fin2 (n + 1)
j : MvPFunctor.B (P F) a i
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) i j)
[PROOFSTEP]
cases i
[GOAL]
case a.fz
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
j : MvPFunctor.B (P F) a Fin2.fz
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) Fin2.fz j)
[PROOFSTEP]
apply ih
[GOAL]
case a.fs
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
p : Fix F α → Prop
h : ∀ (x : F (α ::: Fix F α)), LiftP (PredLast α p) x → p (mk x)
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), p (Quot.mk Setoid.r (f i))
a✝ : Fin2 (Nat.add n 0)
j : MvPFunctor.B (P F) a (Fin2.fs a✝)
⊢ PredLast α p (MvPFunctor.appendContents (P F) f' (fun x => Quotient.mk (wSetoid α) (f x)) (Fin2.fs a✝) j)
[PROOFSTEP]
trivial
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
⊢ ∀ {α : TypeVec n} (x : Fix F α), (fun {α} α_1 => Quot.mk WEquiv α_1) ((fun {α} α_1 => fixToW α_1) x) = x
[PROOFSTEP]
intro α
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
⊢ ∀ (x : Fix F α), (fun {α} α_1 => Quot.mk WEquiv α_1) ((fun {α} α_1 => fixToW α_1) x) = x
[PROOFSTEP]
apply Quot.ind
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
⊢ ∀ (a : MvPFunctor.W (P F) α),
    (fun {α} α_1 => Quot.mk WEquiv α_1) ((fun {α} α_1 => fixToW α_1) (Quot.mk Setoid.r a)) = Quot.mk Setoid.r a
[PROOFSTEP]
intro a
[GOAL]
case mk
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
a : MvPFunctor.W (P F) α
⊢ (fun {α} α_1 => Quot.mk WEquiv α_1) ((fun {α} α_1 => fixToW α_1) (Quot.mk Setoid.r a)) = Quot.mk Setoid.r a
[PROOFSTEP]
apply Quot.sound
[GOAL]
case mk.a
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α : TypeVec n
a : MvPFunctor.W (P F) α
⊢ WEquiv ((fun {α} α_1 => fixToW α_1) (Quot.mk Setoid.r a)) a
[PROOFSTEP]
apply wrepr_equiv
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (MvPFunctor.wp (P F)) α),
    (fun {α} α_1 => Quot.mk WEquiv α_1) (f <$$> p) = f <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) p
[PROOFSTEP]
intro α β g x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α β : TypeVec n
g : α ⟹ β
x : MvPFunctor.Obj (MvPFunctor.wp (P F)) α
⊢ (fun {α} α_1 => Quot.mk WEquiv α_1) (g <$$> x) = g <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) x
[PROOFSTEP]
conv =>
  rhs
  dsimp [MvFunctor.map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α β : TypeVec n
g : α ⟹ β
x : MvPFunctor.Obj (MvPFunctor.wp (P F)) α
| (fun {α} α_1 => Quot.mk WEquiv α_1) (g <$$> x) = g <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) x
[PROOFSTEP]
  rhs
  dsimp [MvFunctor.map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α β : TypeVec n
g : α ⟹ β
x : MvPFunctor.Obj (MvPFunctor.wp (P F)) α
| (fun {α} α_1 => Quot.mk WEquiv α_1) (g <$$> x) = g <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) x
[PROOFSTEP]
  rhs
  dsimp [MvFunctor.map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α β : TypeVec n
g : α ⟹ β
x : MvPFunctor.Obj (MvPFunctor.wp (P F)) α
| (fun {α} α_1 => Quot.mk WEquiv α_1) (g <$$> x) = g <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) x
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α✝ α β : TypeVec n
g : α ⟹ β
x : MvPFunctor.Obj (MvPFunctor.wp (P F)) α
| g <$$> (fun {α} α_1 => Quot.mk WEquiv α_1) x
[PROOFSTEP]
dsimp [MvFunctor.map]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
⊢ x = y.fst
[PROOFSTEP]
symm
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
⊢ y.fst = x
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
⊢ (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst = x
[PROOFSTEP]
apply Fix.ind_rec _ id _ x
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
⊢ ∀ (x : F (α ::: Fix F α)),
    (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
          x =
        (TypeVec.id ::: _root_.id) <$$> x →
      (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) (mk x)).fst = _root_.id (mk x)
[PROOFSTEP]
intro x' ih
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) (mk x')).fst = _root_.id (mk x')
[PROOFSTEP]
rw [Fix.rec_eq]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ {
        fst :=
          mk
            ((TypeVec.id ::: Sigma.fst) <$$>
              (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x'),
        snd :=
          g
            ((TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$>
              x') }.fst =
    _root_.id (mk x')
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    (TypeVec.id ::: _root_.id) <$$> x'
⊢ mk
      ((TypeVec.id ::: Sigma.fst) <$$>
        (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x') =
    mk x'
[PROOFSTEP]
simp [appendFun_id_id] at ih 
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
⊢ mk
      ((TypeVec.id ::: Sigma.fst) <$$>
        (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x') =
    mk x'
[PROOFSTEP]
congr
[GOAL]
case e_x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
⊢ (TypeVec.id ::: Sigma.fst) <$$>
      (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    x'
[PROOFSTEP]
conv =>
  rhs
  rw [← ih]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
| (TypeVec.id ::: Sigma.fst) <$$>
      (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    x'
[PROOFSTEP]
  rhs
  rw [← ih]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
| (TypeVec.id ::: Sigma.fst) <$$>
      (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    x'
[PROOFSTEP]
  rhs
  rw [← ih]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
| (TypeVec.id ::: Sigma.fst) <$$>
      (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    x'
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
| x'
[PROOFSTEP]
rw [← ih]
[GOAL]
case e_x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
⊢ (TypeVec.id ::: Sigma.fst) <$$>
      (TypeVec.id ::: rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x'
[PROOFSTEP]
rw [MvFunctor.map_map, ← appendFun_comp, id_comp]
[GOAL]
case e_x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
x' : F (α ::: Fix F α)
ih :
  (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x' =
    x'
⊢ (TypeVec.id ::: Sigma.fst ∘ rec fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) <$$> x' =
    (TypeVec.id ::: fun x => (rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x).fst) <$$>
      x'
[PROOFSTEP]
simp only [Function.comp]
[GOAL]
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i => { fst := mk ((TypeVec.id ::: Sigma.fst) <$$> i), snd := g i }) x
this : x = y.fst
⊢ β y.fst = β x
[PROOFSTEP]
rw [this]
