mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.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✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ F.map (f✝ ▷ Z✝ ≫ (β Y✝ Z✝).hom) = F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)

Tactic:
refine (cancel_epi (μ F ?_ ?_)).1 ?_

Goal state after:
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
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ μ F X✝ Z✝ ≫ F.map (f✝ ▷ Z✝ ≫ (β Y✝ Z✝).hom) = μ F X✝ Z✝ ≫ F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)
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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁵ : F.OplaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : adj.IsMonoidal
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝² : F'.OplaxMonoidal
inst✝¹ : G'.LaxMonoidal
inst✝ : adj'.IsMonoidal
X Y : E
⊢ μ (G' ⋙ G) X Y =
    (adj.comp adj').unit.app ((G' ⋙ G).obj X ⊗ (G' ⋙ G).obj Y) ≫
      (G' ⋙ G).map
        (δ (F ⋙ F') ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ≫ ((adj.comp adj').counit.app X ⊗ₘ (adj.comp adj').counit.app Y))

Tactic:
by
    simp only [comp_obj, comp_μ, IsMonoidal.leftAdjoint_μ (adj := adj), id_obj,
      IsMonoidal.leftAdjoint_μ (adj := adj'), assoc, ← map_comp, comp_unit_app, comp_δ,
      comp_counit_app, ← tensorHom_comp_tensorHom, δ_natural_assoc, Functor.comp_map]
    simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ g₁.op ≫ i₁.op = i₃.op ≫ f₁.op

Tactic:
simp [eq₁, ← op_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ g₁.op ≫ i₃.op = i₁.op ≫ f₁.op

Tactic:
simp [eq₁, ← op_comp]

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

Goal state before:
pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ X (𝟙_ C) (𝟙_ C)).hom

Tactic:
rw [← braiding_naturality_right]

Goal state after:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ X (𝟙_ C)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ X (𝟙_ C) (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ (𝟙_ C) X).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ (𝟙_ C) (𝟙_ C) X).inv

Tactic:
← braiding_naturality_left

Goal state after:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (β_ (𝟙_ C) X).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
| (α_ (𝟙_ C) (𝟙_ C) X).inv
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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂ = tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        (𝟙 Y₁ ⊗ₘ (α_ Y₂ V₁ V₂).inv) ≫
          (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂) ≫ (𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
slice_lhs 1 2 => rw [associator_naturality]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ (((((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ V₁ V₂).inv)) ≫
          (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂)) ≫
        (𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom)) ≫
      (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        (𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv) ≫
          (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ₘ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
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
⊢ (λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ tensorμ (𝟙_ C) (𝟙_ C) X₁ X₂ ≫ ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ (X₁ ⊗ X₂)).hom =
    (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫
      ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫
          𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv ≫
            𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫
        ((λ_ X₁).hom ⊗ₘ (λ_ X₂).hom)
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
⊢ (ρ_ (X₁ ⊗ X₂)).hom = (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ X₁ X₂ (𝟙_ C) (𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom)

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (ρ_ (X₁ ⊗ X₂)).hom =
    (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv ≫
      ((α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫
          X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv ≫
            X₁ ◁ (β_ X₂ (𝟙_ C)).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).hom ≫ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).inv) ≫
        ((ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom)
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 : Quot F
⊢ (quotUliftToQuot F) ((quotToQuotUlift F) x) = x

Tactic:
conv_rhs => rw [← AddMonoidHom.id_apply _ x]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
⊢ (quotUliftToQuot F) ((quotToQuotUlift F) x) = (AddMonoidHom.id (Quot F)) x
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 : Quot (F ⋙ uliftFunctor)
⊢ (quotToQuotUlift F) ((quotUliftToQuot F) x) = x

Tactic:
conv_rhs => rw [← AddMonoidHom.id_apply _ x]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
⊢ (quotToQuotUlift F) ((quotUliftToQuot F) x) = (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) x
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
⊢ (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom = tensorμ (𝟙_ C) X₁ (𝟙_ C) X₂ ≫ (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom =
    ((α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
        𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).inv ≫
          𝟙_ C ◁ (β_ X₁ (𝟙_ C)).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).hom ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).inv) ≫
      (λ_ (𝟙_ C)).hom ▷ (X₁ ⊗ X₂) ≫ (λ_ (X₁ ⊗ X₂)).hom
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
⊢ (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom = tensorμ X₁ (𝟙_ C) X₂ (𝟙_ C) ≫ (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
⊢ (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
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₂ X₃ Y₁ Y₂ Y₃ : C
⊢ tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫ tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫ tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ (X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃

Tactic:
dsimp only [tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫
        (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫
          (X₁ ⊗ X₂) ◁ (β_ X₃ (Y₁ ⊗ Y₂)).hom ▷ Y₃ ≫
            (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫
      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
            X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
          (X₃ ⊗ Y₃) ≫
        (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
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
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd

Tactic:
op_mul,

Goal state after:
case succ
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
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ (op x.fst * op (x.fst ^ n)) •> x.snd = (x.fst ^ n * x.fst) •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.snd = snd 0

Tactic:
rw [snd_inv, snd_inr, fst_inr, inv_zero, op_zero, zero_smul, snd_zero, neg_zero]

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

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ rTensor R (inl R A B) ∘ₗ (TensorProduct.mk R A R).flip 1 = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

Tactic:
rTensor_comp_flip_mk

Goal state after:
case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ rTensor R (inr R A B) ∘ₗ (TensorProduct.mk R B R).flip 1 = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
rTensor_comp_flip_mk

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ rTensor R (lsingle i✝) ∘ₗ (TensorProduct.mk R (A i✝) R).flip 1 =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝

Tactic:
rTensor_comp_flip_mk

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝ =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ rTensor R (lsingle a✝) ∘ₗ (TensorProduct.mk R A R).flip 1 = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝

Tactic:
rTensor_comp_flip_mk

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝ = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ rTensor R (LinearMap.single R A i✝) ∘ₗ (TensorProduct.mk R (A i✝) R).flip 1 =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝

Tactic:
rTensor_comp_flip_mk

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝ =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (x✝¹ + x✝)) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)

Tactic:
tmul_add,

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹ + 1 ⊗ₜ[R] x✝) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
⊢ ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑X →ₗ[R] ↑Y

Tactic:
refine
    { toFun s := HomEquiv.evalAt f s g, map_add' := fun (s₁ s₂ : S) ↦ ?_,
      map_smul' := fun (r : R) (s : S) ↦ ?_ }
    · ext
      dsimp only [m2, evalAt_apply, LinearMap.add_apply]
      rw [← add_smul]
    · ext x
      apply mul_smul (f r) s (g x)

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a✝ b✝ a b : α
⊢ a * b = b * a

Tactic:
← add_eq_zero',

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a✝ b✝ a b : α
⊢ a * b + b * a = 0
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ ε.op ▷ op A.X ≫ Δ.op = (λ_ (op A.X)).hom

Tactic:
rw [← op_whiskerRight, ← op_comp, counit_comul]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (λ_ A.X).inv.op = (λ_ (op A.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ η.unop ▷ unop A.X = (λ_ (unop A.X)).inv

Tactic:
← unop_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (η ▷ A.X).unop = (λ_ (unop A.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ μ.unop = μ.unop ≫ μ.unop ▷ unop A.X ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
← unop_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ μ.unop = μ.unop ≫ (μ ▷ A.X).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ δ F A A ≫ F.obj A ◁ F.map ε ≫ F.obj A ◁ η F = (ρ_ (F.obj A)).inv

Tactic:
δ_natural_right_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ F.map (A ◁ ε) ≫ δ F A (𝟙_ C) ≫ F.obj A ◁ η F = (ρ_ (F.obj A)).inv
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ δ F A A ≫ F.obj A ◁ F.map Δ ≫ F.obj A ◁ δ F A A =
    F.map Δ ≫ F.map (Δ ▷ A) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom

Tactic:
δ_natural_right_assoc,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ F.map Δ ≫ F.map (A ◁ Δ) ≫ δ F A (A ⊗ A) ≫ F.obj A ◁ δ F A A =
    F.map Δ ≫ F.map (Δ ▷ A) ≫ δ F (A ⊗ A) A ≫ δ F A A ▷ F.obj A ≫ (α_ (F.obj A) (F.obj A) (F.obj A)).hom
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case pos
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : x = 0
⊢ count p (normalizedFactors x) = n

pp: case neg
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ count p (normalizedFactors x) = n

Tactic:
· simp [hx0] at hlt

Goal state after:
case neg
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ count p (normalizedFactors x) = n
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).1
⊢ z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
simpa using h

Goal state after: