mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Mates

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

Tactic:
simp only [conjugateEquiv_id]

Goal state after:
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
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (s •> 1) •> x.snd = (s •> 1) •> x.snd

Tactic:
smul_assoc,

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
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> 1 •> x.snd = (s •> 1) •> x.snd
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
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> x.snd = (s •> 1) •> x.snd

Tactic:
smul_assoc,

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
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> x.snd = s •> 1 •> x.snd
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Equiv.trans ?_ liftEquiv

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 // ∀ (x y : M), f x * f y = 0 } ≃
    { fg //
      (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧
        (∀ (r : R') (x : M), fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ ∀ (r : R') (x : M), fg.2 (x <• r) = fg.2 x * fg.1 r }
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✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
s : S
y : ↑Y
t : S
⊢ ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
          { toFun := fun s_1 ↦ (ConcreteCategory.hom g) (s_1 • s • y), map_add' := ⋯, map_smul' := ⋯ }))
      t =
    ((CoextendScalars.equiv f X)
        ((RingHom.id S) s •
          (CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y), map_add' := ⋯, map_smul' := ⋯ }))
      t

Tactic:
simp [mul_smul]

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✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y : ModuleCat S
s : S
y : ↑Y
t : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
          { toFun := fun s_1 ↦ s_1 • s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y))
        ((RingHom.id S) s •
          (CoextendScalars.equiv f ((restrictScalars f).obj Y)).symm
            { toFun := fun s ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }))
      t

Tactic:
simp [mul_smul]

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

Goal state before:
pp: case refine_3.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
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
s : S
s' : ↑((restrictScalars f).obj (of S S))
x : ↑X
⊢ (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s • s' ⊗ₜ[R] x) =
    s • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (s' ⊗ₜ[R] x)

Tactic:
simp [mul_smul]

Goal state after:
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 : ModuleCat S
s : S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s' : ↑((restrictScalars f).obj (of S S))
y : ↑((restrictScalars f).obj Y)
⊢ (lift { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
      (s • s' ⊗ₜ[R] y) =
    (RingHom.id S) s •
      (lift
          { toFun := fun s ↦ { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ })
        (s' ⊗ₜ[R] y)

Tactic:
simp [mul_smul]

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

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₁ • counit x₁) • x₂ ⊗ₜ[R] y₂ = 1 • counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂

Tactic:
smul_assoc,

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₁ • counit x₁ • x₂ ⊗ₜ[R] y₂ = 1 • counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₂ • counit x₂) • x₁ ⊗ₜ[R] y₁ = 1 • counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁

Tactic:
smul_assoc,

Goal state after:
case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₂ • counit x₂ • x₁ ⊗ₜ[R] y₁ = 1 • counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_add,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + b * (a + b) = a * a + a * b + (b * a + b * b)
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * (1 + a) = 0

Tactic:
mul_add,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * 1 + a * a = 0
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_add,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * (a + b) + a * (a * b) = a
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_add,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * a + a * b + a * (a * b) = a
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.point = Z.point

Tactic:
by rw [Function.comp_apply, f.map_point, g.map_point]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M'
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ

Tactic:
TensorProduct.map_comp

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M'
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

Tactic:
obtain ⟨n, a, hn⟩ := surj r s
    use n, a * u ^ n
    simp [mul_pow, ← mul_assoc, hn]

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

Tactic:
apply Set.image_id

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

Goal state before:
pp: case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I

Tactic:
mul_add,

Goal state after:
case h
R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * r + s * 1 - 1 ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ (algebraMap R S) r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥

Tactic:
· rw [← (RingHom.ker (algebraMap S T)).map_comap_of_surjective _ h₂, ← map_pow,
      ← Ideal.map_pointwise_smul, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]
    rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (hI'.from I ≫ f)
⊢ (inv (hI'.from I ≫ f) ≫ hI'.from I) ≫ f = 𝟙 A

Tactic:
rw [assoc, IsIso.inv_hom_id]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (↑b • a)

Tactic:
simp_rw [Algebra.smul_def, mul_comm _ a]
  apply exists_integer_multiple'

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

Goal state before:
pp: case h
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
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 * y) • mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • y • mk m s

Tactic:
← IsLocalization.mk'_sec (M := S) T y

Goal state after:
case h
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
x y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s
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
s s' : ↥S
m : M
⊢ 1 • s • s' • m = 1 • (s * s') • m

Tactic:
simp [mul_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ (T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X)) ≫ T.μ.app X =
    ((T.toFunctor ⋙ T.toFunctor).map (i.inv.app X) ≫ T.μ.app (T.obj X)) ≫ T.μ.app X

Tactic:
simp [T.assoc X]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Comonad C
X : G.Coalgebra
Y : C
f : G.forget.obj X ⟶ Y
⊢ X.a ≫ G.map (X.a ≫ G.map f) = (X.a ≫ G.map f) ≫ (G.cofree.obj Y).a

Tactic:
by simp [← Coalgebra.coassoc_assoc]

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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ lift S f g h ∘ₗ f = g

Tactic:
dsimp only [IsLocalizedModule.lift]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
⊢ (LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ lift S f g h = l

Tactic:
dsimp only [IsLocalizedModule.lift]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm = l
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
m : s.pt ⟶ (equalizerFork f g).pt
hm : m ≫ (equalizerFork f g).ι = s.ι
x : ↑s.pt
⊢ (Hom.hom m) x = (Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯))) x

Tactic:
exact Subtype.ext <| RingHom.congr_fun (congrArg Hom.hom hm) x

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P
    exact ⟨Q, inferInstance, by rwa [isoClosure_le_iff]⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le P
  have := (isEquivalence_ιOfLE_iff h₁).2 h₂
  rw [← essentiallySmall_congr (ιOfLE h₁).asEquivalence]
  exact essentiallySmall_of_small_of_locallySmall _

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (Ideal.map MvPolynomial.C (RingHom.ker ↑f)).FG

Tactic:
exact hf_ker.map MvPolynomial.C

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁴ : Category.{v_2, u_2} B
T : Type u_3
inst✝³ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom (inv f) = inv (Hom.hom f)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id
  rw [← comp_hom, IsIso.hom_inv_id, id_hom]

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

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ f = g

Tactic:
ext
  · simp
  · exact h

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom

Tactic:
change Ideal.span s₀ = I

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ Ideal.span s₀ = I
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ f = g

Tactic:
by
  ext
  · simp
  · exact h

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ eqToHom ⋯ ≫
      ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ } ≫
          { base := e₁.hom, fiber := e₂.hom }).fiber =
    (𝟙 Y).fiber

Tactic:
have := Functor.congr_hom congr($((F.mapIso e₁).inv_hom_id).toFunctor) e₂.inv
    simp_all

Goal state after: