awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.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
have have : ∀ (s y : R) (y𝔪 : y ∈ 𝔪) (sbyr : s * (b * r) + y = r * 1), 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 _)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.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 ∈ 𝔪₀
have sbyr₁ : y = r - s * (b * r)
Tactic: rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
Cleared hypotheses: sbyr
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.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 ∈ 𝔪₀
have y𝔪₁ : r - s * b * r ∈ 𝔪
Tactic: rw [sbyr, ← mul_assoc] at y𝔪
Cleared hypotheses: y𝔪, sbyr
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.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
have this : 1 - s * b ∈ 𝔪₀
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𝔪]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.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
have this₁ : 1 - s * b + s * b ∈ J
Tactic: have : 1 - s * b + s * b ∈ J := by
        apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ x ∈ 𝔪₀
have 𝔪₀_maximal : 𝔪₀.IsMaximal
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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
⊢ IsUnit r
have obtain : ∀ (s : R) (hs : Membership.mem (γ := Ideal R) ⊥ (s * r - 1)), IsUnit r
Tactic: obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
s : R
hs : Membership.mem (γ := Ideal R) ⊥ (s * r - 1)
⊢ IsUnit r
have hs₁ : r * s = 1
Tactic: rw [mem_bot, sub_eq_zero, mul_comm] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
⊢ (x * y + 1) * z = 1
have rwa : x * y * z + 1 * z = 1
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
⊢ (x * y + 1) * z = 1
have rwa₁ : x * y * z + z = 1
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
rwa₁ : x * y * z + z = 1
⊢ (x * y + 1) * z = 1
have rwa₂ : x * y * z + z - 1 = 0
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
rwa₁ : x * y * z + z = 1
rwa₂ : x * y * z + z - 1 = 0
⊢ (x * y + 1) * z = 1
have rwa₃ : x * z * y + z - 1 = 0
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
rwa₁ : x * y * z + z = 1
rwa₂ : x * y * z + z - 1 = 0
rwa₃ : x * z * y + z - 1 = 0
⊢ (x * y + 1) * z = 1
have rwa₄ : z * x * y + z - 1 = 0
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
rwa₁ : x * y * z + z = 1
rwa₂ : x * y * z + z - 1 = 0
rwa₃ : x * z * y + z - 1 = 0
rwa₄ : z * x * y + z - 1 = 0
⊢ (x * y + 1) * z = 1
have rwa₅ : z * y * x + z - 1 = 0
Tactic: rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.jacobson = I ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
have hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
Tactic: have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
⊢ I.jacobson = I ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
have mp : I.jacobson = I → Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
mp : I.jacobson = I → Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
⊢ I.jacobson = I ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
have mpr : Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥ → I.jacobson = I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.jacobson = I
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
have h₁ : Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson) (map (F := R →+* R ⧸ I) (Quotient.mk I) I)
Tactic: replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson) (map (F := R →+* R ⧸ I) (Quotient.mk I) I)
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
have h₁ : Eq (α := Ideal (R ⧸ I)) (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I)
Tactic: rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
⊢ I.jacobson = I
have h₁ : Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥)) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
Tactic: replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥)) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
⊢ I.jacobson = I
have h₁ : Eq (α := Ideal R) (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
  (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
Tactic: rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.radical = I.jacobson ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
have hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
Tactic: have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
⊢ I.radical = I.jacobson ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
have mp : I.radical = I.jacobson → Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
mp : I.radical = I.jacobson → Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
⊢ I.radical = I.jacobson ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
have mpr : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥) → I.radical = I.jacobson
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.radical = I.jacobson
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
have this : Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.radical)
  (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson)
Tactic: have := congr_arg (map (Ideal.Quotient.mk I)) h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.radical = I.jacobson
this :
  Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.radical)
    (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson)
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
have this₁ : Eq (α := Ideal (R ⧸ I)) (radical (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
  (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
Tactic: rw [map_radical_of_surjective hf (le_of_eq mk_ker),
      map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
⊢ I.radical = I.jacobson
have this : Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (radical ⊥))
  (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥))
Tactic: have := congr_arg (comap (Ideal.Quotient.mk I)) h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
this :
  Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (radical ⊥))
    (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥))
⊢ I.radical = I.jacobson
have this₁ : Eq (α := Ideal R) (radical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
  (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
Tactic: rw [comap_radical, comap_jacobson_of_surjective hf,
      ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpq : p + q = 1
r : R
hr : q = x * r
⊢ r * x - 1 ∈ I
have rw : -p ∈ I
Tactic: rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : TwoSidedIdeal R
⊢ Eq (α := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.jacobson : Ideal R)
    (Ideal.jacobson ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) : Ideal R)
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.jacobson : Ideal R) x ↔
    Membership.mem (γ := Ideal R) (Ideal.jacobson ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ ↔
    N₁ = N₂
have mp : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ →
  N₁ = N₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
mp :
  Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ →
    N₁ = N₂
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ ↔
    N₁ = N₂
have mpr : N₁ = N₂ →
  Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
⊢ N₁ = N₂
have this : N₂ ≤ HSMul.hSMul (α := Ideal R) 𝔪 N₂ ⊔ N₁
Tactic: have : N₂ ≤ 𝔪 • N₂ ⊔ N₁ := by
      simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ HSMul.hSMul (α := Ideal R) 𝔪 N₂ ⊔ N₁
⊢ N₁ = N₂
have this₁ : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
Tactic: rw [sup_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
⊢ LE.le (α := Ideal R) 𝔪 (Ideal.jacobson ⊥)
have h₁ : Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤
Tactic: rw [jacobson_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔ N = ⊤
have rw : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ ⊤
Tactic: rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
rw :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
      Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ ⊤
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔ N = ⊤
have rw₁ : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
    (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ.range
Tactic: rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
rw :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
      Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ ⊤
rw₁ :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
      (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ.range
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔ N = ⊤
have rw₂ : Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤
Tactic: rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
⊢ Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ ↔
    N = ⊤
have mp : Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ →
  N = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
mp :
  Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ →
    N = ⊤
⊢ Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ ↔
    N = ⊤
have mpr : N = ⊤ →
  Eq (α := Submodule R (k ⊗[R] M))
    (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
Tactic: constructor