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

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

Tactic:
whiskerLeft_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙_ C ◁ (λ_ X).hom ▷ Y = 𝟙_ C ◁ (α_ (𝟙_ C) X Y).hom ≫ 𝟙_ C ◁ (λ_ (X ⊗ Y)).hom
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (X : D) {Y Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
intro X

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X : D
⊢ ∀ {Y Z : D} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ 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
h : F.CoreMonoidal
X Y Z : C
⊢ (h.μIso X Y).hom ▷ F.obj Z ≫ (h.μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    (h.μIso X Y).hom ▷ F.obj Z ≫
      (h.μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom ≫ (h.μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (h.μIso Y Z).inv

Tactic:
hom_inv_whiskerRight_assoc,

Goal state after:
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
h : F.CoreMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    (h.μIso X Y).hom ▷ F.obj Z ≫
      (h.μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom ≫ (h.μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (h.μIso Y Z).inv
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).fst

Tactic:
dsimp only [fst]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : naturalityProperty app e.hom
⊢ naturalityProperty app e.inv

Tactic:
simp only [naturalityProperty] at he ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F₁ F₂ : C ⥤ D
app : (X : C) → F₁.obj X ⟶ F₂.obj X
X Y : C
e : X ≅ Y
he : F₁.map e.hom ≫ app Y = app X ≫ F₂.map e.hom
⊢ F₁.map e.inv ≫ app X = app Y ≫ F₂.map e.inv
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
exact hf

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.injective C f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
exact hf

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj X✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝)) ≫
      F.map x✝¹ ▷ F.obj x✝ =
    F.map (x✝¹ ▷ x✝) ≫
      (adj.homEquiv (Y✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
        ((adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm, assoc, ← μ_natural_left]
    simp [← tensorHom_id]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi f

Tactic:
exact hf

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono f

Tactic:
exact hf

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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ η e.functor ≫ e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = 𝟙 (e.functor.obj (𝟙_ C))

Tactic:
← functor_map_ε_inverse_comp_counitIso_hom_app,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (𝟙_ D)) ≫
      e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) =
    𝟙 (e.functor.obj (𝟙_ C))
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 ≫ (ρ_ X).hom) = 𝟙_ C ◁ (λ_ X).hom

Tactic:
whiskerLeft_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = 𝟙_ C ◁ (λ_ X).hom
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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ η e.functor ≫ e.counitInv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = 𝟙 (e.functor.obj (𝟙_ C))

Tactic:
← functor_map_ε_inverse_comp_counitIso_hom_app,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (𝟙_ D)) ≫ e.counitInv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) =
    𝟙 (e.functor.obj (𝟙_ C))
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)
⊢ (desc F c) ((ι F j) x) = (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
by
  dsimp [desc, ι]
  erw [QuotientAddGroup.lift_mk']
  simp

Goal state after:
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₃
⊢ (w₁ ≫ₕ w₂) ≫ᵥ w₃ ≫ₕ w₄ = (w₁ ≫ᵥ w₃) ≫ₕ w₂ ≫ᵥ w₄

Tactic:
unfold hComp vComp whiskerLeft whiskerRight
  ext c
  simp only [comp_obj, NatTrans.comp_app, associator_hom_app, associator_inv_app, comp_id, id_comp,
    map_comp, assoc]
  slice_rhs 2 3 =>
    rw [← Functor.comp_map _ B₃, ← w₄.naturality]
  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
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Quot.desc F c) ((Quot.ι F j) x))) =
    (Hom.hom (s.ι.app j)) x

Tactic:
rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Quot.desc F s) ((Quot.ι F j) x) = (Hom.hom (s.ι.app j)) 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
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((Quot.desc F c) x) = (Quot.desc F s) ((AddEquiv.ofBijective (Quot.desc F c) h).symm ((Quot.desc F c) x))

Tactic:
rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) = (Quot.desc F s) 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
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.obj Y ⊗ F.obj Z) ≫
      F.obj (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:
← tensorHom_def_assoc

Goal state after:
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)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
inv_mul_cancel_right₀ ha,

Goal state after:
case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + g (r₁ •> m₂ + m₁ <• r₂) = f r₁ * f r₂ + g m₁ * f r₂ + f r₁ * g m₂

Tactic:
← map_mul,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ f (r₁ * r₂) + g (r₁ •> m₂ + m₁ <• r₂) = f (r₁ * r₂) + g m₁ * f r₂ + f r₁ * g m₂
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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ ({ toFun := fun s ↦ HomEquiv.evalAt f s g, map_add' := ⋯, map_smul' := ⋯ } 1).toAddHom x = (Hom.hom g) x

Tactic:
LinearMap.coe_mk

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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑X
⊢ ({ toFun := fun s ↦ HomEquiv.evalAt f s g, map_add' := ⋯ } 1).toAddHom x = (Hom.hom g) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ ({ toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
          s').toAddHom
      ((ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))

Tactic:
LinearMap.coe_mk

Goal state after:
case tmul
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ ({ toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯ } s').toAddHom
      ((ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) (x✝ + y✝) =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) (x✝ + y✝)

Tactic:
rw [map_add, map_add]

Goal state after:
case add
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 Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2✝ : Module R ↑Y := Module.compHom (↑Y) f
m2 : Module R ↑Y' := Module.compHom (↑Y') f
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑((restrictScalars f).obj Y)
ih₁ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝
ih₂ :
  (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
⊢ (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) x✝ +
      (Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map f)) y✝ =
    (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) x✝ + (Hom.hom (Counit.map f ≫ (𝟭 (ModuleCat S)).map g)) y✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
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
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) (x✝ + y✝) =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) (x✝ + y✝)

Tactic:
rw [map_add, map_add]

Goal state after:
case add
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
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
a✝¹ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝
a✝ :
  (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
⊢ (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) x✝ +
      (Hom.hom ((ExtendRestrictScalarsAdj.homEquiv f).symm g)) y✝ =
    (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) x✝ +
      (Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit f).app Y)) y✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a : A
b : B
⊢ _root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul = comul ∘ₗ LinearMap.mul' R A

Tactic:
ext a b
    simp [← (ℛ R a).eq, ← (ℛ R b).eq, TensorProduct.sum_tmul]
    simp [TensorProduct.tmul_sum, Finset.sum_mul_sum]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ f' ⊤ = ⊤

Tactic:
by simpa only [h] using map_top f

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)

Tactic:
by
  simp [Localization.mk_eq_monoidOf_mk']

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
⊢ b ≠ 0 → (a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b)

Tactic:
hb

Goal state after:
case succ
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
x : R
h : f x ∈ ↑I → f x ∈ ↑J
⊢ x ∈ (fun I ↦ { ringCon := I.ringCon.comap f }) I → x ∈ (fun I ↦ { ringCon := I.ringCon.comap f }) J

Tactic:
simpa [mem_iff, RingCon.comap]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ 0 ∈ J

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ 0 ∈ Module.jacobson R (R ⧸ I)

Tactic:
exact zero_mem _

Goal state after: