-- 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:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x * r ∈ 𝔪

Tactic:
suffices x ∈ 𝔪₀ by simpa [𝔪₀] using this

Result:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x ∈ 𝔪₀

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 ≤ 𝔪₀
⊢ 𝔪₀.IsMaximal

Tactic:
refine isMaximal_iff.mpr ⟨
  fun h => r𝔪 (by simpa [𝔪₀] using h),
  fun J b 𝔪₀J b𝔪₀ 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
⊢ 1 ∈ J

Proof state:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ x ∈ 𝔪₀

Tactic:
have 𝔪₀_maximal : IsMaximal 𝔪₀ := by
  refine isMaximal_iff.mpr ⟨
    fun h => r𝔪 (by simpa [𝔪₀] using h),
    fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩
  let K : Ideal R := Ideal.span {b*r} ⊔ 𝔪
  have ⟨s, y, y𝔪, sbyr⟩ :=
    mem_span_singleton_sup.mp <|
      mul_mem_left _ r <|
        (isMaximal_iff.mp 𝔪_mem.right).right K (b*r)
        le_sup_right b𝔪₀
        (mem_sup_left <| mem_span_singleton_self _)
  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𝔪]
  have : 1 - s*b + s*b ∈ J := by
    apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)
  simpa using this

Result:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀

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} ⊔ 𝔪
⊢ 1 ∈ J

Tactic:
have ⟨s, y, y𝔪, sbyr⟩ :=
  mem_span_singleton_sup.mp <|
    mul_mem_left _ r <|
      (isMaximal_iff.mp 𝔪_mem.right).right K (b*r)
      le_sup_right b𝔪₀
      (mem_sup_left <| mem_span_singleton_self _)

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
⊢ 1 ∈ J

Proof state:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀

Tactic:
exact mem_sInf.mp xJ ⟨I𝔪₀, 𝔪₀_maximal⟩

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
⊢ 1 ∈ J

Tactic:
let K : Ideal R := Ideal.span {b*r} ⊔ 𝔪

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} ⊔ 𝔪
⊢ 1 ∈ J

Proof state:
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 ∈ 𝔪

Tactic:
let 𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R (S := Rᵐᵒᵖ) R (.op r)) 𝔪

Result:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op 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
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ I_1

Tactic:
intro 𝔪 𝔪_mem

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}
⊢ x * r ∈ 𝔪

Proof state:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x ∈ 𝔪₀

Tactic:
have I𝔪₀ : I ≤ 𝔪₀ := fun i iI =>
  𝔪_mem.left (mul_mem_right iI)

Result:
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 ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ x ∈ 𝔪₀

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 - s * b + s * b ∈ J

Tactic:
apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)

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 ≤ 𝔪₀
h : 1 ∈ 𝔪₀
⊢ r ∈ 𝔪

Tactic:
simpa [𝔪₀] using h

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)) 𝔪
this : x ∈ 𝔪₀
⊢ x * r ∈ 𝔪

Tactic:
simpa [𝔪₀] using this

Result:
no goals