mathlib-initiative/mathlib-tactics huggingface dataset:
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.map (toUnit X ▷ Y) ≫ δ F (𝟙_ C) Y ≫ snd (F.obj (𝟙_ C)) (F.obj Y) = F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom

Tactic:
]

Goal state after:
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.map (toUnit X ▷ Y) ≫ δ F (𝟙_ C) Y ≫ snd (F.obj (𝟙_ C)) (F.obj Y) = F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom
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)
⊢ toConv (h.toLinearMap ∘ₗ (toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap).ofConv) =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap

Tactic:
]

Goal state after:
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)
⊢ toConv (h.toLinearMap ∘ₗ (toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap).ofConv) =
    toConv (toConv (h.comp f.ofConv) * toConv (h.comp g.ofConv)).ofConv.toLinearMap
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case δ
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
x✝¹ x✝ : C
⊢ CartesianMonoidalCategory.prodComparison F x✝¹ x✝ = CartesianMonoidalCategory.prodComparison F x✝¹ x✝

Tactic:
]

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) ≫ (εIso F).inv = F.map (toUnit X) ≫ (εIso F).inv

Tactic:
]

Goal state after:
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) ≫ (εIso F).inv = F.map (toUnit X) ≫ (εIso F).inv
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:
]

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

Goal state after:
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
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)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv

Tactic:
]

Goal state after:
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)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv
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
⊢ (Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    (Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv

Tactic:
]

Goal state after:
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
⊢ (Functor.Monoidal.μIso F X Y).inv ≫ (μ F X Y ≫ α.app (X ⊗ Y)) ≫ (Functor.Monoidal.μIso G X Y).inv =
    (Functor.Monoidal.μIso F X Y).inv ≫ ((α.app X ⊗ₘ α.app Y) ≫ μ G X Y) ≫ (Functor.Monoidal.μIso G X Y).inv
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 ι
⊢ (algebraMap R A) (counit a) = (algebraMap R A) (counit a)

Tactic:
]

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
this : lift f (f ≫ ι) ≫ μ = toUnit A ≫ η
⊢ lift f (f ≫ ι) ≫ μ = toUnit A ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f : A ⟶ B
this : lift f (f ≫ ι) ≫ μ = toUnit A ≫ η
⊢ lift f (f ≫ ι) ≫ μ = toUnit A ≫ η
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
this : lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
]

Goal state after:
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
this : lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
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
this : lift (f ≫ ι) f ≫ μ = toUnit A ≫ η
⊢ lift (f ≫ ι) f ≫ μ = toUnit A ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f : A ⟶ B
this : lift (f ≫ ι) f ≫ μ = toUnit A ≫ η
⊢ lift (f ≫ ι) f ≫ μ = toUnit A ≫ η
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
this : lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
]

Goal state after:
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
this : lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
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
⊢ g = lift f h ≫ μ ↔ g = lift f h ≫ μ

Tactic:
]

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 h g ≫ μ ↔ f = lift h g ≫ μ

Tactic:
]

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 : f = g
⊢ f = g

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g i : A ⟶ B
h : f = g
⊢ f = g
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
⊢ lift (ι ≫ ι) ι ≫ μ = lift (ι ≫ ι) ι ≫ μ

Tactic:
]

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

Tactic:
]

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
⊢ lift (μ ≫ ι) (μ ≫ 𝟙 A) ≫ μ = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ lift (μ ≫ ι) (μ ≫ 𝟙 A) ≫ μ = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ
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
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) μ ≫ μ) ≫ μ

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) μ ≫ μ) ≫ μ
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
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (𝟙 (A ⊗ A) ≫ μ) ≫ μ) ≫ μ

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (𝟙 (A ⊗ A) ≫ μ) ≫ μ) ≫ μ
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
⊢ toUnit (A ⊗ A) ≫ η = toUnit (A ⊗ A) ≫ η

Tactic:
]

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
⊢ (ι ⊗ₘ ι) ≫ μ = (ι ⊗ₘ ι) ≫ μ

Tactic:
]

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
s : PullbackCone μ μ
⊢ s.fst ≫ fst A A = s.fst ≫ fst A A

Tactic:
]

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
s : PullbackCone μ μ
⊢ s.snd ≫ μ = s.snd ≫ μ

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Parametrized

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
⊢ adj₂.homEquiv ((adj₂.adj Y₁).counit.app X₃) ≫ (G.map f.op).app X₃ =
    (G.map f.op).app X₃ ≫ adj₂.homEquiv ((adj₂.adj X₁).counit.app X₃)

Tactic:
]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₃ : C₃
⊢ adj₂.homEquiv ((adj₂.adj Y₁).counit.app X₃) ≫ (G.map f.op).app X₃ =
    (G.map f.op).app X₃ ≫ adj₂.homEquiv ((adj₂.adj X₁).counit.app X₃)
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
s : PullbackCone μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ s.snd ≫ snd A A = s.snd ≫ snd A A

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ (antipode R) a * (antipode R) b = (antipode R) a * (antipode R) b

Tactic:
]

Goal state after:
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
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
]

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv (antipode R)).ofConv ((ℛ R c).left i) * (toConv id).ofConv ((ℛ R c).right i) =
    (ofConv 1) c
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A
⊢ m ≫ fst (A ⊗ A) A ≫ snd A A = lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ

Tactic:
]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A
⊢ m ≫ fst (A ⊗ A) A ≫ snd A A = lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ
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
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
]

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A
⊢ lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A

Tactic:
]

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
h : m ≫ fst (A ⊗ A) A ≫ fst A A = s.snd ≫ fst A A
this : lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A
⊢ lift (s.snd ≫ fst A A) (m ≫ fst (A ⊗ A) A ≫ snd A A) ≫ μ = s.fst ≫ fst A A
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
⊢ δ ∘ₗ ofConv 1 = δ ∘ₗ ofConv 1

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ lift ι (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ lift ι (𝟙 X) ≫ μ = toUnit X ≫ η
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⁻¹ * f =
    toConv
      ((lmul' R).comp
        ((Algebra.TensorProduct.map (f.ofConv.comp (antipodeAlgHom R A)) (f.ofConv.comp (AlgHom.id R A))).comp
          (comulAlgHom R A)))

Tactic:
]

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)
⊢ f⁻¹ * f =
    toConv
      ((lmul' R).comp
        ((Algebra.TensorProduct.map (f.ofConv.comp (antipodeAlgHom R A)) (f.ofConv.comp (AlgHom.id R A))).comp
          (comulAlgHom R A)))
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 : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : (yoneda.obj G).obj X
⊢ 1 = 1

Tactic:
]

Goal state after:
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)
⊢ (toConv
          (f.ofConv.comp
            ((lmul' R).comp
              ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp
                (comulAlgHom R A))))).ofConv.toLinearMap =
    (ofConv 1).toLinearMap

Tactic:
]

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)
⊢ (toConv
          (f.ofConv.comp
            ((lmul' R).comp
              ((Algebra.TensorProduct.map (antipodeAlgHom R A) (AlgHom.id R A)).comp
                (comulAlgHom R A))))).ofConv.toLinearMap =
    (ofConv 1).toLinearMap
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:
]

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)
⊢ f.ofConv.toLinearMap ∘ₗ ofConv 1 = ofConv 1
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A)).ofConv.toLinearMap * toConv (toConv (AlgHom.id R A)).ofConv.toLinearMap = 1

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A)).ofConv.toLinearMap * toConv (toConv (AlgHom.id R A)).ofConv.toLinearMap = 1
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ (ihom A).map g = (ihom A).map g

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X Y : C
g : A ⊗ Y ⟶ X
⊢ f ▷ Y ≫ g = f ▷ Y ≫ g

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X Y : C
inst✝¹ : Closed A
inst✝ : Closed B
f : Y ⟶ (ihom A).obj X
g : B ⟶ A
⊢ f ≫ (pre g).app X = f ≫ (pre g).app X

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A : C
inst✝ : Closed A
⊢ (conjugateEquiv (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A : C
inst✝ : Closed A
⊢ (conjugateEquiv (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)