mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: 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
y x : R
hy : y ∈ closure s
⊢ y * x ∈ closure s

Tactic:
by

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

Goal state before:
pp: 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) ⋯ ⋯ ⋯ ⋯ ⋯
this : z ∈ span s ↔ z ∈ I
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ Away (y * x) T

Tactic:
by

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

Goal state before:
pp: R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ Away ((algebraMap R S₁) y) T

Tactic:
by

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

Goal state before:
pp: 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
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
by

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

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
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ Submonoid.powers x ≤ IsUnit.submonoid R

Tactic:
by

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
⊢ Algebra.algebraMapSubmonoid S (Submonoid.powers r) ≤ IsUnit.submonoid S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ t * s ⊆ ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
I : TwoSidedIdeal R
h : s ⊆ ↑I
t : Set R
⊢ s * t ⊆ ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
x z : R
y : S
inst✝⁵ : Away x S
T : Type u_4
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : Away y T
h : Associated ((algebraMap R S) z) y
⊢ Away ((algebraMap R S) z) T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
x z : R
y : S
inst✝⁵ : Away x S
T : Type u_4
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : Away y T
h : Associated ((algebraMap R S) z) y
⊢ Away (x * z) T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
x✝ : z ∈ span s
⊢ s ⊆ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ jacobson R M ≤ comap f (jacobson R₂ M₂)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
this : ∃ a k, e ^ k * (a * e ^ n) = e ^ k * x
⊢ ∃ a, (algebraMap R S) a = mk' S x ⟨(fun x ↦ e ^ x) n, ⋯⟩

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective ⇑f
h : jacobson R₂ M₂ = ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
r : ↥(Submonoid.powers e)
⊢ IsUnit ((algebraMap R S) ↑r)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : R
⊢ (algebraMap R S) z * (algebraMap R S) ↑(z, 1).2 = (algebraMap R S) (z, 1).1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Function.Bijective ⇑f
⊢ f.ker ≤ jacobson R M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
le : N ≤ jacobson R M
⊢ N.mkQ.ker ≤ jacobson R M

Tactic:
by

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}
H' : Function.Surjective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
h : jacobson R (M ⧸ N) = ⊥
⊢ jacobson R M ≤ N

Tactic:
by

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

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✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
⊢ IsIdempotentElem (1, 0)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ jacobson R (M ⧸ jacobson R M) = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsCoatomic (Submodule R M)
⊢ jacobson R M < ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) (1 * x) 1 = x

Tactic:
by

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

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✝
P : Type u_3
inst✝³ : CommSemiring P
inst✝² : IsLocalization M S✝
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
this : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
⊢ IsIdempotentElem (0, 1)

Tactic:
by

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
hz : z ∈ span (univ * s * univ)
⊢ z ∈ span s

Tactic:
· exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _

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) ≤ ⊥
s : S
⊢ ∃ a, (algebraMap S T) s * (algebraMap S T) r ^ 0 = (algebraMap S T) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ jacobson R ((i : ι) → M i) ≤ pi Set.univ fun x ↦ jacobson R (M x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), jacobson R (M i) = ⊥
⊢ (pi Set.univ fun x ↦ jacobson R (M x)) ≤ ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ jacobson R = sInf {I | I.IsMaximal}

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
x : R
⊢ x ∈ fromIdeal I ↔ x ∈ span ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : R
⊢ x ∈ asIdeal I ↔ x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
m : Ideal R
inst✝ : m.IsMaximal
⊢ jacobson R ≤ m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ asIdeal J
x : R
hx : x ∈ fromIdeal I
⊢ x ∈ J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I✝ I : TwoSidedIdeal R
a✝ x✝ : R
⊢ a✝ ∈ asIdeal I → a✝ * x✝ ∈ asIdeal I

Tactic:
by

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) ≤ ⊥
x y : S
h : (algebraMap S T) x = (algebraMap S T) y
⊢ x - y ∈ ↑(RingHom.ker (algebraMap S T)) ∧ (DistribSMul.toLinearMap S S (r ^ n)) (x - y) = r ^ n * (x - y)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I✝ I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' : x ∈ (fun I ↦ asIdeal { ringCon := I.ringCon.op }) I
⊢ x ∈ (fun I ↦ asIdeal { ringCon := I.ringCon.op }) J

Tactic:
by

Goal state after:
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

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

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝¹ : TwoSidedIdeal R
x✝ : R
⊢ (∀ (I : TwoSidedIdeal R), ↑(asIdeal x✝¹) ⊆ ↑I → x✝ ∈ I) ↔ x✝ ∈ x✝¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R
x✝ : R
h : ∀ (I : TwoSidedIdeal R), ↑J ⊆ ↑I → x✝ ∈ I
x : R
⊢ x ∈ ↑J → x ∈ ↑(mk' ↑J ⋯ ⋯ ⋯ ⋯ ⋯)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R
x : R
⊢ x ∈ J → ∀ (I : TwoSidedIdeal R), ↑J ⊆ ↑I → x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ x ∈ I.toTwoSided ↔ x ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ↑I.toTwoSided = ↑I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ (TwoSidedIdeal.asIdeal I).toTwoSided = I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ TwoSidedIdeal.asIdeal I.toTwoSided = I

Tactic:
by

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
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x✝ : TwoSidedIdeal R
⊢ (fun I ↦
        have this := ⋯;
        (↑I).toTwoSided)
      ((fun I ↦ ⟨asIdeal I, ⋯⟩) x✝) =
    x✝

Tactic:
by

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
le : I ≤ jacobson R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I).toSemilinearMap

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : { I // I.IsTwoSided }
⊢ (fun I ↦ ⟨asIdeal I, ⋯⟩)
      ((fun I ↦
          have this := ⋯;
          (↑I).toTwoSided)
        I) =
    I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I I' : TwoSidedIdeal R
⊢ { toFun := fun I ↦ ⟨asIdeal I, ⋯⟩,
          invFun := fun I ↦
            have this := ⋯;
            (↑I).toTwoSided,
          left_inv := ⋯, right_inv := ⋯ }
        I ≤
      { toFun := fun I ↦ ⟨asIdeal I, ⋯⟩,
          invFun := fun I ↦
            have this := ⋯;
            (↑I).toTwoSided,
          left_inv := ⋯, right_inv := ⋯ }
        I' ↔
    I ≤ I'

Tactic:
by

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
le : I ≤ jacobson R
⊢ (Ideal.Quotient.mk I).toSemilinearMap.ker ≤ Module.jacobson R R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ⊥.jacobson = Ring.jacobson R

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I

Tactic:
by

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
h : jacobson (R ⧸ I) = ⊥
⊢ Module.jacobson R (R ⧸ I) = ⊥

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ ↑(Submodule.map (Ideal.Quotient.mk (jacobson R)).toSemilinearMap (jacobson R)) = ↑⊥

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
⊢ ∃ s, s * r - 1 ∈ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : N.FG
⊢ Ring.jacobson R • N < N

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ Ring.jacobson R • N
⊢ N = ⊥

Tactic:
by

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
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)
⊢ Away ((algebraMap R S) r) T

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommSemiring A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ (awayLift f r ⋯) (mk a ⟨r ^ j, ⋯⟩) = f a * v ^ j

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
a b : R
h : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
⊢ 0 ∈ nonunits R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
ι : Type u_3
s : Finset ι
f : ι → R
h : IsUnit (∑ i ∈ s, f i)
⊢ ∃ i ∈ s, IsUnit (f i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ P.IsPrime
⊢ ∃! I, I.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
a : K
h : a = 0
⊢ IsUnit (1 - a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
inst✝ : Field K
⊢ IsLocalRing K

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b x : R
hx : f x = 0
n : ℕ
hn : a ^ n * x = 0
⊢ (a * b) ^ n * x = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H : Function.Injective ⇑(awayMap f a)
⊢ Function.Injective ⇑(awayMap f b)

Tactic:
by

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I

Tactic:
contrapose hx

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ x ∉ I.jacobson
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ b m, f b = f a ^ m * a_1
b : R
x : S
c : R
m : ℕ
e : f c = f a ^ m * x
⊢ f (b ^ m * c) = f (a * b) ^ m * x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H : Function.Surjective ⇑(awayMap f a)
⊢ Function.Surjective ⇑(awayMap f b)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
by

Goal state after: