awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Artinian (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsArtinianRing R
this : IsNoetherianRing A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A
have rw : IsArtinianRing A ↔ Ring.KrullDimLE 0 A
Tactic: rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Artinian (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsArtinianRing R
this : IsNoetherianRing A
rw : IsArtinianRing A ↔ Ring.KrullDimLE 0 A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A
have rw₁ : IsNoetherianRing A ∧ Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A
Tactic: rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Artinian (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.FiniteType R A
inst_4 : IsArtinianRing R
this : IsNoetherianRing A
rw : IsArtinianRing A ↔ Ring.KrullDimLE 0 A
rw₁ : IsNoetherianRing A ∧ Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A
have rw₂ : Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A
Tactic: rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ LE.le.{u_1} (α := Ideal R[X]) (jacobson ⊥)
    (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal}))
have refine : ∀ (J : Ideal R[X]) (j : Ideal R)
  (hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J),
  jacobson ⊥ ≤ J
Tactic: refine le_sInf fun J => exists_imp.2 fun j hj => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
⊢ jacobson ⊥ ≤ J
have this : j.IsMaximal
Tactic: haveI : j.IsMaximal := hj.1
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
⊢ jacobson ⊥ ≤ J
have refine : J.jacobson = J
Tactic: refine Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
t : Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥
⊢ J.jacobson = J
have rw : Eq.{u_1 + 1} (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))) (jacobson ⊥) ⊥
Tactic: rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
t : Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))) (jacobson ⊥) ⊥
have t₁ : Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j)))
  (map (R := (R ⧸ j)[X]) j.polynomialQuotientEquivQuotientPolynomial.toRingHom (jacobson ⊥))
  (map (R := (R ⧸ j)[X]) j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥)
Tactic: replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
t :
  Eq (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j)))
    (map (R := (R ⧸ j)[X]) j.polynomialQuotientEquivQuotientPolynomial.toRingHom (jacobson ⊥))
    (map (R := (R ⧸ j)[X]) j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥)
⊢ Eq.{u_1 + 1} (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))) (jacobson ⊥) ⊥
have rwa : Function.Bijective (α := (R ⧸ j)[X]) (β := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))
  (⇑j.polynomialQuotientEquivQuotientPolynomial.toRingHom : (a : (R ⧸ j)[X]) → R[X] ⧸ map C j)
Tactic: rwa [map_jacobson_of_bijective _, map_bot] at t
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
⊢ J.jacobson = J
have suffices : Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥
Tactic: suffices t : (⊥ : Ideal (Polynomial (R ⧸ j))).jacobson = ⊥ by
    rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
    replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
    rwa [map_jacobson_of_bijective _, map_bot] at t
    exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
⊢ Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥
have refine : ∀ (f : (R ⧸ j)[X]) (hf : Membership.mem (γ := Submodule (R ⧸ j)[X] (R ⧸ j)[X]) (jacobson ⊥) f),
  Membership.mem (γ := Submodule (R ⧸ j)[X] (R ⧸ j)[X]) ⊥ f
Tactic: refine eq_bot_iff.2 fun f hf => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R[X]
j : Ideal R
hj : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | J.IsMaximal} j ∧ map (F := R →+* R[X]) C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : Membership.mem (γ := Submodule (R ⧸ j)[X] (R ⧸ j)[X]) (jacobson ⊥) f
⊢ Membership.mem (γ := Submodule (R ⧸ j)[X] (R ⧸ j)[X]) ⊥ f
have r1 : Ne.{u_1 + 1} (α := (R ⧸ j)[X]) X 0
Tactic: have r1 : (X : (R ⧸ j)[X]) ≠ 0 := ne_of_apply_ne (coeff · 1) <| by simp
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := Ideal R[X]) (jacobson ⊥) ⊥
have refine : LE.le.{u_1} (α := Ideal R[X]) (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal})) ⊥
Tactic: refine eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
⊢ LE.le.{u_1} (α := Ideal R[X]) (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal}))
    ⊥
have refine : ∀ (f : R[X])
  (hf :
    Membership.mem (γ := Submodule R[X] R[X])
      (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal})) f)
  (n : ℕ), f.coeff n = 0
Tactic: refine fun f hf => (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n =>
    Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
f : R[X]
hf :
  Membership.mem (γ := Submodule R[X] R[X])
    (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal})) f
n : ℕ
this : Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)
⊢ f.coeff n = 0
have rwa : ∀ (this : Membership.mem (γ := Ideal R) ⊥ (f.coeff n)), f.coeff n = 0
Tactic: rwa [h, Submodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
f : R[X]
hf :
  Membership.mem (γ := Submodule R[X] R[X])
    (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal})) f
n : ℕ
this : Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)
rwa : ∀ (this : Membership.mem (γ := Ideal R) ⊥ (f.coeff n)), f.coeff n = 0
⊢ f.coeff n = 0
have rwa₁ : ∀ (this : f.coeff n = 0), f.coeff n = 0
Tactic: rwa [h, Submodule.mem_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
f : R[X]
hf :
  Membership.mem (γ := Submodule R[X] R[X])
    (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal})) f
n : ℕ
⊢ f.coeff n = 0
have suffices : Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)
Tactic: suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
| comap f (jacobson R₂ M₂)
have rw : ⨅ (i : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)), comap f (↑i : Submodule R₂ M₂)
Tactic: rw [jacobson, sInf_eq_iInf', comap_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ jacobson R M ≤ comap f (jacobson R₂ M₂)
have conv_rhs : LE.le (α := Submodule R M) (jacobson R M)
  (⨅ (i : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)), comap f (↑i : Submodule R₂ M₂))
Tactic: conv_rhs => rw [jacobson, sInf_eq_iInf', comap_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ LE.le (α := Submodule R M) (jacobson R M)
    (⨅ (i : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)), comap f (↑i : Submodule R₂ M₂))
have refine : ∀ (S : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)) (m : M)
  (hm : Membership.mem (γ := Submodule R M) (jacobson R M) m), m ∈ comap f (↑S : Submodule R₂ M₂)
Tactic: refine le_iInf_iff.mpr fun S m hm ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)
m : M
hm : Membership.mem (γ := Submodule R M) (jacobson R M) m
⊢ m ∈ comap f (↑S : Submodule R₂ M₂)
have inl : ∀ (h : IsCoatom (comap f (↑S : Submodule R₂ M₂))), m ∈ comap f (↑S : Submodule R₂ M₂)
Tactic: obtain h | h := isCoatom_comap_or_eq_top f S.2
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)
m : M
hm : Membership.mem (γ := Submodule R M) (jacobson R M) m
inl : ∀ (h : IsCoatom (comap f (↑S : Submodule R₂ M₂))), m ∈ comap f (↑S : Submodule R₂ M₂)
⊢ m ∈ comap f (↑S : Submodule R₂ M₂)
have inr : ∀ (h : comap f (↑S : Submodule R₂ M₂) = ⊤), m ∈ comap f (↑S : Submodule R₂ M₂)
Tactic: obtain h | h := isCoatom_comap_or_eq_top f S.2
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : Eq (α := Submodule R₂ M₂) (jacobson R₂ M₂) ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥
have simp_rw : comap f ⊥ ≤ ⊥
Tactic: simp_rw [h, comap_bot, (LinearMap.ker_eq_bot.mpr inj).le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
inj : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : Eq (α := Submodule R₂ M₂) (jacobson R₂ M₂) ⊥
simp_rw : comap f ⊥ ≤ ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥
have simp_rw₁ : f.ker ≤ ⊥
Tactic: simp_rw [h, comap_bot, (LinearMap.ker_eq_bot.mpr inj).le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
le : f.ker ≤ jacobson R M
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)
have le₁ : f.ker ≤ ⨅ (a : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), (↑a : Submodule R M)
Tactic: rw [jacobson, sInf_eq_iInf'] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
le : f.ker ≤ ⨅ (a : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), (↑a : Submodule R M)
| map f (jacobson R M)
have rw : ⨅ (i : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), map f (↑i : Submodule R M)
Tactic: rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
le : f.ker ≤ ⨅ (a : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), (↑a : Submodule R M)
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)
have conv_rhs : LE.le (α := Submodule R₂ M₂) (jacobson R₂ M₂)
  (⨅ (i : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), map f (↑i : Submodule R M))
Tactic: conv_rhs => rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
le : f.ker ≤ jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M
have rw : comap f (map f (jacobson R M)) = jacobson R M
Tactic: rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
le : f.ker ≤ jacobson R M
rw : comap f (map f (jacobson R M)) = jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M
have rw₁ : Eq (α := Submodule R M) (jacobson R M) (jacobson R M)
Tactic: rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ f.ker ≤ jacobson R M
have simp_rw : LE.le (α := Submodule R M) ⊥ (jacobson R M)
Tactic: simp_rw [LinearMap.ker_eq_bot.mpr hf.1, bot_le]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
h : Eq.{u_3 + 1} (α := Submodule R (M ⧸ N)) (jacobson R (M ⧸ N)) ⊥
⊢ jacobson R M ≤ N
have simp_rw : jacobson R M ≤ N.mkQ.ker
Tactic: simp_rw [← N.ker_mkQ, ← comap_bot, ← h, le_comap_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
h : Eq.{u_3 + 1} (α := Submodule R (M ⧸ N)) (jacobson R (M ⧸ N)) ⊥
simp_rw : jacobson R M ≤ N.mkQ.ker
⊢ jacobson R M ≤ N
have simp_rw₁ : jacobson R M ≤ comap N.mkQ ⊥
Tactic: simp_rw [← N.ker_mkQ, ← comap_bot, ← h, le_comap_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
h : Eq.{u_3 + 1} (α := Submodule R (M ⧸ N)) (jacobson R (M ⧸ N)) ⊥
simp_rw : jacobson R M ≤ N.mkQ.ker
simp_rw₁ : jacobson R M ≤ comap N.mkQ ⊥
⊢ jacobson R M ≤ N
have simp_rw₂ : jacobson R M ≤ comap N.mkQ (jacobson R (M ⧸ N))
Tactic: simp_rw [← N.ker_mkQ, ← comap_bot, ← h, le_comap_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_3 + 1} (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M)))
    (jacobson R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M))) ⊥
have rw : Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M)))
  (map (mkQ (jacobson R M)) (jacobson R M)) ⊥
Tactic: rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M)))
    (map (mkQ (jacobson R M)) (jacobson R M)) ⊥
⊢ Eq.{u_3 + 1} (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M)))
    (jacobson R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M))) ⊥
have rw₁ : Eq.{u_3 + 1} (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (jacobson R M))) ⊥ ⊥
Tactic: rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsCoatomic.{u_3} (Submodule R M)
⊢ LT.lt (α := Submodule R M) (jacobson R M) ⊤
have obtain : ∀ (m : Submodule R M) (hm : IsCoatom m), LT.lt (α := Submodule R M) (jacobson R M) ⊤
Tactic: obtain ⟨m, hm, -⟩ := (eq_top_or_exists_le_coatom (⊥ : Submodule R M)).resolve_left bot_ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_6
M : ι → Type u_5
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
⊢ LE.le (α := Submodule R ((i : ι) → M i)) (jacobson R ((i : ι) → M i) : Submodule R ((i : ι) → M i))
    (pi (φ := M) Set.univ fun (x : ι) ↦ jacobson R (M x) : Submodule R ((i : ι) → M i))
have simp_rw : ∀ (i : ι) (i_1 : (↑{m : Submodule R (M i) | IsCoatom m} : Type u_5)),
  LE.le (α := Submodule R ((i : ι) → M i))
    (⨅ (a : (↑{m : Submodule R ((i : ι) → M i) | IsCoatom m} : Type (max u_5 u_6))),
        (↑a : Submodule R ((i : ι) → M i)) :
      Submodule R ((i : ι) → M i))
    (comap (LinearMap.proj (φ := M) i) (↑i_1 : Submodule R (M i)) : Submodule R ((i : ι) → M i))
Tactic: simp_rw [← iInf_comap_proj, jacobson, sInf_eq_iInf', comap_iInf, le_iInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_6
M : ι → Type u_5
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
h : ∀ (i : ι), Eq.{u_5 + 1} (α := Submodule R (M i)) (jacobson R (M i)) ⊥
⊢ LE.le (α := Submodule R ((i : ι) → M i))
    (pi (φ := M) Set.univ fun (x : ι) ↦ jacobson R (M x) : Submodule R ((i : ι) → M i)) ⊥
have simp_rw : LE.le (α := Submodule R ((i : ι) → M i)) (pi (φ := M) Set.univ fun (x : ι) ↦ ⊥ : Submodule R ((i : ι) → M i)) ⊥
Tactic: simp_rw [h, pi_univ_bot, le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
ι : Type u_6
M : ι → Type u_5
inst_1 : (i : ι) → AddCommGroup (M i)
inst_2 : (i : ι) → Module.{u_1, u_5} R (M i)
h : ∀ (i : ι), Eq.{u_5 + 1} (α := Submodule R (M i)) (jacobson R (M i)) ⊥
simp_rw :
  LE.le (α := Submodule R ((i : ι) → M i)) (pi (φ := M) Set.univ fun (x : ι) ↦ ⊥ : Submodule R ((i : ι) → M i)) ⊥
⊢ LE.le (α := Submodule R ((i : ι) → M i))
    (pi (φ := M) Set.univ fun (x : ι) ↦ jacobson R (M x) : Submodule R ((i : ι) → M i)) ⊥
have simp_rw₁ : LE.le (α := Submodule R ((i : ι) → M i)) ⊥ ⊥
Tactic: simp_rw [h, pi_univ_bot, le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ Eq (α := Ideal R) (jacobson R) (sInf {I : Ideal R | I.IsMaximal})
have simp_rw : Eq (α := Ideal R) (Module.jacobson R R : Submodule R R) (sInf {I : Ideal R | I.IsMaximal} : Ideal R)
Tactic: simp_rw [jacobson, Module.jacobson, Ideal.isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
simp_rw : Eq (α := Ideal R) (Module.jacobson R R : Submodule R R) (sInf {I : Ideal R | I.IsMaximal} : Ideal R)
⊢ Eq (α := Ideal R) (jacobson R) (sInf {I : Ideal R | I.IsMaximal})
have simp_rw₁ : Eq.{u_1 + 1} (α := Ideal R) (sInf {m : Submodule R R | IsCoatom m}) (sInf {I : Ideal R | I.IsMaximal})
Tactic: simp_rw [jacobson, Module.jacobson, Ideal.isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
m : Ideal R
inst_1 : m.IsMaximal
⊢ jacobson R ≤ m
have rw : sInf {I : Ideal R | I.IsMaximal} ≤ m
Tactic: rw [Ring.jacobson_eq_sInf_isMaximal]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))
have rw : (↑(Submodule.map f (Module.jacobson R (R ⧸ I))) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))
Tactic: rw [jacobson, ← Module.map_jacobson_of_ker_le (f := f) Function.surjective_id]