-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h :
  Eq (α := F (α ::: (P F).W α))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))
abs :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x))
abs₁ :
  MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
abs₂ :
  map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
      (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    MvQPF.abs (F := F) (α := β ::: (P F).W β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
        (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g)) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
abs₃ :
  map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
      (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₀ f'₀ f₀)) =
    map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
      (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
      (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
⊢ Eq (α := F (β ::: (P F).W β))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
        (P F).wMap (α := α) (β := β) g (f₀ x)))
    (MvQPF.abs (F := F) (α := β ::: (P F).W β)
      ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
        (P F).wMap (α := α) (β := β) g (f₁ x)))
have abs₄ : map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
    (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁))) =
  map (F := F) (α := α ::: (P F).W α) (β := β ::: (P F).W β)
    (appendFun (α := α) (α' := β) g ((P F).wMap (α := α) (β := β) g))
    (MvQPF.abs (F := F) (α := α ::: (P F).W α) ((P F).objAppend1 (α := α) a₁ f'₁ f₁))
Tactic: rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]