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

Goal state before:
pp: case mk.id
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
;

Goal state after:
case mk.id
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = X✝.normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝ = (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝

Tactic:
;

Goal state after:
case mk.α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝ = (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝ = ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝

Tactic:
;

Goal state after:
case mk.α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj x✝ = ((X✝.tensor Y✝).tensor Z✝).normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.l_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (unit.tensor X✝).normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
;

Goal state after:
case mk.l_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (unit.tensor X✝).normalizeObj x✝ = X✝.normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.l_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (unit.tensor X✝).normalizeObj x✝

Tactic:
;

Goal state after:
case mk.l_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (unit.tensor X✝).normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.ρ_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor unit).normalizeObj x✝ = X✝.normalizeObj x✝

Tactic:
;

Goal state after:
case mk.ρ_hom
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ (X✝.tensor unit).normalizeObj x✝ = X✝.normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.ρ_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (X✝.tensor unit).normalizeObj x✝

Tactic:
;

Goal state after:
case mk.ρ_inv
C : Type u
X Y X✝ : F C
x✝ : NormalMonoidalObject C
⊢ X✝.normalizeObj x✝ = (X✝.tensor unit).normalizeObj x✝
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp C Y { as := n }).hom = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

Tactic:
;

Goal state after:
case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp C Y { as := n }).hom = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ (normalizeIsoApp C X { as := n }).hom ≫ eqToHom ⋯ = (normalizeIsoApp' C X n).hom ≫ eqToHom ⋯

Tactic:
;

Goal state after:
case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ (normalizeIsoApp C X { as := n }).hom ≫ eqToHom ⋯ = (normalizeIsoApp' C X n).hom ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
⊢ TensorBimod.actRight (P.tensorBimod Q) L ≫ hom P Q L = hom P Q L ▷ U.X ≫ TensorBimod.actRight P (Q.tensorBimod L)

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
⊢ TensorBimod.actRight (P.tensorBimod Q) L ≫ hom P Q L = hom P Q L ▷ U.X ≫ TensorBimod.actRight P (Q.tensorBimod L)
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.actRight ▷ L.X ≫
      (α_ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ 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.actRight ▷ L.X ≫
      (α_ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ 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)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

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

Tactic:
erw [LinearMap.mul'_apply, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, ← Algebra.commutes,
      ← Algebra.smul_def]

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.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
this : HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)
⊢ (c₁.mapBifunctor c₂ (curriedTensor C)).ι.app WalkingParallelPair.one ≫
      (Iso.refl (c₁.mapBifunctor c₂ (curriedTensor C)).pt).hom =
    (c₁.tensor c₂).ι.app WalkingParallelPair.one

Tactic:
;

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
this : HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)
⊢ (c₁.mapBifunctor c₂ (curriedTensor C)).ι.app WalkingParallelPair.one ≫
      (Iso.refl (c₁.mapBifunctor c₂ (curriedTensor C)).pt).hom =
    (c₁.tensor c₂).ι.app WalkingParallelPair.one
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
R S : Mon C
P : Bimod R S
⊢ μ ▷ P.X ≫ P.actLeft = ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ P.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
R S : Mon C
P : Bimod R S
⊢ μ ▷ P.X ≫ P.actLeft = ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫
      coequalizer.desc P.actLeft ⋯ ≫
        (λ_ P.X).inv ≫
          η ▷ P.X ≫
            coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) =
    coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫
      𝟙 (coequalizer ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft))

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫
      coequalizer.desc P.actLeft ⋯ ≫
        (λ_ P.X).inv ≫
          η ▷ P.X ≫
            coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) =
    coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫
      𝟙 (coequalizer ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| R.X ◁ P.actLeft

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| η ▷ (R.X ⊗ P.X)

Tactic:
← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| η ▷ (R.X ⊗ P.X)
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
      (coprod.braiding X (Y ⨿ Z)).hom ≫
        coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) =
    coprod.map (coprod.braiding X Y).hom (𝟙 Z) ≫
      coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
        coprod.map (𝟙 Y) (coprod.braiding X Z).hom

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
      (coprod.braiding X (Y ⨿ Z)).hom ≫
        coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) =
    coprod.map (coprod.braiding X Y).hom (𝟙 Z) ≫
      coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
        coprod.map (𝟙 Y) (coprod.braiding X Z).hom
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
      (coprod.braiding (X ⨿ Y) Z).hom ≫
        coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) =
    coprod.map (𝟙 X) (coprod.braiding Y Z).hom ≫
      coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
        coprod.map (coprod.braiding X Z).hom (𝟙 Y)

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
      (coprod.braiding (X ⨿ Y) Z).hom ≫
        coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) =
    coprod.map (𝟙 X) (coprod.braiding Y Z).hom ≫
      coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
        coprod.map (coprod.braiding X Z).hom (𝟙 Y)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft (regular R) P ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft (regular R) P ≫ hom P = R.X ◁ hom P ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actRight (regular R) P ≫ hom P = hom P ▷ S.X ≫ P.actRight

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actRight (regular R) P ≫ hom P = hom P ▷ S.X ≫ P.actRight
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
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ P.actRight

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
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ P.actRight
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫
          P.X ◁ η ≫
            coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫
          P.X ◁ η ≫
            coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft P (regular S) ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft P (regular S) ≫ hom P = R.X ◁ hom P ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actRight P (regular S) ≫ hom P = hom P ▷ S.X ≫ P.actRight

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actRight P (regular S) ≫ hom P = hom P ▷ S.X ≫ P.actRight
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf✝ : f ∈ (ofHoms f✝).toSet
i : ι
hf : Arrow.mk f.hom = Arrow.mk (f✝ i)
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf✝⟩

Tactic:
obtain rfl : f = _ := hf

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
i : ι
hf : Arrow.mk (f i) ∈ (ofHoms f).toSet
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f i), ⋯⟩) a = ⟨Arrow.mk (f i), hf⟩
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ η.app X✝ ≫ A.map f = η.app Y✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ η.app X✝ ≫ A.map f = η.app Y✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ 𝟙 (𝟙_ D) ≫ η.app Y✝ = η.app Y✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ 𝟙 (𝟙_ D) ≫ η.app Y✝ = η.app Y✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ μ.app X✝ ≫ A.map f = (A.map f ⊗ₘ A.map f) ≫ μ.app Y✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ μ.app X✝ ≫ A.map f = (A.map f ⊗ₘ A.map f) ≫ μ.app Y✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ { hom := A.map (𝟙 X), isMonHom_hom := ⋯ }.hom = (𝟙 (functorObjObj A X)).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ { hom := A.map (𝟙 X), isMonHom_hom := ⋯ }.hom = (𝟙 (functorObjObj A X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)