mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case inl
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₂
S : ↑{m | IsCoatom m}
m : M
hm : m ∈ jacobson R M
h : IsCoatom (comap f ↑S)
⊢ m ∈ comap f ↑S

pp: case inr
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₂
S : ↑{m | IsCoatom m}
m : M
hm : m ∈ jacobson R M
h : comap f ↑S = ⊤
⊢ m ∈ comap f ↑S

Tactic:
·

Goal state after:
case inl
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₂
S : ↑{m | IsCoatom m}
m : M
hm : m ∈ jacobson R M
h : IsCoatom (comap f ↑S)
⊢ m ∈ comap f ↑S
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: case inr
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₂
S : ↑{m | IsCoatom m}
m : M
hm : m ∈ jacobson R M
h : comap f ↑S = ⊤
⊢ m ∈ comap f ↑S

Tactic:
·

Goal state after:
case inr
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₂
S : ↑{m | IsCoatom m}
m : M
hm : m ∈ jacobson R M
h : comap f ↑S = ⊤
⊢ m ∈ comap f ↑S
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 ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ) ↔
    z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
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 : ℕ
⊢ e ^ 1 * (x * e ^ n) = e ^ (n + 1) * x

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 : ℕ
⊢ e ^ (n + 1) * x = e ^ 1 * x

Tactic:
·

Goal state after:
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 : ℕ
⊢ e ^ 1 * (x * e ^ n) = e ^ (n + 1) * x
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
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 : ℕ
⊢ e ^ (n + 1) * x = e ^ 1 * x

Tactic:
·

Goal state after:
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 : ℕ
⊢ e ^ (n + 1) * x = e ^ 1 * x
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
⊢ x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_1.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
⊢ x * y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_1.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ → y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_2.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
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 ∈ span (univ * s * univ)

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (univ * s * univ)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ

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:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ
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:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
hz : z ∈ span (univ * s * univ)
⊢ z ∈ span s
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

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

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span (univ * s * univ) ↔ z ∈ AddSubgroup.closure (univ * s * univ)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ

pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
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) ≤ ⊥
t : T
⊢ ∃ n a, t * (algebraMap S T) r ^ n = (algebraMap S T) a

pp: case refine_2
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
⊢ r ^ n * x = r ^ n * y

Tactic:
·

Goal state after:
case refine_1
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) ≤ ⊥
t : T
⊢ ∃ n a, t * (algebraMap S T) r ^ n = (algebraMap S T) a
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ
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
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
⊢ r ^ n * x = r ^ n * y

Tactic:
·

Goal state after:
case refine_2
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
⊢ r ^ n * x = r ^ n * y
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))

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:
·

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

Goal state after:
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)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
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)
⊢ IsUnit ((algebraMap S T) ((algebraMap R S) r))

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:
·

Goal state after:
case refine_1
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)
⊢ IsUnit ((algebraMap S T) ((algebraMap R S) r))
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:
·

Goal state after:
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) ≤ ⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr.inl
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_max : I.IsMaximal
⊢ x ∈ I

pp: case mpr.inr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I

Tactic:
·

Goal state after:
case mpr.inl
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_max : I.IsMaximal
⊢ x ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr.inr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I

Tactic:
·

Goal state after:
case mpr.inr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

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

pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I → ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hM : (fun I ↦ I.IsMaximal) M
⊢ M ≠ ⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

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

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})