mathlib-initiative/mathlib-tactics huggingface dataset:
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ R.X ◁ (α_ P.X S.X Q.X).hom ≫ (α_ R.X P.X (S.X ⊗ Q.X)).inv ≫ P.actLeft ▷ (S.X ⊗ Q.X) ≫ P.X ◁ Q.actLeft =
    ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X) ≫
      (α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ pushout.inl (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
        (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
      Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    pushout.inl (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
        (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
      Arrow.Hom.left ((ρ_ X).hom ▷ Y)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ Arrow.Hom.right ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) = Arrow.Hom.right ((ρ_ X).hom ▷ Y)

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)

Tactic:
· simp [← comp_whiskerRight_assoc]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ pushout.inl (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    pushout.inl (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ Arrow.Hom.right ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    Arrow.Hom.right ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
w₃ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)))) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
x✝ : (coyoneda.obj (Opposite.op d)).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
⊢ (ConcreteCategory.hom
          ((↾fun f ↦ R.map ((adj.homEquiv d (L.obj ((ihom d').obj (R.obj c)))).symm f)) ≫
            (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c))))).toFun
      x✝ =
    (ConcreteCategory.hom (𝟙 ((coyoneda.obj (Opposite.op d)).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))))).toFun x✝

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app Y.left) (((curriedTensor C).obj X.left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    pushout.inr (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ Arrow.Hom.right ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    Arrow.Hom.right (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
w₃ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c))) =
    ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d))) (R.obj c)).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)))) ∘
        ⇑((ihom.adjunction d').homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d))) (R.obj c))
w₄ :
  (coyoneda.map (adj.unit.app d).op).app ((ihom d').obj (R.obj c)) ≫
      (coyoneda.obj (Opposite.op d)).map (adj.unit.app ((ihom d').obj (R.obj c))) =
    (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).map (adj.unit.app ((ihom d').obj (R.obj c))) ≫
      (coyoneda.map (adj.unit.app d).op).app ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
f : (coyoneda.obj (Opposite.op ((L ⋙ R).obj d))).obj ((L ⋙ R).obj ((ihom d').obj (R.obj c)))
⊢ f = R.map (R.preimage f)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalLeftAction C D
M : C
inst✝¹ : MonObj M
X : D
inst✝ : ModObj M X
⊢ M ⊴ₗ γ ≫ γ = (αₗ M M X).inv ≫ μ ⊵ₗ X ≫ γ

Tactic:
simp

Goal state after:
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (P.X ⊗ S.X) ◁ Q.actRight ≫ P.actRight ▷ Q.X =
    ((α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (α_ P.X S.X (Q.X ⊗ T.X)).hom ≫ P.X ◁ S.X ◁ Q.actRight ≫ (α_ P.X S.X Q.X).inv) ≫
      P.actRight ▷ Q.X

Tactic:
simp

Goal state after:
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X S.X Q.X).hom ▷ T.X ≫
      (α_ P.X (S.X ⊗ Q.X) T.X).hom ≫ P.X ◁ (α_ S.X Q.X T.X).hom ≫ P.X ◁ (S.X ◁ Q.actRight ≫ Q.actLeft) =
    (α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (α_ P.X S.X (Q.X ⊗ T.X)).hom ≫ P.X ◁ S.X ◁ Q.actRight ≫ P.X ◁ Q.actLeft

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CartesianMonoidalCategory C
G H K : C
inst✝² : GrpObj G
inst✝¹ : GrpObj H
inst✝ : GrpObj K
φ : H ⟶ G
⊢ ∃ ψ, ψ ≫ η = G ◁ η ≫ conj G

Tactic:
use toUnit _

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CartesianMonoidalCategory C
G H K : C
inst✝² : GrpObj G
inst✝¹ : GrpObj H
inst✝ : GrpObj K
φ : H ⟶ G
⊢ toUnit (G ⊗ 𝟙_ C) ≫ η = G ◁ η ≫ conj G
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ Normal φ ↔ ∀ (X : C), (monoidHom φ X).range.Normal

Tactic:
isNormalHom_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G) ↔ ∀ (X : C), (monoidHom φ X).range.Normal
Module: Mathlib.CategoryTheory.Monoidal.Mod

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
⊢ M ◁ γ ≫ γ = (α_ M M X).inv ≫ μ ▷ X ≫ γ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalLeftAction C D
A : C
inst✝ : MonObj A
M : Mod D A
⊢ A ⊴ₗ γ ≫ γ = (αₗ A A M.X).inv ≫ μ ⊵ₗ M.X ≫ γ

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ (η ≫ f) ⊵ₗ M ≫ γ = (λₗ M).hom

Tactic:
rw [IsMonHom.one_hom, ModObj.one_smul]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
X : C
g : X ⟶ G
h : X ⟶ H
⊢ h ≫ φ ∈ (monoidHom φ X).range

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
G H : C
inst✝⁴ : GrpObj G
inst✝³ : GrpObj H
φ : H ⟶ G
inst✝² : IsMonHom φ
P : C
p : G ⟶ P
inst✝¹ : GrpObj P
inst✝ : IsMonHom p
h : IsPullback φ (toUnit H) p η
⊢ h.lift (G ◁ φ ≫ conj G) (toUnit (G ⊗ H)) ⋯ ≫ φ = G ◁ φ ≫ conj G

Tactic:
simp

Goal state after:
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X Q.X (𝟙_ C)).hom ≫
      P.X ◁ (ρ_ Q.X).hom ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ 𝟙_ C ≫
      (ρ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
x✝ : (fun X ↦ X) ((coyoneda.obj (Opposite.op (L.obj ((L ⋙ R).obj d ⊗ d')))).obj c)
⊢ (ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) x✝ =
    (⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
        ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
          ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c))
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
x✝ : (tensorLeft ((L ⋙ R).obj d)).obj (Opposite.unop (Opposite.op d')) ⟶ R.obj c
⊢ (ConcreteCategory.hom (↾fun g ↦ g ≫ (pre (adj.unit.app d)).app (R.obj c)))
      ((ihom.adjunction (R.obj (L.obj d))).unit.app d' ≫ (ihom (R.obj (L.obj d))).map x✝) =
    (ihom.adjunction d).unit.app d' ≫
      (ihom d).map ((ConcreteCategory.hom ((yoneda.obj (R.obj c)).map ((adj.unit.app d).op ▷ Opposite.op d'))) x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) =
    ⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv d' (R.obj c)).symm
⊢ Function.Bijective
      (⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
        ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
          ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv d' (R.obj c)).symm) ↔
    Function.Bijective
      (⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
        ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
          ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c))

Tactic:
simp

Goal state after:
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X Q.X (T.X ⊗ T.X)).hom ≫
      (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ (P.X ⊗ Q.X) T.X T.X).inv ≫
      (α_ P.X Q.X T.X).hom ▷ T.X ≫
        (P.X ◁ Q.actRight) ▷ T.X ≫
          (α_ P.X Q.X T.X).hom ≫
            P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
simp

Goal state after: