mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U).symm =
    ((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
          ↑(assoc R R R ↑S ↑U ↑T).symm).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑S) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))

Tactic:
ext

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ ((((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
            ↑(assoc R R R ↑S ↑T ↑U).symm).comp
        includeLeft)
      x✝ =
    ((((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
                ↑(assoc R R R ↑S ↑U ↑T).symm).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑S)
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))).comp
        includeLeft)
      x✝

case hb.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ (((AlgHom.restrictScalars R
                (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
            includeRight).comp
        includeLeft)
      x✝ =
    (((AlgHom.restrictScalars R
                (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                          (AlgHom.id R ↑T)).comp
                      ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                  (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                    (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
            includeRight).comp
        includeLeft)
      x✝

case hb.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                        (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                    ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
              includeRight)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                            (AlgHom.id R ↑T)).comp
                        ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                    (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
              includeRight)).comp
        includeRight)
      x✝
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✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ 1 * f = f

Tactic:
ext

Goal state after:
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✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (1 * f).ofConv x✝ = f.ofConv x✝
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✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
⊢ f * 1 = f

Tactic:
ext

Goal state after:
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✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (f * 1).ofConv x✝ = f.ofConv x✝
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✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid C
inst✝³ : Algebra R A
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
⊢ (mul' R A) ((TensorProduct.comm R A A) ((g.ofConv ⊗ₘ f.ofConv) (δ x))) = (g * f).ofConv x

Tactic:
mul'_comm,

Goal state after:
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✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid C
inst✝³ : Algebra R A
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
f g : WithConv (C →ₗ[R] A)
x : C
⊢ (mul' R A) ((g.ofConv ⊗ₘ f.ofConv) (δ x)) = (g * f).ofConv x
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: 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 : C
⊢ (lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv) = Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯

Tactic:
ext

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: 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 = lift (F.map f) (F.map g)

Tactic:
ext

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: 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 =
    F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y✝ X

Tactic:
ext

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

Tactic:
ext

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: 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✝ : C
⊢ (λ_ (F.obj x✝)).inv =
    F.map (λ_ x✝).inv ≫
      CartesianMonoidalCategory.prodComparison F (𝟙_ C) x✝ ≫ CartesianMonoidalCategory.terminalComparison F ▷ F.obj x✝

Tactic:
ext

Goal state after:
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✝ : C
⊢ (λ_ (F.obj x✝)).inv ≫ snd (𝟙_ D) (F.obj x✝) =
    (F.map (λ_ x✝).inv ≫
        CartesianMonoidalCategory.prodComparison F (𝟙_ C) x✝ ≫
          CartesianMonoidalCategory.terminalComparison F ▷ F.obj x✝) ≫
      snd (𝟙_ D) (F.obj x✝)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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✝ : C
⊢ (ρ_ (F.obj x✝)).inv =
    F.map (ρ_ x✝).inv ≫
      CartesianMonoidalCategory.prodComparison F x✝ (𝟙_ C) ≫ F.obj x✝ ◁ CartesianMonoidalCategory.terminalComparison F

Tactic:
ext

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✝ : C
⊢ (ρ_ (F.obj x✝)).inv ≫ fst (F.obj x✝) (𝟙_ D) =
    (F.map (ρ_ x✝).inv ≫
        CartesianMonoidalCategory.prodComparison F x✝ (𝟙_ C) ≫
          F.obj x✝ ◁ CartesianMonoidalCategory.terminalComparison F) ≫
      fst (F.obj x✝) (𝟙_ D)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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 = (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv

Tactic:
ext

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)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ (εIso F).symm = preservesTerminalIso F

Tactic:
ext

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

Goal state before:
pp: 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✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv =
    ((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv

Tactic:
ext

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✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ ((μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv) ≫ fst (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ 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✝² : BraidedCategory C
inst✝¹ : BraidedCategory D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ ((μ F X Y ≫ F.map (β_ X Y).hom) ≫ (Monoidal.μIso F Y X).inv) ≫ snd (F.obj Y) (F.obj X) =
    (((β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X) ≫ (Monoidal.μIso F Y X).inv) ≫ snd (F.obj Y) (F.obj X)
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ counit ∘ₗ antipode R = counit

Tactic:
ext

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
x✝ : A
⊢ (counit ∘ₗ antipode R) x✝ = counit x✝
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul) 1 =
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit) 1
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ mulRight η = Iso.refl A

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ (mulRight η).hom = (Iso.refl A).hom
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ) = δ ∘ₗ mul' R C

Tactic:
ext

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
x✝¹ x✝ : C
⊢ ((AlgebraTensorModule.curry (mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (δ ∘ₗ mul' R C)) x✝¹) x✝
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ δ ∘ₗ Algebra.linearMap R C = Algebra.linearMap R (C ⊗[R] C)

Tactic:
ext

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ (δ ∘ₗ Algebra.linearMap R C) 1 = (Algebra.linearMap R (C ⊗[R] C)) 1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
⊢ (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)

Tactic:
ext

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

case hb
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
x✝ : A
⊢ ((restrictScalars R ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv))).comp includeRight) x✝ =
    ((restrictScalars R (f.ofConv.comp (lmul' R))).comp includeRight) x✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (f✝ ⊗ₘ g✝).hom.hom = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).hom.hom
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
⊢ f.ofConv.toLinearMap ∘ₗ ofConv 1 = ofConv 1

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring C
inst✝¹ : Bialgebra R C
inst✝ : HopfAlgebra R A
f : WithConv (A →ₐ[R] C)
H : (lmul' R).comp (Algebra.TensorProduct.map f.ofConv f.ofConv) = f.ofConv.comp (lmul' R)
x✝ : A
⊢ (f.ofConv.toLinearMap ∘ₗ ofConv 1) x✝ = (ofConv 1) x✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ x✝¹ x✝ : Grp C
⊢ (α_ x✝¹ (𝟙_ (Grp C)) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom = (ρ_ x✝¹).hom ▷ x✝

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G H H₁ H₂ x✝¹ x✝ : Grp C
⊢ ((α_ x✝¹ (𝟙_ (Grp C)) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).hom.hom = ((ρ_ x✝¹).hom ▷ x✝).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H H₁ H₂ G : Grp C
f : G ⟶ 𝟙_ (Grp C)
⊢ f = homMk' (toUnit G.toMon)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H H₁ H₂ G : Grp C
f : G ⟶ 𝟙_ (Grp C)
⊢ f.hom.hom = (homMk' (toUnit G.toMon)).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ homMk' (fst G.toMon H.toMon) = G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (fst G.toMon H.toMon)).hom.hom =
    (G ◁ (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from H ≫ (ρ_ G).hom).hom.hom
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ homMk' (snd G.toMon H.toMon) = (IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from G ▷ H ≫ (λ_ H).hom

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ (homMk' (snd G.toMon H.toMon)).hom.hom =
    ((IsTerminal.ofUniqueHom (fun G ↦ homMk' (toUnit G.toMon)) ⋯).from G ▷ H ≫ (λ_ H).hom).hom.hom