-- 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 : HasBinaryCoproduct.{v, u} A B
inst_3 : HasBinaryCoproduct.{v, u} A' B'
inst_4 : HasBinaryCoproduct.{w, u₂} (F.obj A) (F.obj B)
inst_5 : HasBinaryCoproduct.{w, u₂} (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
rw :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
rw₁ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprod.desc (F.map coprod.inl) (F.map coprod.inr)))
rw₂ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map f ≫ F.map coprod.inl) (F.map g ≫ F.map coprod.inr))
rw₃ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map g ≫ F.map coprod.inr))
rw₄ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprod.desc (F.map coprod.inl) (F.map coprod.inr))
      (F.map (coprod.map f g)))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
rw₅ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (coprod.desc (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inl) (F.map (coprod.map f g)))
      (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inr) (F.map (coprod.map f g))))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
rw₆ :
  Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (coprod.desc (F.map (CategoryStruct.comp (Y := coprod.{v, u} A B) coprod.inl (coprod.map f g)))
      (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inr) (F.map (coprod.map f g))))
    (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
⊢ Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (coprodComparison F A B) (F.map (coprod.map f g)))
    (CategoryStruct.comp (Y := coprod.{w, u₂} (F.obj A') (F.obj B')) (coprod.map (F.map f) (F.map g))
      (coprodComparison F A' B'))
have rw₇ : Eq (α := coprod.{w, u₂} (F.obj A) (F.obj B) ⟶ F.obj (coprod.{v, u} A' B'))
  (coprod.desc (F.map (f ≫ coprod.inl))
    (CategoryStruct.comp (Y := F.obj (coprod.{v, u} A B)) (F.map coprod.inr) (F.map (coprod.map f g))))
  (coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr)))
Tactic: rw [coprodComparison, coprodComparison, coprod.map_desc, ← F.map_comp, ← F.map_comp,
    coprod.desc_comp, ← F.map_comp, coprod.inl_map, ← F.map_comp, coprod.inr_map]