mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
x y : X
f : x ⟶ y
⊢ ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.right G₁).symm },
                  map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).snd.map
        f ≫
      η.right.app (S.snd.obj y) =
    η.right.app (S.snd.obj x) ≫
      ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).snd.map
        f

Tactic:
by simp

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).hom ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε)

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_forward _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝² : Lifting L W F₁ F₁'
inst✝¹ : Lifting L W F₂ F₂'
inst✝ : HasZeroMorphisms E
⊢ ∀ (X : C), (liftNatTrans L W F₁ F₂ F₁' F₂' 0).app (L.obj X) = NatTrans.app 0 (L.obj X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Preadditive E
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝¹ : Lifting L W F₁ F₁'
inst✝ : Lifting L W F₂ F₂'
τ τ' : F₁ ⟶ F₂
⊢ ∀ (X : C),
    (liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ')).app (L.obj X) =
      (liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ').app (L.obj X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ lift (Over.Hom.left u) (Over.Hom.left v) ⋯ ≫ (binaryFan Y Z).pt.hom = T✝.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.LaxRightLinear C
d : D
c c' : C
⊢ μᵣ F d c ⊵ᵣ c' ≫ μᵣ F (d ⊙ᵣ c) c' ≫ F.map (αᵣ d c c').inv = (αᵣ (F.obj d) c c').inv ≫ μᵣ F d (c ⊗ c')

Tactic:
by
  simpa [-μᵣ_associativity, -μᵣ_associativity_assoc] using
    (αᵣ _ _ _).inv ≫=
      (μᵣ_associativity F d c c').symm =≫
      F.map (αᵣ _ _ _).inv

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : CreatesColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G

Tactic:
by
  have I {A B} (f g : A ⟶ B) [G.IsSplitPair f g] : HasColimit (parallelPair f g ⋙ G) := by
    rw [hasColimit_iff_of_iso (diagramIsoParallelPair.{v₁} _)]
    exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)
  have : HasCoequalizerOfIsSplitPair G := ⟨fun _ _ => hasColimit_of_created (parallelPair _ _) G⟩
  have : PreservesColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩
  have : ReflectsColimitOfIsSplitPair G := ⟨by intros; infer_instance⟩
  exact monadicOfHasPreservesReflectsGSplitCoequalizers adj

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

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 C
inst✝¹ : MonoidalLeftAction C D
x : C
y z : D
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ₗ f ≫ x ⊴ₗ inv f = 𝟙 (x ⊙ₗ y) ∧ x ⊴ₗ inv f ≫ x ⊴ₗ f = 𝟙 (x ⊙ₗ z)

Tactic:
by simp

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

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 C
inst✝¹ : MonoidalLeftAction C D
x y : C
f : x ⟶ y
inst✝ : IsIso f
z : D
⊢ f ⊵ₗ z ≫ inv f ⊵ₗ z = 𝟙 (x ⊙ₗ z) ∧ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (y ⊙ₗ z)

Tactic:
by simp

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

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 C
inst✝¹ : MonoidalRightAction C D
x y : D
f : x ⟶ y
inst✝ : IsIso f
z : C
⊢ f ⊵ᵣ z ≫ inv f ⊵ᵣ z = 𝟙 (x ⊙ᵣ z) ∧ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
by simp

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

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 C
inst✝¹ : MonoidalRightAction C D
x : D
y z : C
f : y ⟶ z
inst✝ : IsIso f
⊢ x ⊴ᵣ f ≫ x ⊴ᵣ inv f = 𝟙 (x ⊙ᵣ y) ∧ x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (x ⊙ᵣ z)

Tactic:
by 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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Arrow.Hom.right (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ (α_ Y₁ Y₂ Y₃).hom) = Arrow.Hom.right ((α_ X₁ X₂ X₃).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ μ ≫ Δ = Δ ≫ (μ ⊗ₘ μ)

Tactic:
by simp

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

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    ((forget C).mapCone (limitCone F c hc)).π.app j =
      (Iso.refl ((forget C).mapCone (limitCone F c hc)).pt).hom ≫ c.π.app j

Tactic:
by simp

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

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
⊢ ∀ (j : J), (η ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j = η ≫ c.π.app j

Tactic:
by simp

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

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
s : Cone F
⊢ ∀ (j : J),
    (μ ≫ hc.lift ((forget C).mapCone s)) ≫ c.π.app j =
      ((hc.lift ((forget C).mapCone s) ⊗ₘ hc.lift ((forget C).mapCone s)) ≫ μ) ≫ c.π.app j

Tactic:
by 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
f : X ⟶ Y
⊢ pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) =
    pushout.inl (((curriedTensor C).map (𝟙_ (Arrow C)).hom).app X.left)
        (((curriedTensor C).obj (𝟙_ (Arrow C)).left).map X.hom) ≫
      Arrow.Hom.left ((λ_ X).hom ≫ f)

Tactic:
by 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
f : X ⟶ Y
⊢ Arrow.Hom.right (𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom) = Arrow.Hom.right ((λ_ X).hom ≫ f)

Tactic:
by 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
f : X ⟶ Y
⊢ pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) =
    pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left ((ρ_ X).hom ≫ f)

Tactic:
by 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
f : X ⟶ Y
⊢ Arrow.Hom.right (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) = Arrow.Hom.right ((ρ_ X).hom ≫ f)

Tactic:
by 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
W X Y Z : Arrow C
⊢ pushout.inl (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
        (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    pushout.inl (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
        (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
by 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
W X Y Z : Arrow C
⊢ Arrow.Hom.right ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    Arrow.Hom.right ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
by 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
W X Y Z : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    (tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
by 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:
by 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:
by 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.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:
by 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:
by 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:
by 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:
by 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:
by 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 : 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:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop ≫ 1 = 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop ≫ 0 = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : RingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 1 ≫ f.hom = 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : RingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 0 ≫ f.hom = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommRingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 1 ≫ f.hom = 1

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommRingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 0 ≫ f.hom = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ diag A ≫ prod.fst = 𝟙 A

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ f = g

Tactic:
← prod.lift_fst f g,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ prod.lift f g ≫ prod.fst = g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B)).symm (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)) =
    prodComparison (reflector i) A B

Tactic:
by
  simp only [bijection, Equiv.trans_def, curriedTensor_obj_obj, Equiv.symm_trans_apply,
    Equiv.symm_symm, Functor.FullyFaithful.homEquiv_apply, Functor.map_id, Iso.homCongr_symm,
    Iso.symm_symm_eq, Iso.refl_symm, Iso.homCongr_apply, Iso.refl_hom, Category.comp_id,
    unitCompPartialBijective_symm_apply, Functor.id_obj, Functor.comp_obj, Iso.symm_inv]
  -- Porting note: added
  erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
  rw [uncurry_natural_left, uncurry_curry, uncurry_natural_left, uncurry_curry,
    ← BraidedCategory.braiding_naturality_left_assoc, SymmetricCategory.symmetry_assoc,
    ← MonoidalCategory.whisker_exchange_assoc, ← tensorHom_def'_assoc,
    Adjunction.homEquiv_symm_apply, ← Adjunction.eq_unit_comp_map_iff, Iso.comp_inv_eq,
    Category.assoc, prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)]
  apply hom_ext
  · rw [tensorHom_fst, Category.assoc, Category.assoc, prodComparison_fst, ← i.map_comp,
    prodComparison_fst]
    apply (reflectorAdjunction i).unit.naturality
  · rw [tensorHom_snd, Category.assoc, Category.assoc, prodComparison_snd, ← i.map_comp,
    prodComparison_snd]
    apply (reflectorAdjunction i).unit.naturality

Goal state after:
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
f g : C
⊢ ∀ {Z : C} (f_1 : g ⟶ Z), f ◁ f_1 ≫ (coprod.braiding f Z).hom = (coprod.braiding f g).hom ≫ f_1 ▷ f

Tactic:
by simp

Goal state after:
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✝ : C
f : X✝ ⟶ Y✝
g : C
⊢ f ▷ g ≫ (coprod.braiding Y✝ g).hom = (coprod.braiding X✝ g).hom ≫ g ◁ f

Tactic:
by simp

Goal state after:
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 : C
⊢ (coprod.braiding X Y).hom ≫ (coprod.braiding Y X).hom = 𝟙 (X ⊗ Y)

Tactic:
by 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 : Mon C
P : Bimod R S
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
by
  dsimp [hom, inv]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  rw [one_actLeft, Iso.inv_hom_id]

Goal state after: