awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
simp_rw : LE.le (α := Submodule R M) ⊥ (jacobson R M)
⊢ f.ker ≤ jacobson R M

Tactic:
simp_rw [LinearMap.ker_eq_bot.mpr hf.1, bot_le]

Premises used: Iff.mpr, LinearMap.ker_eq_bot, And.left, bot_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
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
le rwa rwa₁ rwa₂ rwa₃ : N ≤ jacobson R M
⊢ N.mkQ.ker ≤ jacobson R M

Tactic:
rwa [ker_mkQ]

Premises used: Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Jacobson.Radical
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 ⊥
simp_rw₂ : jacobson R M ≤ comap N.mkQ (jacobson R (M ⧸ N))
⊢ jacobson R M ≤ N

Tactic:
simp_rw [← N.ker_mkQ, ← comap_bot, ← h, le_comap_jacobson]

Premises used: Submodule.ker_mkQ, Module.le_comap_jacobson, Submodule.comap_bot
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)) ⊥
rw₁ rw₂ : Eq.{u_3 + 1} (α := Submodule R (HasQuotient.Quotient M (B := Submodule 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))) ⊥

Tactic:
rw [jacobson_quotient_of_le le_rfl, mkQ_map_self]

Premises used: le_rfl, Module.jacobson_quotient_of_le, Submodule.mkQ_map_self
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
obtain : ∀ (m : Submodule R M) (hm : IsCoatom m), LT.lt (α := Submodule R M) (jacobson R 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

Premises used: Or.resolve_left, Bot.bot, IsCoatomic.eq_top_or_exists_le_coatom, bot_ne_top
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
m : Submodule R M
hm : IsCoatom m
⊢ LT.lt (α := Submodule R M) (jacobson R M) ⊤

Tactic:
(sInf_le <| Set.mem_setOf.mpr hm).trans_lt hm.1.lt_top

Premises used: Iff.mpr, Set.mem_setOf, And.left, Ne.lt_top, sInf_le, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
m : Submodule R M
hm : IsCoatom m
⊢ LT.lt (α := Submodule R M) (jacobson R M) ⊤

Tactic:
exact (sInf_le <| Set.mem_setOf.mpr hm).trans_lt hm.1.lt_top

Premises used: Iff.mpr, Set.mem_setOf, And.left, Ne.lt_top, sInf_le, LE.le.trans_lt
-- 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₂
inst_7 : Nontrivial M
inst_8 : Module.Finite R M
⊢ LT.lt (α := Submodule R M) (jacobson R M) ⊤

Tactic:
jacobson_lt_top R M

Premises used: Module.jacobson_lt_top
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
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))
⊢ 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))

Tactic:
simp_rw [← iInf_comap_proj, jacobson, sInf_eq_iInf', comap_iInf, le_iInf_iff]

Premises used: Module.jacobson, Submodule.comap_iInf, le_iInf_iff, sInf_eq_iInf', Submodule.iInf_comap_proj
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
i : ι
m : (↑{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) (↑m : Submodule R (M i)) : Submodule R ((i : ι) → M i))

Tactic:
iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl

Premises used: Iff.mpr, le_rfl, Set.Mem, Submodule.isCoatom_comap_iff, Subtype.mk, iInf_le_of_le, Subtype.property
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
i : ι
m : (↑{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) (↑m : Submodule R (M i)) : Submodule R ((i : ι) → M i))

Tactic:
exact iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl

Premises used: le_rfl, iInf_le_of_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)) ⊥
simp_rw₁ : LE.le (α := 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)) ⊥

Tactic:
simp_rw [h, pi_univ_bot, le_rfl]

Premises used: le_rfl, Submodule.pi_univ_bot
-- Module: Mathlib.RingTheory.Jacobson.Radical
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)
simp_rw₁ : Eq.{u_1 + 1} (α := Ideal R) (sInf {m : Submodule R R | IsCoatom m}) (sInf {I : Ideal R | I.IsMaximal})
⊢ Eq (α := Ideal R) (jacobson R) (sInf {I : Ideal R | I.IsMaximal})

Tactic:
simp_rw [jacobson, Module.jacobson, Ideal.isMaximal_def]

Premises used: Module.jacobson, Ring.jacobson, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
f : R →+* R₂
inst_2 : RingHomSurjective f
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ Ideal.IsTwoSided (jacobson R)

Tactic:
⟨fun b ha ↦ Module.le_comap_jacobson (f := LinearMap.toSpanSingleton R R b) ha⟩

Premises used: Ideal.IsTwoSided.mk, LinearMap.toSpanSingleton, Module.le_comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
m : Ideal R
inst_1 : m.IsMaximal
rw : sInf {I : Ideal R | I.IsMaximal} ≤ m
⊢ jacobson R ≤ m

Tactic:
rw [Ring.jacobson_eq_sInf_isMaximal]

Premises used: Ring.jacobson_eq_sInf_isMaximal
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
m : Ideal R
inst_1 : m.IsMaximal
⊢ sInf {I : Ideal R | I.IsMaximal} ≤ m

Tactic:
sInf_le ‹_›

Premises used: Set.Mem, sInf_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
m : Ideal R
inst_1 : m.IsMaximal
⊢ sInf {I : Ideal R | I.IsMaximal} ≤ m

Tactic:
exact sInf_le ‹_›

Premises used: sInf_le
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
f : R →+* R₂
inst_2 : RingHomSurjective f
⊢ LE.le (α := Ideal R) (jacobson R) (Ideal.comap f (jacobson R₂))

Tactic:
Module.le_comap_jacobson f.toSemilinearMap

Premises used: Set.Mem, RingHom.toSemilinearMap, Module.le_comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
f : R →+* R₂
inst_2 : RingHomSurjective f
⊢ Submodule.map f.toSemilinearMap (jacobson R) ≤ jacobson R₂

Tactic:
Module.map_jacobson_le f.toSemilinearMap

Premises used: Set.Mem, Module.map_jacobson_le, RingHom.toSemilinearMap
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
f : R →+* R₂
inst_2 : RingHomSurjective f
le : LE.le (α := Ideal R) (RingHom.ker f) (jacobson R)
⊢ Submodule.map f.toSemilinearMap (jacobson R) = jacobson R₂

Tactic:
Module.map_jacobson_of_ker_le f.surjective le

Premises used: Module.map_jacobson_of_ker_le, RingHom.surjective
-- Module: Mathlib.RingTheory.Jacobson.Radical
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' := ⋯ }
rw : (↑(Submodule.map f (Module.jacobson R (R ⧸ I))) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))
rw₁ : f.ker ≤ Module.jacobson R (R ⧸ I)
⊢ (↑(jacobson (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]

Premises used: Module.map_jacobson_of_ker_le, Function.surjective_id, Ring.jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
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' := ⋯ }
⊢ (↑(Submodule.map f (Module.jacobson R (R ⧸ I))) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))

Tactic:
apply Set.image_id

Premises used: Set.image_id
-- Module: Mathlib.RingTheory.Jacobson.Radical
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' := ⋯ }
⊢ Membership.mem (γ := Submodule R (R ⧸ I)) (Module.jacobson R (R ⧸ I)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Jacobson.Radical
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' := ⋯ }
⊢ Membership.mem (γ := Submodule R (R ⧸ I)) (Module.jacobson R (R ⧸ I)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
le : I ≤ jacobson R
⊢ Function.Surjective (α := R) (β := R ⧸ I) (⇑(RingHom.toSemilinearMap (Ideal.Quotient.mk I)) : (a : R) → R ⧸ I)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Submodule.Quotient.mk, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
le : I ≤ jacobson R
⊢ Function.Surjective (α := R) (β := R ⧸ I) (⇑(RingHom.toSemilinearMap (Ideal.Quotient.mk I)) : (a : R) → R ⧸ I)

Tactic:
exact Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
le : I ≤ jacobson R
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (le :
      LE.le.{u_1} (α := Ideal R)
        (LinearMap.ker (R₂ := R) (M₂ := R ⧸ I) (τ₁₂ := RingHom.id R) (Submodule.mkQ I) : Submodule R R)
        (jacobson R : Ideal R)),
    LinearMap.ker (τ₁₂ := Ideal.Quotient.mk I) (RingHom.toSemilinearMap (Ideal.Quotient.mk I)) ≤ Module.jacobson R R
⊢ LinearMap.ker (τ₁₂ := Ideal.Quotient.mk I) (RingHom.toSemilinearMap (Ideal.Quotient.mk I)) ≤ Module.jacobson R R

Tactic:
rwa [← I.ker_mkQ] at le

Premises used: Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h : Eq.{u_1 + 1} (α := Ideal (R ⧸ I)) (jacobson (R ⧸ I)) ⊥
rw :
  ∀ (h : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))),
    (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
⊢ Eq (α := Submodule R (R ⧸ I)) (Module.jacobson R (R ⧸ I)) ⊥

Tactic:
rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢

Premises used: le_bot_iff, SetLike.coe_subset_coe
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
rwa rwa₁ rwa₂ rwa₃ : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
⊢ (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))

Tactic:
rwa [← coe_jacobson_quotient]

Premises used: Ring.coe_jacobson_quotient
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
⊢ (↑(Submodule.map (σ₁₂ := Ideal.Quotient.mk (jacobson R)) (RingHom.toSemilinearMap (Ideal.Quotient.mk (jacobson R)))
          (jacobson R)) :
      Set (R ⧸ jacobson R)) =
    (↑⊥ : Set (R ⧸ jacobson R))

Tactic:
apply SetLike.ext'_iff.mp (jacobson R).mkQ_map_self

Premises used: Submodule.mkQ_map_self, Iff.mp, SetLike.ext'_iff, Ring.jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
inst_1 : Nontrivial R
⊢ LT.lt (α := Ideal R) (jacobson R) ⊤

Tactic:
Module.jacobson_lt_top R R

Premises used: Module.jacobson_lt_top
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (jacobson R) ⊤ ≤ Module.jacobson R M

Tactic:
Submodule.smul_le.mpr fun _ hr m _ ↦ Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr

Premises used: Iff.mpr, Set.Mem, Submodule.smul_le, LinearMap.toSpanSingleton, Module.le_comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
inst_4 : IsCoatomic.{u_3} (Submodule R M)
N : Submodule R M
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < ⊤

Tactic:
((smul_mono_right _ le_top).trans <| Ring.jacobson_smul_top_le R M).trans_lt
    (Module.jacobson_lt_top R M)

Premises used: Module.jacobson_lt_top, Ring.jacobson_smul_top_le, smul_mono_right, le_top, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : N.FG
⊢ Module.Finite.{u_1, u_3} R ↥N

Tactic:
rw [← Module.Finite.iff_fg] at fg

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ Nontrivial.{u_3} ↥N

Tactic:
rw [← nontrivial_iff_ne_bot] at ne_bot

Premises used: Submodule.nontrivial_iff_ne_bot
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite.{u_1, u_3} R ↥N
ne_bot₁ : Nontrivial.{u_3} ↥N
⊢ Module.Finite.{u_1, u_3} R ↥N

Tactic:
rw [← nontrivial_iff_ne_bot] at ne_bot

Premises used: Submodule.nontrivial_iff_ne_bot
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤) <
    Submodule.map N.subtype ⊤

Tactic:
map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)

Premises used: Submodule.jacobson_smul_lt_top, Submodule.map_strictMono_of_injective, Submodule.injective_subtype, Top.top
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h :
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)
h₁ : N = Submodule.map N.subtype ⊤
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < N

Tactic:
convert! map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)

Premises used: Submodule.jacobson_smul_lt_top, Submodule.map_strictMono_of_injective, Submodule.injective_subtype, Top.top
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h :
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)

Tactic:
rw [map_smul'']

Premises used: Submodule.map_smul''
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h :
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)

Tactic:
on_goal 1 => rw [map_smul'']

Premises used: Submodule.map_smul''
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N = HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N.subtype.range
h₁ h₂ : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N = HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)

Tactic:
rw [Submodule.map_top, range_subtype]

Premises used: Submodule.map_top, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h : N = N.subtype.range
h₁ h₂ : N = N
⊢ N = Submodule.map N.subtype ⊤

Tactic:
rw [Submodule.map_top, range_subtype]

Premises used: Submodule.map_top, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
contrapose! : ∀ (le : N ≠ ⊥), ¬N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
⊢ N = ⊥

Tactic:
contrapose! le
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N

Tactic:
(jacobson_smul_lt le fg).not_ge

Premises used: Submodule.FG.jacobson_smul_lt, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Jacobson.Radical
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N

Tactic:
exact (jacobson_smul_lt le fg).not_ge

Premises used: Submodule.FG.jacobson_smul_lt, LT.lt.not_ge
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_3
inst : CommRing R
⊢ IsJacobsonRing R ↔ ∀ (I : Ideal R), I.IsRadical → I.jacobson = I

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, IsJacobsonRing.mk, IsJacobsonRing.out'
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_3
inst : CommRing R
⊢ IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I

Tactic:
isJacobsonRing_iff.1

Premises used: Iff.mp, isJacobsonRing_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P

Tactic:
isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩

Premises used: Ideal.IsPrime.isRadical, Iff.intro, Iff.trans, isJacobsonRing_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
refine : (∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
⊢ IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P

Tactic:
refine isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩

Premises used: Iff.intro, Iff.trans, isJacobsonRing_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
⊢ (∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I

Tactic:
fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx)

Premises used: Iff.mpr, Ideal.mem_sInf, le_antisymm, And.left
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
refine :
  ∀ (h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P) (I : Ideal R) (hI : I.IsRadical) (x : R) (hx : x ∈ I.jacobson),
    x ∈ I
⊢ (∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I

Tactic:
refine fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
rw : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} I_1 → x ∈ I_1
⊢ x ∈ I

Tactic:
rw [← hI.radical, radical_eq_sInf I, mem_sInf]

Premises used: Ideal.mem_sInf, Ideal.radical_eq_sInf, Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} P
⊢ I ≤ P ∧ P.IsPrime

Tactic:
rw [Set.mem_setOf_eq] at hP

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
rw :
  ∀ (hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1)
    ⦃P : Ideal R⦄ (hP : I ≤ P ∧ P.IsPrime), x ∈ P
⊢ x ∈ P

Tactic:
rw [jacobson, mem_sInf] at hx

Premises used: Ideal.jacobson, Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
rw : ∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | P ≤ J ∧ J.IsMaximal} I → x ∈ I
⊢ x ∈ P

Tactic:
rw [← h P hP.right, jacobson, mem_sInf]

Premises used: Ideal.jacobson, Ideal.mem_sInf, And.right