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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.unop.fst = (Iso.refl p.cocone.unop.pt).hom ≫ ⋯.cone.fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.unop.snd = (Iso.refl p.cocone.unop.pt).hom ≫ ⋯.cone.snd

Tactic:
simp

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

Goal state before:
pp: case ε
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : G.LaxMonoidal
⊢ ε G = ε G

Tactic:
simp

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

Goal state before:
pp: case η
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : F.OplaxMonoidal
⊢ η F = η F

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
by
  simp [← braiding_rightUnitor]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (β_ X Y).hom ≫ i.hom.app (Y ⊗ X)

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
inst✝¹⁵ : MonoidalCategory C✝
inst✝¹⁴ : BraidedCategory C✝
D✝ : Type u₂
inst✝¹³ : Category.{v₂, u₂} D✝
inst✝¹² : MonoidalCategory D✝
inst✝¹¹ : BraidedCategory D✝
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
inst✝⁸ : BraidedCategory E
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✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory C
inst✝² : SymmetricCategory D
F : C ⥤ D
inst✝¹ : F.Braided
inst✝ : F.Faithful
X Y : C
⊢ F.map ((β_ X Y).hom ≫ (β_ Y X).hom) = F.map (𝟙 (X ⊗ Y))

Tactic:
simp

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ (f₁ ⊗ₘ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂ = ((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂) = tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂)

Tactic:
simp

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (Z₁ ⊗ Z₂) ◁ (f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂ = ((𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ⊗ₘ f₁ ⊗ₘ f₂) ≫ tensorμ Z₁ Z₂ Y₁ Y₂

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
Z₁ Z₂ X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ tensorμ Z₁ Z₂ X₁ X₂ ≫ (Z₁ ◁ f₁ ⊗ₘ Z₂ ◁ f₂) = tensorμ Z₁ Z₂ X₁ X₂ ≫ ((𝟙 Z₁ ⊗ₘ f₁) ⊗ₘ 𝟙 Z₂ ⊗ₘ f₂)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    ((𝟙 (𝟙_ D) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X))) ≫
      LaxMonoidal.μ F (𝟙_ C) X ≫ F.map (λ_ X).hom ≫ i.hom.app X

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    ((i.inv.app X ⊗ₘ 𝟙 (𝟙_ D)) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F)) ≫
      LaxMonoidal.μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom ≫ i.hom.app X

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
j : J
r : R
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (coconePointSMul F) r =
    (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
          s.pt.smul r =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        (colimitCocone F).pt.smul r ≫
          colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
intro j

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
        s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimitCocone F).pt.smul r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        (forget₂ (ModuleCat R) AddCommGrpCat).map
          (homMk
            (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
            ⋯)

Tactic:
intro j

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (forget₂ (ModuleCat R) AddCommGrpCat).map
        (homMk
          (colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s))
          ⋯)
Module: Mathlib.CategoryTheory.Functor.TwoSquare

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
C₅ : Type u₅
C₆ : Type u₆
C₇ : Type u₇
C₈ : Type u₈
inst✝⁴ : Category.{v₅, u₅} C₅
inst✝³ : Category.{v₆, u₆} C₆
inst✝² : Category.{v₇, u₇} C₇
inst✝¹ : Category.{v₈, u₈} C₈
T' : C₂ ⥤ C₅
R' : C₅ ⥤ C₆
B' : C₄ ⥤ C₆
L' : C₃ ⥤ C₇
R'' : C₄ ⥤ C₈
B'' : C₇ ⥤ C₈
C₉ : Type u₉
inst✝ : Category.{v₉, u₉} C₉
R₃ : C₆ ⥤ C₉
B₃ : C₈ ⥤ C₉
w₁ : TwoSquare T L R B
w₂ : TwoSquare T' R R' B'
w₃ : TwoSquare B L' R'' B''
w₄ : TwoSquare B' R'' R₃ B₃
c : C₁
⊢ R₃.map (w₂.natTrans.app (T.obj c)) ≫
      R₃.map (B'.map (w₁.natTrans.app c)) ≫ w₄.natTrans.app (B.obj (L.obj c)) ≫ B₃.map (w₃.natTrans.app (L.obj c)) =
    R₃.map (w₂.natTrans.app (T.obj c)) ≫
      ((B' ⋙ R₃).map (w₁.natTrans.app c) ≫ w₄.app (B.obj (L.obj c))) ≫ B₃.map (w₃.natTrans.app (L.obj c))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a ∈
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝¹ x✝ : Quot F
⊢ (quotToQuotUlift F) (x✝¹ + x✝) = (quotToQuotUlift F) x✝¹ + (quotToQuotUlift F) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((toCocone F f).ι.app j)) x = f ((ι F j) x)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂) α).app d) ≫ adj₂.counit.app (H.obj d) = α.app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
x : ↑G
⊢ (Hom.hom (f ≫ ofHom (mk' (Hom.hom f).range))) x = (Hom.hom 0) x

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : Cᵒᵖ
f : x✝¹ ⟶ x✝
⊢ (X ◁ f ≫ (β_ (Opposite.unop x✝) (Opposite.unop X)).op.hom).unop =
    ((β_ (Opposite.unop x✝¹) (Opposite.unop X)).op.hom ≫ f ▷ X).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : Cᵒᵖ
f : x✝¹ ⟶ x✝
Z : Cᵒᵖ
⊢ (f ▷ Z ≫ (β_ (Opposite.unop Z) (Opposite.unop x✝)).op.hom).unop =
    ((β_ (Opposite.unop Z) (Opposite.unop x✝¹)).op.hom ≫ Z ◁ f).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : Cᴹᵒᵖ
f : x✝¹ ⟶ x✝
⊢ (X ◁ f ≫ (β_ x✝.unmop X.unmop).mop.hom).unmop = ((β_ x✝¹.unmop X.unmop).mop.hom ≫ f ▷ X).unmop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : Cᴹᵒᵖ
f : x✝¹ ⟶ x✝
Z : Cᴹᵒᵖ
⊢ (f ▷ Z ≫ (β_ Z.unmop x✝.unmop).mop.hom).unmop = ((β_ Z.unmop x✝¹.unmop).mop.hom ≫ Z ◁ f).unmop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ X ◁ f ≫ (β_ x✝ X).symm.hom = (β_ x✝¹ X).symm.hom ≫ f ▷ X

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
Z : C
⊢ f ▷ Z ≫ (β_ Z x✝).symm.hom = (β_ Z x✝¹).symm.hom ≫ Z ◁ f

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (⇑(((fun f ↦ (ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯)
                ((fun F ↦ F.toLinearMap ∘ₗ { toFun := fun m ↦ ↑(FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ })
                  F)).comp
            (RingCon.mkₐ R (ringCon R M))) ∘
        FreeAlgebra.ι R)
      x =
    (⇑(F.comp (RingCon.mkₐ R (ringCon R M))) ∘ FreeAlgebra.ι R) x

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ F ↑(FreeAlgebra.ι R x) = F ↑(FreeAlgebra.ι R x)
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² : AlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (AlgCat R) (ModuleCat R)).obj x✝³)
⊢ ((Hom.hom
            ((forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝¹ ≫
              ofHom ((TensorAlgebra.lift R) LinearMap.id))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x✝ =
    ((Hom.hom (ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝¹)).toLinearMap ∘ₗ TensorAlgebra.ι R)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : ModuleCat R
x✝ : ↑x✝¹
⊢ ((((TensorAlgebra.lift R) LinearMap.id).comp
            ((TensorAlgebra.lift R) (TensorAlgebra.ι R ∘ₗ TensorAlgebra.ι R))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x✝ =
    ((AlgHom.id R (TensorAlgebra R ↑x✝¹)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case zero
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ x.snd <• x.fst ^ 0 = x.fst ^ 0 •> x.snd

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
d : D
⊢ L₂.map (((conjugateEquiv adj₁ adj₂) α).app d) ≫ adj₂.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case nil
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
⊢ [].prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst [])).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst [])).prod)
        [].zipIdx).sum

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
this :
  adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
          𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
            𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
              R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                  𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c))
⊢ adj₂.unit.app c ≫ R₂.map (𝟙 (L₂.obj c) ≫ α.app c ≫ 𝟙 (L₁.obj c)) = adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
x✝ : D
⊢ ((conjugateEquiv adj₁ adj₁) (𝟙 L₁)).app x✝ = (𝟙 R₁).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommMonoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
x₁ x₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₂.2 + x₁.2 <• x₂.1 = x₂.1 •> x₁.2 + x₂.2 <• x₁.1

Tactic:
rw [op_smul_eq_smul, op_smul_eq_smul, add_comm]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).fst

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).snd

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 L₁

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 L₂

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 R₂

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 R₁

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (↑(TensorProduct.comm R R R) ∘ₗ comul) 1 = comul 1

Tactic:
simp

Goal state after: