Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ (CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
        CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝) =
    (F.map (α_ x✝² x✝¹ x✝).hom ≫
        CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
          F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)

pp: case h_snd.h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝)

pp: case h_snd
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝)

Tactic:
<;>

Goal state after:
case h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ (CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
        CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝) =
    (F.map (α_ x✝² x✝¹ x✝).hom ≫
        CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
          F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
      fst (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)

case h_snd.h_fst
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      fst (F.obj x✝¹) (F.obj x✝)

case h_snd
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F✝ : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F✝.OplaxMonoidal
inst✝ : PreservesFiniteProducts F✝
F : C ⥤ D
x✝² x✝¹ x✝ : C
⊢ ((CartesianMonoidalCategory.prodComparison F (x✝² ⊗ x✝¹) x✝ ≫
          CartesianMonoidalCategory.prodComparison F x✝² x✝¹ ▷ F.obj x✝ ≫ (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝) =
    ((F.map (α_ x✝² x✝¹ x✝).hom ≫
          CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
            F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝) ≫
        snd (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝)) ≫
      snd (F.obj x✝¹) (F.obj x✝)