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

Goal state before:
pp: case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ f ▷ A ≫ B ◁ (𝒮 ≫ f) ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hac
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ f ▷ A ≫ B ◁ (𝒮 ≫ f) ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ A ◁ ε ≫ 𝒮 ▷ 𝟙_ C ≫ ε ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : Δ ≫ A ◁ ε ≫ 𝒮 ▷ 𝟙_ C ≫ ε ▷ 𝟙_ C ≫ (λ_ (𝟙_ C)).hom = ε ≫ η ≫ ε
⊢ 𝒮 ≫ ε = ε
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ 𝒮 ▷ A ≫ (((A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      A ◁ Δ ≫
        A ◁ A ◁ Δ ≫
          A ◁ A ◁ 𝒮 ▷ A ≫ (((A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ ε ≫ (ρ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η = ε ≫ (λ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ ε ≫ (ρ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η = ε ≫ (λ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (𝒮 ≫ Δ) ▷ A ≫ (A ⊗ A) ◁ Δ ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ Δ ▷ A ≫ (A ⊗ A) ◁ (Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)) ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ Δ ▷ A ≫ (A ⊗ A) ◁ (Δ ≫ (β_ A A).hom ≫ (𝒮 ⊗ₘ 𝒮)) ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (((α_ P.X (Q.X ⊗ T.X) L.X).inv ≫ (α_ P.X Q.X T.X).inv ▷ L.X ≫ ((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ▷ L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    P.X ◁ ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (((α_ P.X (Q.X ⊗ T.X) L.X).inv ≫ (α_ P.X Q.X T.X).inv ▷ L.X ≫ ((α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight) ▷ L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    P.X ◁ ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X (Q.X ⊗ T.X) L.X).inv ≫
      (α_ P.X Q.X T.X).inv ▷ L.X ≫
        (((α_ (P.X ⊗ Q.X) T.X L.X).hom ≫
              coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ L.X)) ≫
            coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    (((P.X ◁ (α_ Q.X T.X L.X).hom ≫ P.X ◁ Q.X ◁ L.actLeft) ≫ (α_ P.X Q.X L.X).inv) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
          coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)

Tactic:
slice_rhs 2 3 => rw [associator_inv_naturality_right]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X (Q.X ⊗ T.X) L.X).inv ≫
      (α_ P.X Q.X T.X).inv ▷ L.X ≫
        (((α_ (P.X ⊗ Q.X) T.X L.X).hom ≫
              coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ L.X)) ≫
            coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
              coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) =
    P.X ◁ (α_ Q.X T.X L.X).hom ≫
      (((α_ P.X Q.X (T.X ⊗ L.X)).inv ≫ (P.X ⊗ Q.X) ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X) ≫
        coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
          ((α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X L.X).hom ≫
            coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            A ◁ (α_ A A A).hom ≫
              (α_ A A (A ⊗ A)).inv ≫
                ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                  (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ A) ◁ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            A ◁ (α_ A A A).hom ≫
              (α_ A A (A ⊗ A)).inv ≫
                ((α_ A A (A ⊗ A)).hom ≫ A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                  (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            A ◁ (β_ A A).hom ▷ A ≫
              A ◁ (α_ A A A).hom ≫
                ((((((A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫ (α_ (A ⊗ A) A A).inv) ≫
                        (α_ A A A).hom ▷ A) ≫
                      (A ◁ μ) ▷ A) ≫
                    μ ▷ A) ≫
                  μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            A ◁ (β_ A A).hom ▷ A ≫
              A ◁ (α_ A A A).hom ≫
                ((((((A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫ (α_ (A ⊗ A) A A).inv) ≫
                        (α_ A A A).hom ▷ A) ≫
                      (A ◁ μ) ▷ A) ≫
                    μ ▷ A) ≫
                  μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (α_ A A A).hom ≫
        ((((((A ◁ (β_ A A).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (A ◁ 𝒮 ≫ 𝒮 ▷ A)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (α_ A A A).hom ≫
        ((((((A ◁ (β_ A A).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (A ◁ 𝒮 ≫ 𝒮 ▷ A)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (α_ A A A).hom ≫ ((A ◁ A ◁ ε ≫ A ◁ (β_ A (𝟙_ C)).hom) ≫ A ◁ (λ_ A).hom) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (α_ A A A).hom ≫ ((A ◁ A ◁ ε ≫ A ◁ (β_ A (𝟙_ C)).hom) ≫ A ◁ (λ_ A).hom) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (A ⊗ A) ◁ ε ≫ μ ▷ 𝟙_ C ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (A ⊗ A) ◁ ε ≫ μ ▷ 𝟙_ C ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ (μ ≫ 𝒮) ▷ (A ⊗ A) ≫ A ◁ μ ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ (𝒮 ≫ 𝒮) ▷ A ≫ A ◁ 𝒮 ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ μ ≫ 𝒮 = ε ≫ η

Tactic:
]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ μ ≫ 𝒮 = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = ε ≫ η

Tactic:
]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = ε ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = x

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ x * (y + z) = (Hom.hom μ) (x ⊗ₜ[R] (y + z))

Tactic:
]

Goal state after:
case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ x * (y + z) = (Hom.hom μ) (x ⊗ₜ[R] (y + z))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) ((x + y) ⊗ₜ[R] z)

Tactic:
]

Goal state after:
case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) ((x + y) ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
h : (Hom.hom η) (x • y) = (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (x ⊗ₜ[R] (ConcreteCategory.hom η) y)
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y : R
h : (Hom.hom η) (x • y) = (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (x ⊗ₜ[R] (ConcreteCategory.hom η) y)
⊢ (Hom.hom η).toFun (x * y) = (Hom.hom η).toFun x * (Hom.hom η).toFun y
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (1, x).1 • LinearMap.id (1, x).2 = 1 • x

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (1, x).1 • LinearMap.id (1, x).2 = 1 • x
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (LinearMap.id (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A))))
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (LinearMap.id (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A))))
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (x, 1).2 • LinearMap.id (x, 1).1 = 1 • x

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (x, 1).2 • LinearMap.id (x, 1).1 = 1 • x
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))