mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ localized₀ p f (M' ⊓ M'') = localized₀ p f M' ⊓ localized₀ p f M''

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
⊢ (map N.mkQ P).annihilator = N.colon ↑P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ ⊤ = map N.mkQ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ ↑(localized' S p f (M' ⊓ M'')) = ↑(localized' S p f M' ⊓ localized' S p f M'')

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ localized' S p f (⨆ i, g i) = ⨆ i, localized' S p f (g i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ localized₀ p f (⨆ i, g i) = ⨆ i, localized₀ p f (g i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ Module.annihilator R (M ⧸ N) = N.colon Set.univ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ Module.annihilator R (R ⧸ I) = I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized' S p f (sSup s) = sSup (localized' S p f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty ↑I.minimalPrimes

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
s : Set M
⊢ localized' S p f (span R s) = span S (⇑f '' s)

Tactic:
rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
s : Set M
⊢ localized' S p f (span R s) = span S (⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ IsReduced S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ (Ideal.span {y}).IsRadical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ J.IsPrime} = sInf {J | J.IsPrime}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ nilradical R = ⊥ ↔ IsReduced R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical.minimalPrimes = I.minimalPrimes

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ sInf I.minimalPrimes = I.radical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.minimalPrimes = {I.radical}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.minimalPrimes = {I}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ ⊤.minimalPrimes = ∅

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
⊢ IsNilpotent ((toMatrix b b) f) ↔ IsNilpotent f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.minimalPrimes = ∅ ↔ I = ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ localized₀ p f (I • M') = I • localized₀ p f M'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ J ≤ p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r 1 = (algebraMap R S) r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
hf : IsNilpotent (LinearMap.restrict f hq)
⊢ IsNilpotent (LinearMap.restrict f hp)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
⊢ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N') = I • restrictScalars R N'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ (f.restrict hf ^ n) m = 0 m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo ⇑f ↑p ↑p
hnil : IsNilpotent f
⊢ IsNilpotent (f.restrict hf)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ restrictScalars R (localized' S p f (I • M')) =
    restrictScalars R (localized' S p (Algebra.linearMap R S) I • localized' S p f M')

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.IsRadical ↔ IsReduced (R ⧸ I)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ p ∈ (I ⊔ J).minimalPrimes

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
⊢ IsUnit ((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ (⟨x, hx⟩, s).2 • ⟨IsLocalizedModule.mk' f x s, ⋯⟩ = (toLocalized₀ p f M') (⟨x, hx⟩, s).1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ ∀ (y : ↥(localized₀ p f M')), ∃ x, x.2 • y = (toLocalized₀ p f M') x.1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x₁✝ x₂✝ : ↥M'
e : (toLocalized₀ p f M') x₁✝ = (toLocalized₀ p f M') x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
⊢ localized₀ p f P ≤ localized₀ p f Q

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
x : ↥p
m : N ⧸ localized' S p f M'
⊢ ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x) (IsLocalization.mk' S 1 x • m) = m

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ n + 1 + 1 ≤ 2 * (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ≤ q ∧ J ≤ q
⊢ map (algebraMap R S) p ≤ q

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
x : ↥p
⊢ IsUnit ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : IsNilpotent I
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
⊢ P I

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
y : M
s : ↥p
⊢ (Submodule.Quotient.mk y, s).2 • Submodule.Quotient.mk (Function.uncurry (mk' f) (y, s)) =
    (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk y, s).1

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
y : N ⧸ localized' S p f M'
⊢ ∃ x, x.2 • y = (Submodule.toLocalizedQuotient' S p f M') x.1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
⊢ P ∈ (map (algebraMap R S) I ⊔ J).minimalPrimes

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
m n : M
e :
  (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk m) =
    (Submodule.toLocalizedQuotient' S p f M') (Submodule.Quotient.mk n)
⊢ f (m - n) ∈ ?m.478

Tactic:
by

Goal state after: