-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x x_1 x_2 : C
h_fst :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ⟶ F.obj x)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
      (CartesianMonoidalCategory.prodComparison F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫
        CartesianMonoidalCategory.prodComparison F x x_1 ▷ F.obj x_2 ≫ Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2)))
      (fst (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
      (F.map (Iso.hom (α_ x x_1 x_2)) ≫
        CartesianMonoidalCategory.prodComparison F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ≫
          F.obj x ◁ CartesianMonoidalCategory.prodComparison F x_1 x_2)
      (fst (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
    (CartesianMonoidalCategory.prodComparison F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫
      CartesianMonoidalCategory.prodComparison F x x_1 ▷ F.obj x_2 ≫ Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2)))
    (F.map (Iso.hom (α_ x x_1 x_2)) ≫
      CartesianMonoidalCategory.prodComparison F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ≫
        F.obj x ◁ CartesianMonoidalCategory.prodComparison F x_1 x_2)
have h_snd : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ⟶ F.obj x_1)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
    ((CartesianMonoidalCategory.prodComparison F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫
        CartesianMonoidalCategory.prodComparison F x x_1 ▷ F.obj x_2 ≫ Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2))) ≫
      snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
    (fst (F.obj x_1) (F.obj x_2)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
      (F.map (Iso.hom (α_ x x_1 x_2)) ≫
        CartesianMonoidalCategory.prodComparison F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ≫
          F.obj x ◁ CartesianMonoidalCategory.prodComparison F x_1 x_2)
      (snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
    (fst (F.obj x_1) (F.obj x_2)))
Tactic: ext