mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map α))
      ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂))) x *
        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂))) y) =
    (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map f)) x * (ConcreteCategory.hom (F.map g)) y)

Tactic:
map_mul,

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂))) x) *
      (ConcreteCategory.hom (F.map α)) ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂))) y) =
    (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map f)) x) *
      (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map g)) y)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
      ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) x *
        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y

Tactic:
map_mul,

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j))) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) x) *
      (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
        ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x y : limit F
w : ∀ (j : J), (hom (limit.π F j)) x = (hom (limit.π F j)) y
⊢ x = y

Tactic:
by
  apply (limitEquivSections F).injective
  ext j
  simp [w j]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
this : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
⊢ IsLimit ((forget₂ CommGrpCat GrpCat).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (X ◁ f) ▷ Z = (α_ X Y Z).hom ≫ X ◁ f ▷ Z ≫ (α_ X Y' Z).inv

Tactic:
by
  simp only [← id_tensorHom, ← tensorHom_id]
  rw [← assoc, ← associator_naturality]
  simp

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

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

Tactic:
rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ ((α_ W X (Y ⊗ Z)).inv ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv) ≫ (α_ W X Y).inv ▷ Z =
    ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) ≫ (α_ W X Y).inv ▷ Z
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
⊢ ∀ (w : ↑W) (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom
          (whiskerRight (associator W X Y).hom Z ≫
            (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro w x y z

Goal state after:
R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
w : ↑W
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom
        (whiskerRight (associator W X Y).hom Z ≫
          (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
      (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) =
    (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)
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
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_id]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝ : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ?m.112))

Tactic:
dsimp only [span_map_fst, span_map_snd]
      exact isColimitOfPreserves _ (PushoutCocone.flipIsColimit hc)

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' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (f ⊗ₘ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ₘ f)

Tactic:
rw [tensorHom_def' f g, tensorHom_def g f]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ 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✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁ adj.unit.app Y ▷ Z ≫
        G.obj (F.obj X) ◁ G.obj (F.obj Y) ◁ adj.unit.app Z ≫
          G.obj (F.obj X) ◁ μ G (F.obj Y) (F.obj Z) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
← associator_naturality_middle_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
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (G.obj (F.obj X) ◁ adj.unit.app Y) ▷ Z ≫
      (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) Z).hom ≫
        G.obj (F.obj X) ◁ G.obj (F.obj Y) ◁ adj.unit.app Z ≫
          G.obj (F.obj X) ◁ μ G (F.obj Y) (F.obj Z) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: case a.a
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
c : C
| R₂.map ((L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c)))

pp: case a
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
c : C
| adj₂.unit.app (G.obj c)

pp: case a.a
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
c : C
| R₂.map (α.app c)

Tactic:
rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]

Goal state after:
case a.a
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
c : C
| R₂.map (H.map (𝟙 (L₁.obj c)))

case a
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
c : C
| adj₂.unit.app (G.obj c)

case a.a
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
c : C
| R₂.map (α.app c)
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
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + -(r •> x.snd <• r) <• x.fst = 0

Tactic:
smul_neg,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ r •> x.snd + -(r •> x.snd <• r <• x.fst) = 0
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
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x.fst •> -(r •> (x.snd <• r)) + x.snd <• r = 0

Tactic:
smul_neg,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: 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
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) * x = 1

Tactic:
convert! mul_left_eq_one _ _ (invOf_mul_self x.fst)

Goal state after:
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
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ * x = 1

Tactic:
convert mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx)
  ext <;> simp

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
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (r • s)) = f r • (ConcreteCategory.hom g) (1 ⊗ₜ[R] s)

Tactic:
RestrictScalars.smul_def,

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
r : R
s : ↑X
⊢ (ConcreteCategory.hom g)
      (1 ⊗ₜ[R] (RestrictScalars.addEquiv R R ↑X).symm ((algebraMap R R) r • (RestrictScalars.addEquiv R R ↑X) s)) =
    f r • (ConcreteCategory.hom g) (1 ⊗ₜ[R] s)
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
r : R
s : ↑X
⊢ (ConcreteCategory.hom g)
      (1 ⊗ₜ[R] (RestrictScalars.addEquiv R R ↑X).symm ((algebraMap R R) r • (RestrictScalars.addEquiv R R ↑X) s)) =
    (ConcreteCategory.hom g) (f r • 1 ⊗ₜ[R] s)

Tactic:
tmul_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
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : ↑X
⊢ (ConcreteCategory.hom g) ((algebraMap R R) r • 1 ⊗ₜ[R] (RestrictScalars.addEquiv R R ↑X) s) =
    (ConcreteCategory.hom g) (f r • 1 ⊗ₜ[R] s)
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) 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' := ⋯, map_smul' := ⋯ } 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')
      ((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' := ⋯, map_smul' := ⋯ }
          s').toAddHom
      ((ConcreteCategory.hom g) y) =
    (Hom.hom g) ((Hom.hom (Counit.map f)) (s' ⊗ₜ[R] y))
Module: Mathlib.CategoryTheory.Adjunction.Unique

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
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom = adj2.unit

Tactic:
ext x
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ (fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
      ((fun f ↦ ↾(f.toFun ∘ some)) f) =
    f

Tactic:
apply Pointed.Hom.ext

Goal state after:
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
        ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun =
    f.toFun
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ { toFun := fun f ↦ ↾(f.toFun ∘ some),
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    typeToPointed.map f ≫
      { toFun := fun f ↦ ↾(f.toFun ∘ some),
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
apply Pointed.Hom.ext

Goal state after:
X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ ({ toFun := fun f ↦ ↾(f.toFun ∘ some),
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        (f ≫ g)).toFun =
    (typeToPointed.map f ≫
        { toFun := fun f ↦ ↾(f.toFun ∘ some),
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          g).toFun
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

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

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

Tactic:
· cases n
    · exact count_eq_zero.2 (zero_notMem_normalizedFactors _)
    · rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt
      exact absurd hle hlt

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : Rᵐᵒᵖ
⊢ x ∈ asIdealOpposite I ↔ MulOpposite.unop x ∈ I

Tactic:
by
  simpa [asIdealOpposite, asIdeal, TwoSidedIdeal.mem_iff, RingCon.op_iff] using
    ⟨I.ringCon.symm, I.ringCon.symm⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
⊢ Away r T

Tactic:
by
  refine .mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩
  · obtain ⟨s, rfl⟩ := h₁ t
    exact ⟨0, by simp⟩
  · rw [← sub_eq_zero, ← mul_sub]
    exact hn ⟨x - y, by simp [h]⟩

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' := ⋯ }
⊢ f.ker ≤ Module.jacobson R (R ⧸ I)

Tactic:
rintro _ rfl; exact zero_mem _

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
a : ↑↑s
⊢ f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)

Tactic:
map_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
a : ↑↑s
⊢ f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (↑a ^ (N - n a)) * (algebraMap R (Away ↑a)) (r✝ a)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (algebraMap R (Away (↑a * ↑b))) (r a * ↑b ^ N) = (algebraMap R (Away (↑a * ↑b))) (r b * ↑a ^ N)

Tactic:
map_mul,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (algebraMap R (Away (↑a * ↑b))) (r a) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (algebraMap R (Away (↑a * ↑b))) (r b) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)