mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ : Arrow (Type u)
φ : X✝ ⟶ Y✝
y : ↑(Set.range ⇑(TypeCat.Hom.hom X✝.hom))
⊢ (hom (Arrow.Hom.right φ)) ↑y ∈ Set.range ⇑(TypeCat.Hom.hom Y✝.hom)

Tactic:
obtain ⟨_, x, rfl⟩ := y; exact ⟨φ.left x, congr_hom φ.w x⟩

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

Goal state before:
pp: case a.a.a.a
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₁ ≫ f₁ ⊗ₘ (f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (α_ Y₂ V₁ V₂).inv

pp: case a.a.a.a
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₂
| 𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

pp: case a.a.a
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₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

pp: case a.a
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₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
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

Tactic:
associator_inv_naturality,

Goal state after:
case a.a.a.a
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₁ ≫ f₁ ⊗ₘ (α_ X₂ U₁ U₂).inv ≫ ((f₂ ⊗ₘ g₁) ⊗ₘ g₂)

case a.a.a.a
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₂
| 𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂

case a.a.a
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₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

case a.a
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₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
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
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₂ Z₁ Z₂ : C
⊢ ((α_ 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) ▷
        (Z₁ ⊗ Z₂) ≫
      ((α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
          (X₁ ⊗ Y₁) ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫
            (X₁ ⊗ Y₁) ◁
                ((α_ X₂ Y₂ Z₁).hom ≫
                    X₂ ◁ (β_ Y₂ Z₁).hom ≫ (α_ X₂ Z₁ Y₂).inv ≫ (β_ X₂ Z₁).hom ▷ Y₂ ≫ (α_ Z₁ X₂ Y₂).hom) ▷
                  Z₂ ≫
              (X₁ ⊗ Y₁) ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv) ≫
        ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ := by monoidal
    _ = _ := by rw [← whisker_exchange]; monoidal

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
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map (α_ (W ⊗ X) Y Z).inv ≫
          F.map ((α_ W X Y).hom ▷ Z) ≫
            F.map ((W ◁ (β_ X Y).hom) ▷ Z) ≫ F.map ((α_ W Y X).inv ▷ Z) ≫ F.map (α_ (W ⊗ Y) X Z).hom =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)

Tactic:
simp only [← Functor.map_comp, whisker_assoc, Category.assoc, pentagon_inv_inv_hom_hom_inv,
    pentagon_inv_hom_hom_hom_inv_assoc]

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

Goal state before:
pp: 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
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i) •> (x.snd <• x.fst ^ i)) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd

Tactic:
aux,

Goal state after:
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
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i) •> x.fst ^ i •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (G ⋙ 𝟭 C) L₁ L₃ (H ⋙ 𝟭 D)
        ((G.associator (𝟭 C) L₃).hom ≫
          G.whiskerLeft (natTrans (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) ≫
            (G.associator L₂ (𝟭 D)).inv ≫ whiskerRight α.natTrans (𝟭 D) ≫ (L₁.associator H (𝟭 D)).hom)) =
    TwoSquare.mk R₁ (H ⋙ 𝟭 D) (G ⋙ 𝟭 C) R₃
      ((R₁.associator G (𝟭 C)).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) α).natTrans (𝟭 C) ≫
          (H.associator R₂ (𝟭 C)).hom ≫
            H.whiskerLeft ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)).natTrans ≫
              (H.associator (𝟭 D) R₃).inv)
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.app (G.obj (R₁.obj b))) ≫ R₃.map (α.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    adj₂.unit.app (G.obj (R₁.obj b)) ≫
      R₂.map (α.natTrans.app (R₁.obj b)) ≫
        R₂.map (H.map (adj₁.counit.app b)) ≫
          adj₃.unit.app (R₂.obj (H.obj b)) ≫ R₃.map (β.app (R₂.obj (H.obj b))) ≫ R₃.map (adj₂.counit.app (H.obj b))
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)).natTrans.app b

Tactic:
simpa [mateEquiv]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃)
      (TwoSquare.mk (𝟭 A ⋙ G) L₁ L₃ (𝟭 B ⋙ H)
        (((𝟭 A).associator G L₃).hom ≫
          (𝟭 A).whiskerLeft β.natTrans ≫
            ((𝟭 A).associator L₂ H).inv ≫
              whiskerRight (natTrans (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) H ≫ (L₁.associator (𝟭 B) H).hom)) =
    TwoSquare.mk R₁ (𝟭 B ⋙ H) (𝟭 A ⋙ G) R₃
      ((R₁.associator (𝟭 A) G).inv ≫
        whiskerRight ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).natTrans G ≫
          ((𝟭 B).associator R₂ G).hom ≫
            (𝟭 B).whiskerLeft ((mateEquiv adj₂ adj₃) β).natTrans ≫ ((𝟭 B).associator H R₃).inv)
vcompb :
  adj₃.unit.app (G.obj (R₁.obj b)) ≫
      R₃.map (β.natTrans.app (R₁.obj b)) ≫ R₃.map (H.map (α.app (R₁.obj b))) ≫ R₃.map (H.map (adj₁.counit.app b)) =
    G.map (adj₂.unit.app (R₁.obj b)) ≫
      G.map (R₂.map (α.app (R₁.obj b))) ≫
        G.map (R₂.map (adj₁.counit.app b)) ≫
          adj₃.unit.app (G.obj (R₂.obj b)) ≫ R₃.map (β.natTrans.app (R₂.obj b)) ≫ R₃.map (H.map (adj₂.counit.app b))
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
simpa [mateEquiv]

Goal state after:
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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s₁ s₂ : S
y : ↑Y
⊢ (s₁ + s₂) • y = s₁ • y + s₂ • y

Tactic:
add_smul

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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s₁ s₂ : S
y : ↑Y
⊢ s₁ • y + s₂ • y = s₁ • y + s₂ • y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M)))
      ((Hom.hom ((extendScalarsComp (RingHom.id R₁) f₁₂).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
extendScalarsComp_hom_app_one_tmul (RingHom.id R₁) f₁₂ M m

Goal state after:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M))) (1 ⊗ₜ[R₁] (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a - b = a + b

Tactic:
by rw [sub_eq_add_neg, add_right_inj, neg_eq]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (n • g x)

Tactic:
exact IsAddUnit.map (nsmulAddMonoidHom n : C →+ C) hg

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫
        ModuleCat.ofHom CoalgebraStruct.comul ▷ ModuleCat.of R ↑X.toModuleCat ≫
          (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat)).hom)

Tactic:
by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ Hom.hom
      (Under.Hom.right
        (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
          {
                app := fun S ↦
                  Under.homMk
                    (ofHom
                      (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                        (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                    ⋯,
                naturality := ⋯ }.app
            (R.monoidAlgebra.obj G))) =
    Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))

Tactic:
apply MonoidAlgebra.ringHom_ext <;> intro <;> simp [MonoidAlgebra.liftNCRingHom]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ η ≫ f ▷ Z = η

Tactic:
by simpa using ((inferInstance : IsMonHom (f ⊗ₘ (𝟙 Z)))).one_hom

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

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y X (X ⊗ Y)).hom ≫ Y ◁ X ◁ (β_ X Y).hom

pp: case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ X Y X).inv

pp: case a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (β_ X Y).hom ▷ X

pp: case a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ Y X X).hom

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y Y (X ⊗ X)).inv

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| μ ⊗ₘ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (β_ X Y).hom ▷ (X ⊗ Y)

Tactic:
rw [← associator_naturality_right]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (Y ⊗ X) ◁ (β_ X Y).hom ≫ (α_ Y X (Y ⊗ X)).hom

case a.a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ X Y X).inv

case a.a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (β_ X Y).hom ▷ X

case a.a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| Y ◁ (α_ Y X X).hom

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (α_ Y Y (X ⊗ X)).inv

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| μ ⊗ₘ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
| (β_ X Y).hom ▷ (X ⊗ Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inr' ≫ (isoIsPushout X Y h h').inv = inr

Tactic:
by
  simp only [Iso.comp_inv_eq, inr_isoIsPushout_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
w : fst ≫ f = snd ≫ g
hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄, φ ≫ fst = φ' ≫ fst → φ ≫ snd = φ' ≫ snd → φ = φ'
exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y), a ≫ f = b ≫ g → ∃ l, l ≫ fst = a ∧ l ≫ snd = b
⊢ Nonempty (IsLimit (PullbackCone.mk fst snd w))

Tactic:
by
    let l (s : PullbackCone f g) := exists_lift _ _ s.condition
    exact ⟨PullbackCone.IsLimit.mk _
      (fun s ↦ (l s).choose)
      (fun s ↦ (l s).choose_spec.1)
      (fun s ↦ (l s).choose_spec.2)
      (fun s m h₁ h₂ ↦ hom_ext
        (h₁.trans (l s).choose_spec.1.symm)
        (h₂.trans (l s).choose_spec.2.symm))⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: M : Type u_7
N : Type u_8
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_9
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
y : M
hy : y ∈ ↑(IsUnit.submonoid M)
⊢ f y ∈ IsUnit.submonoid N

Tactic:
exact hy.map _

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
y : R
hy : y ∈ ↑(IsUnit.submonoid R)
⊢ (algebraMap R S) y ∈ IsUnit.submonoid S

Tactic:
exact hy.map _

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_2
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
M' : Type u_4
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M'
inst✝⁷ : Module A M'
inst✝⁶ : IsScalarTower R A M'
S : Submonoid A
N : Type u_7
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
P : Type u_8
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
g : M →ₗ[A] M'
h : IsLocalizedModule S g
⊢ (map S ((AlgebraTensorModule.rTensor R N) g) ((AlgebraTensorModule.rTensor R P) g))
      ((AlgebraTensorModule.lTensor A M) f) =
    (AlgebraTensorModule.lTensor A M') f

Tactic:
apply linearMap_ext S (AlgebraTensorModule.rTensor R N g) (AlgebraTensorModule.rTensor R P g)
  rw [map_comp]
  ext
  simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
S : Submonoid R
⊢ OreLocalization.instMonoid = instMonoid

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
S : Submonoid R
⊢ OreLocalization.instCommRing = instCommRing

Tactic:
with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeRing α
⊢ ∀ (x : FreeMonoid α),
    ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) =
      ((fun α_1 ↦ FreeAbelianGroup.of α_1) ∘ fun l ↦ ↑l) x

Tactic:
intro L

Goal state after:
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 ↦ FreeAbelianGroup.of α_1) ∘ fun l ↦ ↑l) L
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
x : LocalizedModule S A
⊢ (numeratorRingHom.comp (algebraMap R A)) r * x = x * (numeratorRingHom.comp (algebraMap R A)) r

Tactic:
induction x using induction_on with | _ a s => _
    simp only [RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
      Function.comp_apply]
    rw [mk_mul_mk, mk_mul_mk, mul_comm, Algebra.commutes]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
S : Submonoid R
⊢ OreLocalization.instAlgebra = algebra'

Tactic:
with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₁)

Tactic:
rw [LocalizedModule.mk_cancel_common_right]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝¹ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
j : J
inst✝ : IsLocalRing ↑(F.obj j)
hj :
  ∀ (x : ↑c.pt),
    IsUnit ((ConcreteCategory.hom (c.π.app j)) x) →
      ∀ (i : J),
        ∃ k f g,
          IsLocalHom (Hom.hom (F.map f)) ∧
            (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (c.π.app i)) x) =
              (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (c.π.app j)) x)
this : IsLocalHom (Hom.hom (c.π.app j))
⊢ IsLocalRing ↑c.pt

Tactic:
apply RingHom.domain_isLocalRing (c.π.app j).hom

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)

Tactic:
← inv_comp_eq,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso f g).hom ▷ F.map h ≫
      (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : F.Elements
e : x.fst ≅ y.fst
he : (ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd
⊢ (ConcreteCategory.hom (F.map e.inv)) y.snd = x.snd

Tactic:
rw [← he, Functor.map_hom_inv'_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ (ConcreteCategory.hom (F.map (inv ((π F).map f)))) B✝.snd = A✝.snd

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ?refine_1⟩ = 𝟙 A✝

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ?refine_1⟩ ≫ f = 𝟙 B✝

Tactic:
· simp only [← map_snd f, ← Functor.map_comp_apply,
        π_obj, π_map, IsIso.hom_inv_id, Functor.map_id_apply]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ⋯⟩ = 𝟙 A✝

case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ⋯⟩ ≫ f = 𝟙 B✝