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 : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
⊢ ((unop S).binaryCofan (unop T)).inl.op = S ◁ (terminalOpOfInitial isInitialSelf).from T ≫ (ρ_ S).hom

Tactic:
by

Goal state after:
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
⊢ (f * g).ofConv c = (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (comul c)

Tactic:
by

Goal state after:
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 : WithConv (C →ₐ[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Bialgebra R C
inst✝¹ : Algebra R A
inst✝ : Bialgebra R B
f g : WithConv (C →ₐ[R] A)
h : B →ₐc[R] C
⊢ (f * g).ofConv.comp ↑h = (toConv (f.ofConv.comp ↑h) * toConv (g.ofConv.comp ↑h)).ofConv

Tactic:
by

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)ᵒᵖ
⊢ ((unop S).binaryCofan (unop T)).inr.op = (terminalOpOfInitial isInitialSelf).from S ▷ T ≫ (λ_ T).hom

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Semiring C
inst✝² : Bialgebra R C
inst✝¹ : Algebra R A
inst✝ : Algebra R B
h : A →ₐ[R] B
f g : WithConv (C →ₐ[R] A)
⊢ h.comp (f * g).ofConv = (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv

Tactic:
by

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

Tactic:
by

Goal state after:
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 A
inst✝¹ : Bialgebra R C
inst✝ : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv (f ^ (n + 1)).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ (n + 1)

Tactic:
by

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
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:
by

Goal state after:
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 A
inst✝¹ : Bialgebra R C
inst✝ : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv ↑(f ^ (n + 1)).ofConv = toConv ↑f.ofConv ^ (n + 1)

Tactic:
by

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y = CartesianMonoidalCategory.prodComparison F X Y

Tactic:
by

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✝¹ : 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:
by

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✝¹ : 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:
by

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✝¹ : 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 =
    F.map (α_ x✝² x✝¹ x✝).hom ≫
      CartesianMonoidalCategory.prodComparison F x✝² (x✝¹ ⊗ x✝) ≫
        F.obj x✝² ◁ CartesianMonoidalCategory.prodComparison F x✝¹ x✝

Tactic:
by

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✝¹ : 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:
by

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✝¹ : 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:
by

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✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ a = b

Tactic:
by

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
F : C ⥤ D
inst✝ : F.Monoidal
X : C
⊢ toUnit (F.obj X) ≫ ε F = F.map (toUnit X)

Tactic:
by

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
F : C ⥤ D
X Y Z : C
inst✝ : F.Monoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ (lift (F.map f) (F.map g) ≫ μ F Y Z) ≫ (μIso F Y Z).inv = F.map (lift f g) ≫ (μIso F Y Z).inv

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ ε F = (preservesTerminalIso F).inv

Tactic:
by

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
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ μ F X Y = (prodComparisonIso F X Y).inv

Tactic:
by

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 = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Tactic:
by

Goal state after:
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
⊢ (antipode R) 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = (algebraMap R A) (counit a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = (algebraMap R A) (counit a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = counit a • 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i * (antipode R) (repr.right i) = counit a • 1

Tactic:
by

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
F G : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
α : F ⟶ G
X Y : C
⊢ μ F X Y ≫ α.app (X ⊗ Y) = (α.app X ⊗ₘ α.app Y) ≫ μ G X Y

Tactic:
by

Goal state after:
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
a : A
⊢ counit ((antipode R) a) = counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * (antipode R) ((ℛ R a).right i))

Tactic:
by

Goal state after:
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
a : A
⊢ counit (∑ i ∈ (ℛ R a).index, (ℛ R a).left i * (antipode R) ((ℛ R a).right i)) = counit a

Tactic:
by

Goal state after:
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
a : A
⊢ counit ((antipode R) a) = counit a

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
antipode : A →ₗ[R] A
antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1
id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1
⊢ mul' R A ∘ₗ rTensor A antipode ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
antipode : A →ₗ[R] A
antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1
id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1
⊢ mul' R A ∘ₗ lTensor A antipode ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
mul_antipode_lTensor_comul :
  (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
⊢ (toConv antipode.toLinearMap * toConv LinearMap.id).ofConv = ofConv 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
mul_antipode_lTensor_comul :
  (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
⊢ (toConv LinearMap.id * toConv antipode.toLinearMap).ofConv = ofConv 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f : A ⟶ B
⊢ lift f (f ≫ ι) ≫ μ = toUnit A ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
⊢ LinearMap.mul' S (B ⊗[R] A) ∘ₗ
      LinearMap.rTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul =
    Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f : A ⟶ B
⊢ lift (f ≫ ι) f ≫ μ = toUnit A ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ ↔ lift g f ≫ μ = h

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
⊢ LinearMap.mul' S (B ⊗[R] A) ∘ₗ
      LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul =
    Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift (f ≫ ι) g ≫ μ = h ↔ g = lift f h ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift g (h ≫ ι) ≫ μ ↔ lift f h ≫ μ = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ lift f (g ≫ ι) ≫ μ = h ↔ f = lift h g ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g i : A ⟶ B
h : lift f i ≫ μ = lift g i ≫ μ
⊢ f = g

Tactic:
by

Goal state after:
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
⊢ ι ≫ ι = 𝟙 A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X✝ : C
inst✝¹ : GrpObj G
A B G' X : C
inst✝ : AddGrpObj G'
e : G' ≅ X
⊢ lift (e.inv ≫ AddGrpObj.neg ≫ e.hom) (𝟙 X) ≫ AddMonObj.add = toUnit X ≫ AddMonObj.zero

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X✝ : C
inst✝¹ : GrpObj G
A B G' X : C
inst✝ : AddGrpObj G'
e : G' ≅ X
⊢ lift (𝟙 X) (e.inv ≫ AddGrpObj.neg ≫ e.hom) ≫ AddMonObj.add = toUnit X ≫ AddMonObj.zero

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
G X : C
inst✝ : GrpObj G
A B : C
e : G ≅ X
⊢ lift (e.inv ≫ ι ≫ e.hom) (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
G X : C
inst✝ : GrpObj G
A B : C
e : G ≅ X
⊢ lift (𝟙 X) (e.inv ≫ ι ≫ e.hom) ≫ μ = toUnit X ≫ η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X : C
inst✝¹ : GrpObj G
A✝ B A : C
inst✝ : GrpObj A
⊢ ι ≫ ι = 𝟙 A

Tactic:
by

Goal state after:
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
⊢ CategoryTheory.inv ι = ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ ι = (β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ (ι ⊗ₘ ι) ≫ μ = (β_ A A).hom ≫ μ ≫ ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G : C
inst✝ : GrpObj G
⊢ μ ≫ ι = (ι ⊗ₘ ι) ≫ (β_ G G).hom ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X : C
inst✝¹ : GrpObj G
A✝ B A : C
inst✝ : GrpObj A
f : 𝟙_ C ⟶ A
⊢ (lift (𝟙 A) (toUnit A ≫ f) ≫ μ) ≫ lift (𝟙 A) (toUnit A ≫ f ≫ ι) ≫ μ = 𝟙 A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X : C
inst✝¹ : GrpObj G
A✝ B A : C
inst✝ : GrpObj A
f : 𝟙_ C ⟶ A
⊢ (lift (𝟙 A) (toUnit A ≫ f ≫ ι) ≫ μ) ≫ lift (𝟙 A) (toUnit A ≫ f) ≫ μ = 𝟙 A

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ μ ▷ A ≫ μ = ((α_ A A A).hom ≫ A ◁ μ) ≫ μ

Tactic:
by

Goal state after: