-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
a₁ :
  Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (repr (F := F) (α := α ::: (P F).W α)
            (abs (F := F) (α := α ::: (P F).W α)
              (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
                  ((P F).appendContents (α := α) f' f))))))))
    (abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
a₂ :
  Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (repr (F := F) (α := α ::: (P F).W α)
        (abs (F := F) (α := α ::: (P F).W α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
    (abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
a₃ :
  Eq.{u + 1} (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (repr (F := F) (α := α ::: (P F).W α)
        (abs (F := F) (α := α ::: (P F).W α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
    (abs (F := F) (α := α ::: (P F).W α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
a₄ a₅ :
  Eq.{u + 1} (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
    (abs (F := F) (α := α ::: (P F).W α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
⊢ abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))) =
    abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f)))))

Tactic:
rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]

Premises used: MvPFunctor.wDest'_wMk', MvQPF.abs_repr, MvQPF.wrepr_wMk, MvQPF.P