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)
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)
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
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)
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)
rw [this]
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)
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)
apply Quot.sound
no goals
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)
apply wrepr_equiv
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))
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))
apply Quot.sound
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)))
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))
apply wEquiv.abs'
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)))
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)))
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
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 }
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)))
conv =>
  rhs
  rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
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
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 }
congr 2
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
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
rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
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)
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
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
no goals
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)
rfl