mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      fst (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      fst (F.obj y) (F.obj z)

pp: case h_snd
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      snd (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      snd (F.obj y) (F.obj z)

Tactic:
<;>

Goal state after:
case h_fst
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      fst (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      fst (F.obj y) (F.obj z)

case h_snd
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z ≫
      snd (F.obj y) (F.obj z) =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z ≫
      snd (F.obj y) (F.obj z)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ ((curriedTensor C ⋙ (Functor.whiskeringRight C C D).obj F).map f ≫ prodComparisonNatTrans F y).app z =
    (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ (Functor.whiskeringLeft C D D).obj F).map f).app z

Tactic:
apply hom_ext <;> simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B)

pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B)

Tactic:
<;>

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B)

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B)
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
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

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
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)

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
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

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
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)).comp
        includeLeft)
      x✝

pp: case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑Y✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom))).comp
        includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)).comp
        includeLeft)
      x✝

case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑Y✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom))).comp
        includeRight)
      x✝
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)).comp
        includeLeft)
      x✝

pp: case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑Z✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom))).comp
        includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)).comp
        includeLeft)
      x✝

case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑Z✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom))).comp
        includeRight)
      x✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case left
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P ((pair X Y).obj { as := WalkingPair.left })

pp: case right
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P ((pair X Y).obj { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case left
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P ((pair X Y).obj { as := WalkingPair.left })

case right
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P ((pair X Y).obj { as := WalkingPair.right })
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: case ha
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)).comp includeLeft) x✝ =
    ((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯).comp includeLeft) x✝

pp: case hb
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯)).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ (((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)).comp includeLeft) x✝ =
    ((Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯).comp includeLeft) x✝

case hb
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c x✝ : C
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯)).comp includeRight) x✝
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
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ fst (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ fst (F.obj Y) (F.obj Z)

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
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ snd (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ snd (F.obj Y) (F.obj Z)

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
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ fst (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ fst (F.obj Y) (F.obj Z)

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
F : C ⥤ D
X Y Z : C
inst✝ : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (F.map (lift f g) ≫ δ F Y Z) ≫ snd (F.obj Y) (F.obj Z) = lift (F.map f) (F.map g) ≫ snd (F.obj Y) (F.obj Z)
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✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ fst (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ fst (F.obj Y✝) (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✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ snd (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ snd (F.obj Y✝) (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✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ fst (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ fst (F.obj Y✝) (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✝ Y✝ : C
f : X✝ ⟶ Y✝
X : C
⊢ (CartesianMonoidalCategory.prodComparison F X✝ X ≫ F.map f ▷ F.obj X) ≫ snd (F.obj Y✝) (F.obj X) =
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X) ≫ snd (F.obj Y✝) (F.obj X)
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✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ fst (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ fst (F.obj X) (F.obj Y✝)

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✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ snd (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ snd (F.obj X) (F.obj Y✝)

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✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ fst (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ fst (F.obj X) (F.obj Y✝)

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✝ Y✝ X : C
g : X✝ ⟶ Y✝
⊢ (CartesianMonoidalCategory.prodComparison F X X✝ ≫ F.obj X ◁ F.map g) ≫ snd (F.obj X) (F.obj Y✝) =
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y✝) ≫ snd (F.obj X) (F.obj Y✝)
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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)

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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)

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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)

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
inst✝² : F.Monoidal
inst✝¹ : G.Monoidal
inst✝ : (F ⋙ G).Monoidal
X Y : C
⊢ (μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y) =
    ((μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv) ≫ snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)