-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{w, u₂} D
F : Functor.{v, w, u, u₂} C D
A A' B B' : C
inst_2 : HasBinaryProduct.{v, u} A B
inst_3 : HasBinaryProduct.{v, u} A' B'
inst_4 : HasBinaryProduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryProduct.{w, u₂} (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
rw :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
rw₁ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prod.lift (F.map prod.fst) (F.map prod.snd))
      (prod.map (F.map f) (F.map g)))
rw₂ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ F.map g))
rw₃ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ F.map g))
rw₄ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g))
      (prod.lift (F.map prod.fst) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
rw₅ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (prod.lift (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.fst))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
rw₆ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (prod.lift (F.map (CategoryStruct.comp (Y := prod.{v, u} A' B') (prod.map f g) prod.fst))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
rw₇ :
  Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (prod.lift (F.map (prod.fst ≫ f))
      (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (F.map prod.snd)))
    (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
⊢ Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (prod.{v, u} A' B')) (F.map (prod.map f g)) (prodComparison F A' B'))
    (CategoryStruct.comp (Y := prod.{w, u₂} (F.obj A) (F.obj B)) (prodComparison F A B) (prod.map (F.map f) (F.map g)))
have rw₈ : Eq (α := F.obj (prod.{v, u} A B) ⟶ prod.{w, u₂} (F.obj A') (F.obj B'))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map (CategoryStruct.comp (Y := prod.{v, u} A' B') (prod.map f g) prod.snd)))
  (prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g)))
Tactic: rw [prodComparison, prodComparison, prod.lift_map, ← F.map_comp, ← F.map_comp, prod.comp_lift, ←
    F.map_comp, prod.map_fst, ← F.map_comp, prod.map_snd]