awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑(Insert.insert a s) : Set ι).Pairwise (IsCoprime on J)
insert :
  ∀ (ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
    (hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a),
    J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ Insert.insert a s, J i) (⨅ i ∈ Insert.insert a s, J i)

Tactic:
simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]

Premises used: Finset.prod_insert, Finset.iInf_insert, ne_eq, Set.pairwise_insert, SetLike.mem_coe, forall_const, not_false_eq_true, Finset.coe_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ (↑s : Set ι).Pairwise (IsCoprime on J)

Tactic:
obtain ⟨hp1, hp2⟩ := hp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
⊢ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a

Tactic:
obtain ⟨hp1, hp2⟩ := hp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ ∀ j ∈ s, IsCoprime (J a) (J j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
insert insert₁ : J a ⊓ ⨅ j ∈ s, J j = J a ⊓ ⨅ x ∈ s, J x
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x

Tactic:
rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]

Premises used: Ideal.mul_eq_inf_of_isCoprime, Ideal.isCoprime_biInf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
empty :
  ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
insert :
  ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
    (ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
    (hp : (↑(Insert.insert a s) : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ Insert.insert a s, J i) (⨅ i ∈ Insert.insert a s, J i)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]

Premises used: Finset.prod_insert, Ideal.mul_eq_inf_of_isCoprime, Finset.iInf_insert, Insert.insert, ne_eq, Set.pairwise_insert, SetLike.mem_coe, Ideal.isCoprime_biInf, forall_const, not_false_eq_true, Finset.coe_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
empty :
  ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
insert :
  ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
    (ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
    (hp : (↑(Insert.insert a s) : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ Insert.insert a s, J i) (⨅ i ∈ Insert.insert a s, J i)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]

Premises used: Finset.prod_insert, Ideal.mul_eq_inf_of_isCoprime, Finset.iInf_insert, Insert.insert, ne_eq, Set.pairwise_insert, SetLike.mem_coe, Ideal.isCoprime_biInf, forall_const, not_false_eq_true, Finset.coe_insert
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
⊢ r ∈ I.radical ↔ ∃ (n : ℕ), r ^ n ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I ≤ I.radical

Tactic:
fun r hri => ⟨1, (pow_one r).symm ▸ hri⟩

Premises used: Set.Mem, setOf, Eq.rec, pow_one, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
rw : I.radical ≤ I ∧ I ≤ I.radical ↔ I.IsRadical
rw₁ : I.radical ≤ I ↔ I.IsRadical
rw₂ rw₃ : I.radical ≤ I ↔ I.radical ≤ I
⊢ I.radical = I ↔ I.IsRadical

Tactic:
rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]

Premises used: Ideal.le_radical, and_iff_left, le_antisymm_iff, Ideal.IsRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
k : ℕ
hk : 1 < k
⊢ I.IsRadical ↔ ∀ (r : R), r ^ k ∈ I → r ∈ I

Tactic:
⟨fun h _r hr ↦ h ⟨k, hr⟩, fun h x ⟨n, hx⟩ ↦
    k.pow_imp_self_of_one_lt hk _ (fun _ _ ↦ .inr ∘ I.smul_mem _) h n x hx⟩

Premises used: Function.comp, Membership.mem, _private.0.Ideal.isRadical_iff_pow_one_lt.match_1, Iff.intro, Exists.intro, Nat.pow_imp_self_of_one_lt, Or.inr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Ideal R) (radical ⊤) ⊤

Tactic:
(eq_top_iff_one _).2 ⟨0, Submodule.mem_top⟩

Premises used: Iff.mpr, Ideal.eq_top_iff_one, Exists.intro, OfNat.ofNat, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
H : I ≤ J
⊢ I.radical ≤ J.radical

Tactic:
fun _ ⟨n, hrni⟩ => ⟨n, H hrni⟩

Premises used: Membership.mem, _private.0.Ideal.isRadical_iff_pow_one_lt.match_1, Exists.intro, Ideal.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I.radical.IsRadical

Tactic:
fun r ⟨n, k, hrnki⟩ =>
  ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩

Premises used: HMul.hMul, Membership.mem, Eq.rec, pow_mul, _private.0.Ideal.radical_isRadical.match_1, Ideal.IsRadical, Exists.intro, Eq.symm, Ideal.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I.radical.radical = I.radical

Tactic:
(radical_isRadical I).radical

Premises used: Ideal.radical_isRadical, Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hJ : J.IsRadical
⊢ I.radical ≤ J ↔ I ≤ J

Tactic:
⟨le_trans le_radical, fun h => hJ.radical ▸ radical_mono h⟩

Premises used: Ideal.radical_mono, Ideal.le_radical, Eq.rec, Iff.intro, Ideal.IsRadical.radical, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ I.radical ≤ J.radical ↔ I ≤ J.radical

Tactic:
(radical_isRadical J).radical_le_iff

Premises used: Ideal.IsRadical.radical_le_iff, Ideal.radical_isRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I.radical = ⊤ ↔ I = ⊤

Tactic:
⟨fun h =>
    (eq_top_iff_one _).2 <|
      let ⟨n, hn⟩ := (eq_top_iff_one _).1 h
      @one_pow R _ n ▸ hn,
    fun h => h.symm ▸ radical_top R⟩

Premises used: Iff.mpr, one_pow, Membership.mem, Eq.rec, Ideal.eq_top_iff_one, Iff.intro, Iff.mp, Ideal.radical_top, OfNat.ofNat, Eq.symm, _private.0.Ideal.radical_eq_top.match_1, Ideal.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
H : I.IsPrime
⊢ I.IsRadical

Tactic:
fun _ ⟨n, hrni⟩ =>
  H.mem_of_pow_mem n hrni

Premises used: Ideal.IsPrime.mem_of_pow_mem, Membership.mem, _private.0.Ideal.isRadical_iff_pow_one_lt.match_1, Ideal.IsRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
H : I.IsPrime
⊢ I.radical = I

Tactic:
IsRadical.radical H.isRadical

Premises used: Ideal.IsPrime.isRadical, Ideal.IsRadical.radical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
x : R
m : ℕ
hx : x ^ m ∈ I.radical
⊢ x ∈ I.radical

Tactic:
radical_idem I ▸ ⟨m, hx⟩

Premises used: Ideal.radical_idem, Eq.rec, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
⊢ Disjoint (↑(Submonoid.powers y) : Set R) (↑I : Set R) ↔ y ∉ I

Tactic:
⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _),
      fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩

Premises used: Iff.mpr, Set.disjoint_left, disjoint_iff, Iff.intro, Iff.mp, Submonoid.mem_powers, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
refine : ∀ (h : y ∉ I), (↑(Submonoid.powers y) : Set R) ⊓ (↑I : Set R) ≤ ⊥
⊢ Disjoint (↑(Submonoid.powers y) : Set R) (↑I : Set R) ↔ y ∉ I

Tactic:
refine ⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _),
      fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I
n : ℕ
hx' : (fun (x : ℕ) ↦ y ^ x) n ∈ (↑I : Set R)
⊢ Membership.mem (γ := Set R) ⊥ ((fun (x : ℕ) ↦ y ^ x) n)

Tactic:
h (hI <| mem_radical_of_pow_mem <| le_radical hx')

Premises used: Set.Mem, Ideal.le_radical, Ideal.mem_radical_of_pow_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
h : y ∉ I
n : ℕ
hx' : (fun (x : ℕ) ↦ y ^ x) n ∈ (↑I : Set R)
⊢ Membership.mem (γ := Set R) ⊥ ((fun (x : ℕ) ↦ y ^ x) n)

Tactic:
exact h (hI <| mem_radical_of_pow_mem <| le_radical hx')

Premises used: Ideal.le_radical, Ideal.mem_radical_of_pow_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
y : R
⊢ Disjoint (↑(Submonoid.powers y) : Set R) (↑I : Set R) ↔ y ∉ I

Tactic:
disjoint_powers_iff_notMem y (IsPrime.isRadical ‹_›)

Premises used: Ideal.disjoint_powers_iff_notMem, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
le_antisymm (radical_mono <| sup_le_sup le_radical le_radical) <|
    radical_le_radical_iff.2 <| sup_le (radical_mono le_sup_left) (radical_mono le_sup_right)

Premises used: Ideal.radical_mono, Iff.mpr, sup_le_sup, le_sup_left, Ideal.le_radical, le_sup_right, le_antisymm, Ideal.radical_le_radical_iff, sup_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical

Tactic:
le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right))
    fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right _ hrm,
      (pow_add r m n).symm ▸ J.mul_mem_left _ hrn⟩

Premises used: Ideal.radical_mono, pow_add, Membership.mem, inf_le_right, Eq.rec, _private.0.Ideal.radical_inf.match_1, le_inf, le_antisymm, HPow.hPow, HAdd.hAdd, Ideal.mul_mem_right, And.intro, Exists.intro, inf_le_left, Ideal.mul_mem_left, Eq.symm, Ideal.radical, Min.min
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
rw : I.radical ⊓ J.radical ≤ I ⊓ J
⊢ (I ⊓ J).IsRadical

Tactic:
rw [IsRadical, radical_inf]

Premises used: Ideal.radical_inf, Ideal.IsRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J

Tactic:
inf_le_inf hI hJ

Premises used: inf_le_inf, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J

Tactic:
exact inf_le_inf hI hJ

Premises used: inf_le_inf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
⊢ IsRadical.{u} (R := R) ⊥ ↔ IsReduced R

Tactic:
simp only [IsRadical, SetLike.le_def, Ideal.mem_radical_iff, Ideal.mem_bot,
    forall_exists_index, isReduced_iff, IsNilpotent]

Premises used: Ideal.mem_bot, isReduced_iff, SetLike.le_def, forall_exists_index, Ideal.IsRadical, Ideal.mem_radical_iff, IsNilpotent
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
inst_1 rwa rwa₁ rwa₂ rwa₃ : IsReduced R
⊢ IsRadical.{u} (R := R) ⊥

Tactic:
rwa [Ideal.isRadical_bot_iff]

Premises used: Ideal.isRadical_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ (radicalInfTopHom : (a : Ideal R) → Ideal R) I = I.radical

Tactic:
rfl

Premises used: Ideal.radical, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
rw : s.inf' ⋯ ((⇑radicalInfTopHom : (a : Ideal R) → Ideal R) ∘ f) = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]

Premises used: map_finset_inf, Exists.intro, Ideal.radicalInfTopHom_apply, Finset.inf'_eq_inf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ ((⇑radicalInfTopHom : (a : Ideal R) → Ideal R) ∘ f) = (f i).radical

Tactic:
Finset.inf'_eq_of_forall _ _ hs

Premises used: Finset.inf'_eq_of_forall
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ ((⇑radicalInfTopHom : (a : Ideal R) → Ideal R) ∘ f) = (f i).radical

Tactic:
exact Finset.inf'_eq_of_forall _ _ hs

Premises used: Finset.inf'_eq_of_forall
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_2
I : ι → Ideal R
⊢ LE.le.{u} (α := Ideal R) (radical (⨅ (i : ι), I i)) (⨅ (i : ι), (I i).radical)

Tactic:
le_iInf fun _ ↦ radical_mono (iInf_le _ _)

Premises used: Ideal.radical_mono, Set.Mem, le_iInf, iInf_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Sort u_2
I : ι → Ideal R
hI : ∀ (i : ι), (I i).IsRadical
⊢ IsRadical.{u} (R := R) (⨅ (i : ι), I i)

Tactic:
(radical_iInf_le I).trans (iInf_mono hI)

Premises used: iInf_mono, Ideal.IsRadical, Ideal.radical_iInf_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
refine : (I * J).radical ≤ I.radical ⊓ J.radical
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I * J).radical ≤ (I ⊓ J).radical

Tactic:
have := radical_mono <| mul_le_inf (I := I) (J := J)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ (I ⊓ J).radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
simp_rw [radical_inf I J] at this

Premises used: Ideal.radical_inf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
this : (I * J).radical ≤ I.radical ⊓ J.radical
⊢ (I * J).radical ≤ I.radical ⊓ J.radical

Tactic:
assumption
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hJ : J.IsPrime
⊢ I.radical ≤ J ↔ I ≤ J

Tactic:
IsRadical.radical_le_iff hJ.isRadical

Premises used: Ideal.IsRadical.radical_le_iff, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
rw : x ∈ m ⊔ span {x}
⊢ x ∈ m

Tactic:
rw [hm.eq_of_le hrmx le_sup_left]

Premises used: le_sup_left, Maximal.eq_of_le
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
⊢ x ∈ m ⊔ span {x}

Tactic:
Submodule.mem_sup_right <| mem_span_singleton_self x

Premises used: Set.Mem, setOf, Submodule.mem_sup_right, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
⊢ x ∈ m ⊔ span {x}

Tactic:
exact Submodule.mem_sup_right <| mem_span_singleton_self x

Premises used: Submodule.mem_sup_right, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) ⊤
hrm : r ∉ radical ⊤
this : ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r
⊢ r ∉ ⊤

Tactic:
rw [radical_top] at hrm

Premises used: Ideal.radical_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) ⊤
hrm : r ∉ radical ⊤
this : ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r
hrm₁ : r ∉ ⊤
⊢ ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r

Tactic:
rw [radical_top] at hrm

Premises used: Ideal.radical_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r
⊢ False

Tactic:
hrm trivial

Premises used: trivial
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
hIm : I ≤ ⊤
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) ⊤
hrm : r ∉ ⊤
this : ∀ x ∉ ⊤, Membership.mem (γ := Ideal R) (radical (⊤ ⊔ span {x})) r
⊢ False

Tactic:
exact hrm trivial

Premises used: trivial
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : Membership.mem (γ := Submodule R R) (span {y}) g
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
rw : p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m
⊢ r ^ (n + k) ∈ m

Tactic:
rw [pow_add, ← hpqrn, ← hcxq, ← hfgrk, ← hdyg, add_mul, mul_add (c * x),
                      mul_assoc c x (d * y), mul_left_comm x, ← mul_assoc]

Premises used: add_mul, HMul.hMul, mul_assoc, pow_add, mul_left_comm, mul_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : Membership.mem (γ := Submodule R R) (span {y}) g
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m

Tactic:
m.add_mem (m.mul_mem_right _ hpm)
                    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))

Premises used: Set.Mem, Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
this : ∀ x ∉ m, r ∈ (m ⊔ span {x}).radical
x y : R
hxym : x * y ∈ m
hxm : x ∉ m
hym : y ∉ m
n : ℕ
hrn : r ^ n ∈ m ⊔ span {x}
p : R
hpm : p ∈ m
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpqrn : p + q = r ^ n
c : R
hcxq : c * x = q
k : ℕ
hrk : r ^ k ∈ m ⊔ span {y}
f : R
hfm : f ∈ m
g : R
hg : Membership.mem (γ := Submodule R R) (span {y}) g
hfgrk : f + g = r ^ k
d : R
hdyg : d * y = g
⊢ p * (f + d * y) + (c * x * f + c * d * (x * y)) ∈ m

Tactic:
refine
                    m.add_mem (m.mul_mem_right _ hpm)
                    (m.add_mem (m.mul_mem_left _ hfm) (m.mul_mem_left _ hxym))

Premises used: Ideal.add_mem, Ideal.mul_mem_right, Ideal.mul_mem_left