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

Goal state before:
pp: case right.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.right.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                  (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.left } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                  (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                  ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.right } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫
        tensorHom ℬ (𝟙 X) (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right } =
    tensorHom ℬ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (𝟙 Y) ≫
      (ℬ X Y).cone.π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
            ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                  ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
            ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
      (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.left } =
    ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
        ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
            ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
            ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
              ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                  ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
      (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun X {x x_1} g ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_1} f Y ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit,
    rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit }
x✝¹ : C
x✝ : x✝¹ ⟶ 𝟙_ C
⊢ ∀ (j : Discrete PEmpty.{1}), x✝ ≫ 𝒯.cone.π.app j = 𝒯.isLimit.lift (asEmptyCone x✝¹) ≫ 𝒯.cone.π.app j

Tactic:
simp

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
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst X Y = lift (f ≫ g) (f ≫ h) ≫ fst X Y

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y : C
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd X Y = lift (f ≫ g) (f ≫ h) ≫ snd X Y

Tactic:
simp

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
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ fst X Y = 𝟙 (X ⊗ Y) ≫ fst X Y

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ lift (fst X Y) (snd X Y) ≫ snd X Y = 𝟙 (X ⊗ Y) ≫ snd X Y

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (fst (X ⊗ X) X ≫ fst X X) * (α.homEquiv' (fst (X ⊗ X) X ≫ snd X X) * α.homEquiv' (snd (X ⊗ X) X)) =
    α.homEquiv' (fst (X ⊗ X) X ≫ fst X X) *
      (α.homEquiv' ((α_ X X X).hom ≫ snd X (X ⊗ X) ≫ fst X X) * α.homEquiv' ((α_ X X X).hom ≫ snd X (X ⊗ X) ≫ snd X X))

Tactic:
simp

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
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ fst Y Z = lift (f ≫ h) (g ≫ k) ≫ fst Y Z

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ (lift f g ≫ (h ⊗ₘ k)) ≫ snd Y Z = lift (f ≫ h) (g ≫ k) ≫ snd Y Z

Tactic:
simp

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
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ fst X Z = (g ⊗ₘ g') ≫ fst X Z

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') ≫ snd X Z = (g ⊗ₘ g') ≫ snd X Z

Tactic:
simp

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

Goal state before:
pp: case e_a.e_a.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ (lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ fst M (M ⊗ M) = lift f₁ (lift f₂ f₃) ≫ fst M (M ⊗ M)

Tactic:
simp

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

Goal state before:
pp: case h_snd.h_fst
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ fst M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ fst M M

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ snd M (M ⊗ M)) ≫ snd M M = (lift f₁ (lift f₂ f₃) ≫ snd M (M ⊗ M)) ≫ snd M M

Tactic:
simp

Goal state after:
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
X Y Z : C
x✝ : Z ⟶ X ⊗ Y
⊢ (fun f ↦ lift f.1 f.2) ((fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X✝ Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
⊢ φ.unop ≫ 1 = 1

Tactic:
by
        change φ.unop ≫ toUnit _ ≫ η = toUnit _ ≫ η
        rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]

Goal state after:
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
X Y Z : C
x✝ : (Z ⟶ X) × (Z ⟶ Y)
⊢ (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) ((fun f ↦ lift f.1 f.2) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y✝ : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ α.homEquiv' (lift f₁ f₂ ≫ fst X X) * α.homEquiv' (lift f₁ f₂ ≫ snd X X) = α.homEquiv' f₁ * α.homEquiv' f₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommBialgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommBialgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: A : Type u_2
B : Type u_3
f : A ≃ B
x : WithConv B
⊢ (WithConv.congr f).symm x = toConv (f.symm x.ofConv)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝ : AddMonoid A
⊢ ∀ (x y : WithConv A), (WithConv.equiv A).toFun (x + y) = (WithConv.equiv A).toFun x + (WithConv.equiv A).toFun y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝² : AddCommMonoid A
inst✝¹ : Semiring R
inst✝ : Module R A
⊢ ∀ (m : R) (x : WithConv A), (WithConv.addEquiv A).toFun (m • x) = (RingHom.id R) m • (WithConv.addEquiv A).toFun x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Semiring R
inst✝² : Module R A
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
f : A ≃ₗ[R] B
x : WithConv B
⊢ (congrLinearEquiv f).symm x = toConv (f.symm x.ofConv)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (0 * f).ofConv x✝ = (ofConv 0) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (f * 0).ofConv x✝ = (ofConv 0) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R C
inst✝⁴ : CoalgebraStruct R C
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower S A A
s : S
f g : WithConv (C →ₗ[R] A)
⊢ (s • f) • g = s • f • g

Tactic:
by ext c; simp [(ℛ R c).convMul_apply, Finset.smul_sum, smul_mul_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A x✝ : C
⊢ (prodComparisonNatTrans (𝟭 C) A).app x✝ = (𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x y : A
⊢ (toConv (toSpanSingleton R A x) * toConv (toSpanSingleton R A y)).ofConv 1 =
    (toConv (toSpanSingleton R A (x * y))).ofConv 1

Tactic:
simp

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)

Tactic:
simp

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

Goal state before:
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:
simp

Goal state after:
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
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
⊢ ∀ (j : Discrete PEmpty.{1}), P ((Functor.empty C).obj j)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ ((mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ) x✝ =
    (mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : ↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left })))
⊢ x ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R ↑(unop T)) 1

Tactic:
simp

Goal state after: