awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Artinian
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
rw₂ rw₃ : Ring.KrullDimLE 0 A ↔ Ring.KrullDimLE 0 A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
    and_iff_right this]

Premises used: Module.finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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}))

Tactic:
le_sInf fun J => exists_imp.2 fun j hj => ?_

Premises used: Iff.mpr, Set.Mem, le_sInf, exists_imp
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
Goal:
R : Type u_1
inst : CommRing R
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
⊢ LE.le.{u_1} (α := Ideal R[X]) (jacobson ⊥)
    (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal}))

Tactic:
refine le_sInf fun J => exists_imp.2 fun j hj => ?_

Premises used: Iff.mpr, le_sInf, exists_imp
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
⊢ j.IsMaximal

Tactic:
haveI : j.IsMaximal := hj.1
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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

Tactic:
Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)

Premises used: Trans.trans, Ideal.jacobson_mono, le_of_eq, bot_le
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
refine : J.jacobson = J
⊢ jacobson ⊥ ≤ J

Tactic:
refine Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)

Premises used: Trans.trans, Ideal.jacobson_mono, le_of_eq, bot_le
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 ⊥) ⊥
rw : Eq.{u_1 + 1} (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))) (jacobson ⊥) ⊥
⊢ J.jacobson = J

Tactic:
rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]

Premises used: Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot, And.right
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 (α := 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
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 ⊥)
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)
⊢ Eq.{u_1 + 1} (α := Ideal (HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C j))) (jacobson ⊥) ⊥

Tactic:
rwa [map_jacobson_of_bijective _, map_bot] at t

Premises used: Ideal.map_bot, Ideal.map_jacobson_of_bijective
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 ⊥)
⊢ 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:
RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)

Premises used: Ideal.polynomialQuotientEquivQuotientPolynomial, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 ⊥)
⊢ 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:
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)

Premises used: Ideal.polynomialQuotientEquivQuotientPolynomial, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
suffices : Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥
⊢ J.jacobson = J

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)
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 ⊥) ⊥

Tactic:
eq_bot_iff.2 fun f hf => ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
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
⊢ Eq.{u_1 + 1} (α := Ideal (R ⧸ j)[X]) (jacobson ⊥) ⊥

Tactic:
refine eq_bot_iff.2 fun f hf => ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
⊢ Ne.{u_1 + 1} (α := R ⧸ j) ((fun (x : (R ⧸ j)[X]) ↦ x.coeff 1) X) ((fun (x : (R ⧸ j)[X]) ↦ x.coeff 1) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
⊢ 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
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
r1 : Ne.{u_1 + 1} (α := (R ⧸ j)[X]) X 0
⊢ Membership.mem (γ := Submodule (R ⧸ j)[X] (R ⧸ j)[X]) ⊥ f

Tactic:
simpa [r1] using eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit ((mem_jacobson_bot.1 hf) X))

Premises used: Polynomial.eq_C_of_degree_eq_zero, Polynomial.degree_eq_zero_of_isUnit, Iff.mp, Polynomial.X, Ideal.mem_jacobson_bot
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := Ideal R[X]) (jacobson ⊥) ⊥

Tactic:
eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)

Premises used: Iff.mpr, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, eq_bot_iff, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
refine :
  LE.le.{u_1} (α := Ideal R[X]) (sInf (Set.image (α := Ideal R) (map (F := R →+* R[X]) C) {J : Ideal R | J.IsMaximal}))
    ⊥
⊢ Eq.{u_1 + 1} (α := Ideal R[X]) (jacobson ⊥) ⊥

Tactic:
refine eq_bot_iff.2 (le_trans jacobson_bot_polynomial_le_sInf_map_maximal ?_)

Premises used: Iff.mpr, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, eq_bot_iff, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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}))
    ⊥

Tactic:
fun f hf => (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n =>
    Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm

Premises used: Iff.mpr, Trans.trans, Polynomial.ext, Set.Mem, Submodule.mem_bot, Polynomial, Polynomial.coeff_zero, Eq.symm
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
Goal:
R : Type u_1
inst : CommRing R
h : Eq.{u_1 + 1} (α := Ideal R) (jacobson ⊥) ⊥
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
⊢ 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 fun f hf => (Submodule.mem_bot R[X]).2 <| Polynomial.ext fun n =>
    Trans.trans (?_ : coeff f n = 0) (coeff_zero n).symm

Premises used: Iff.mpr, Trans.trans, Polynomial.ext, Submodule.mem_bot, Polynomial, Polynomial.coeff_zero, Eq.symm
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : f.coeff n = 0), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
rwa [h, Submodule.mem_bot] at this

Premises used: Submodule.mem_bot
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 : ℕ
suffices : Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)
⊢ f.coeff n = 0

Tactic:
suffices f.coeff n ∈ Ideal.jacobson ⊥ by rwa [h, Submodule.mem_bot] at this
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 : ℕ
⊢ Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)

Tactic:
mem_sInf.2 fun j hj => (mem_map_C_iff.1 ((mem_sInf.1 hf) ⟨j, ⟨hj.2, rfl⟩⟩)) n

Premises used: Iff.mpr, Set.Mem, Ideal.mem_sInf, Ideal.mem_map_C_iff, And.right, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Jacobson.Polynomial
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 : ℕ
⊢ Membership.mem (γ := Ideal R) (jacobson ⊥) (f.coeff n)

Tactic:
exact mem_sInf.2 fun j hj => (mem_map_C_iff.1 ((mem_sInf.1 hf) ⟨j, ⟨hj.2, rfl⟩⟩)) n

Premises used: Iff.mpr, Ideal.mem_sInf, Ideal.mem_map_C_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂
rw : ⨅ (i : (↑{m : Submodule R₂ M₂ | IsCoatom m} : Type u_4)), comap f (↑i : Submodule R₂ M₂)
| comap f (jacobson R₂ M₂)

Tactic:
rw [jacobson, sInf_eq_iInf', comap_iInf]

Premises used: Module.jacobson, Submodule.comap_iInf, sInf_eq_iInf'
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂
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₂))
⊢ jacobson R M ≤ comap f (jacobson R₂ M₂)

Tactic:
conv_rhs => rw [jacobson, sInf_eq_iInf', comap_iInf]

Premises used: Module.jacobson, Submodule.comap_iInf, sInf_eq_iInf'
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂))

Tactic:
le_iInf_iff.mpr fun S m hm ↦ ?_

Premises used: Iff.mpr, Set.Mem, le_iInf_iff
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂
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₂)
⊢ 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:
refine le_iInf_iff.mpr fun S m hm ↦ ?_

Premises used: Iff.mpr, le_iInf_iff
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂)
inr : ∀ (h : comap f (↑S : Submodule R₂ M₂) = ⊤), m ∈ 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

Premises used: Submodule.isCoatom_comap_or_eq_top, Subtype.property
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
h : IsCoatom (comap f (↑S : Submodule R₂ M₂))
⊢ m ∈ comap f (↑S : Submodule R₂ M₂)

Tactic:
mem_sInf.mp hm _ h

Premises used: Iff.mp, Submodule.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
h : IsCoatom (comap f (↑S : Submodule R₂ M₂))
⊢ m ∈ comap f (↑S : Submodule R₂ M₂)

Tactic:
exact mem_sInf.mp hm _ h

Premises used: Iff.mp, Submodule.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
h : comap f (↑S : Submodule R₂ M₂) = ⊤
⊢ m ∈ comap f (↑S : Submodule R₂ M₂)

Tactic:
simpa only [h] using mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Jacobson.Radical
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₂
⊢ map f (jacobson R M) ≤ jacobson R₂ M₂

Tactic:
map_le_iff_le_comap.mpr (le_comap_jacobson f)

Premises used: Iff.mpr, Submodule.map_le_iff_le_comap, Module.le_comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
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 ⊥ ≤ ⊥
simp_rw₁ : f.ker ≤ ⊥
⊢ comap f (jacobson R₂ M₂) ≤ ⊥

Tactic:
simp_rw [h, comap_bot, (LinearMap.ker_eq_bot.mpr inj).le]

Premises used: Iff.mpr, LinearMap.ker_eq_bot, Eq.le, Submodule.comap_bot
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
⊢ f.ker ≤ ⨅ (a : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), (↑a : Submodule R M)

Tactic:
rw [jacobson, sInf_eq_iInf'] at le

Premises used: Module.jacobson, sInf_eq_iInf'
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
rw : ⨅ (i : (↑{m : Submodule R M | IsCoatom m} : Type u_3)), map f (↑i : Submodule R M)
| map f (jacobson R M)

Tactic:
rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]

Premises used: Module.jacobson, sInf_eq_iInf', Submodule.map_iInf_of_ker_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
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))
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
conv_rhs => rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]

Premises used: Module.jacobson, sInf_eq_iInf', Submodule.map_iInf_of_ker_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
⊢ 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:
le_iInf fun m ↦ sInf_le (isCoatom_map_of_ker_le surj (le_iInf_iff.mp le m) m.2)

Premises used: Set.Mem, le_iInf, le_iInf_iff, Submodule.isCoatom_map_of_ker_le, sInf_le, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
⊢ 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:
exact le_iInf fun m ↦ sInf_le (isCoatom_map_of_ker_le surj (le_iInf_iff.mp le m) m.2)

Premises used: le_iInf
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
rw₁ rw₂ : Eq (α := Submodule R M) (jacobson R M) (jacobson R M)
⊢ comap f (jacobson R₂ M₂) = jacobson R M

Tactic:
rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]

Premises used: Submodule.comap_map_eq_self, Module.map_jacobson_of_ker_le