-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem jacobson_mul_mem_right {I : Ideal R}
    (mul_mem_right : ∀ {x y}, x ∈ I → x * y ∈ I) :
    ∀ {x y}, x ∈ I.jacobson → x * y ∈ I.jacobson

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
rw [sbyr, ← mul_assoc] at y𝔪

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * b * r ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Proof state:
case pos
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
apply 𝔪.smul_mem _ r𝔪

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this : 1 - s * b ∈ 𝔪₀
⊢ 1 ∈ J

Tactic:
have : 1 - s*b + s*b ∈ J := by
  apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this✝ : 1 - s * b ∈ 𝔪₀
this : 1 - s * b + s * b ∈ J
⊢ 1 ∈ J

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this✝ : 1 - s * b ∈ 𝔪₀
this : 1 - s * b + s * b ∈ J
⊢ 1 ∈ J

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * b * r ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
simp [𝔪₀, sub_mul, y𝔪]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
⊢ ∀ {x y : R}, x ∈ I.jacobson → x * y ∈ I.jacobson

Tactic:
intro x r xJ

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
⊢ x * r ∈ I.jacobson

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ 1 ∈ J

Tactic:
have : 1 - s*b ∈ 𝔪₀ := by
  rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
  rw [sbyr, ← mul_assoc] at y𝔪
  simp [𝔪₀, sub_mul, y𝔪]

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this : 1 - s * b ∈ 𝔪₀
⊢ 1 ∈ J

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
⊢ x * r ∈ 𝔪

Tactic:
by_cases r𝔪 : r ∈ 𝔪

Result:
case pos
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∈ 𝔪
⊢ x * r ∈ 𝔪

case neg
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
⊢ x * r ∈ 𝔪

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
⊢ x * r ∈ I.jacobson

Tactic:
apply mem_sInf.mpr

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
mul_mem_right : ∀ {x y : R}, x ∈ I → x * y ∈ I
x r : R
xJ : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ I_1