awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ha : IsRadical.{u_1} (R := M) 0
⊢ Multiset.Nodup.{u_1} (α := M) (normalizedFactors 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha₀ : a ≠ 0
inr : Squarefree a
inr₁ inr₂ inr₃ inr₄ : IsRadical a
⊢ (normalizedFactors a).Nodup

Tactic:
rwa [← squarefree_iff_nodup_normalizedFactors ha₀, ← isRadical_iff_squarefree_of_ne_zero ha₀]

Premises used: isRadical_iff_squarefree_of_ne_zero, UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
⊢ primeFactors a = ∅

Tactic:
rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]

Premises used: UniqueFactorizationMonoid.normalizedFactors_of_isUnit, Multiset.toFinset_zero, UniqueFactorizationMonoid.primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
⊢ primeFactors a = ∅

Tactic:
classical
  rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]

Premises used: UniqueFactorizationMonoid.normalizedFactors_of_isUnit, Multiset.toFinset_zero, UniqueFactorizationMonoid.primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
rw₁ : normalizedFactors a = 0 ↔ IsUnit a
rw₂ rw₃ : IsUnit a ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a

Tactic:
rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff ha]

Premises used: Multiset.toFinset_eq_empty, UniqueFactorizationMonoid.primeFactors, UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
rw₁ : normalizedFactors a = 0 ↔ IsUnit a
rw₂ rw₃ : IsUnit a ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a

Tactic:
classical
  rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff ha]

Premises used: Multiset.toFinset_eq_empty, UniqueFactorizationMonoid.primeFactors, UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
rw : (normalizedFactors a).Nodup
⊢ (primeFactors a).val = normalizedFactors a

Tactic:
rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]

Premises used: Multiset.dedup_eq_self, UniqueFactorizationMonoid.primeFactors, Multiset.toFinset_val
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (normalizedFactors a).Nodup

Tactic:
normalizedFactors_nodup ha

Premises used: UniqueFactorizationMonoid.normalizedFactors_nodup
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (normalizedFactors a).Nodup

Tactic:
exact normalizedFactors_nodup ha

Premises used: UniqueFactorizationMonoid.normalizedFactors_nodup
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
rw : (normalizedFactors a).toFinset.val = normalizedFactors a
rw₁ : (normalizedFactors a).dedup = normalizedFactors a
rw₂ rw₃ rw₄ : (normalizedFactors a).Nodup
⊢ (primeFactors a).val = normalizedFactors a

Tactic:
classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup ha

Premises used: Multiset.dedup_eq_self, UniqueFactorizationMonoid.normalizedFactors_nodup, UniqueFactorizationMonoid.primeFactors, Multiset.toFinset_val
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inst_3 : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : M), p ∈ primeFactors (a * b) ↔ p ∈ primeFactors a ∪ primeFactors b
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b

Tactic:
ext p
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inst_3 : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
p : M
⊢ p ∈ primeFactors (a * b) ↔ p ∈ primeFactors a ∪ primeFactors b

Tactic:
simp [mem_normalizedFactors_iff', mem_primeFactors, ha, hb]

Premises used: UniqueFactorizationMonoid.mem_primeFactors, UniqueFactorizationMonoid.mem_normalizedFactors_iff'
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Premises used: Iff.mpr, UniqueFactorizationMonoid.disjoint_normalizedFactors, Multiset.disjoint_toFinset, UniqueFactorizationMonoid.primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Premises used: Iff.mpr, UniqueFactorizationMonoid.disjoint_normalizedFactors, Multiset.disjoint_toFinset
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ Disjoint (primeFactors a) (primeFactors b)

Tactic:
classical
  exact Multiset.disjoint_toFinset.mpr (disjoint_normalizedFactors hc)

Premises used: Iff.mpr, UniqueFactorizationMonoid.disjoint_normalizedFactors, Multiset.disjoint_toFinset
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
inl : ∀ (hc : IsRelPrime 0 b), primeFactors (0 * b) = Finset.disjUnion (primeFactors 0) (primeFactors b) ⋯
inr : ∀ (ha : a ≠ 0), primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
b : M
hc : IsRelPrime 0 b
⊢ IsUnit b

Tactic:
rw [isRelPrime_zero_left] at hc

Premises used: isRelPrime_zero_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
b : M
hc_1 : IsRelPrime 0 b
hc : IsUnit b
⊢ primeFactors (0 * b) = Finset.disjUnion (primeFactors 0) (primeFactors b) ⋯

Tactic:
simp only [zero_mul, primeFactors_zero, Finset.empty_disjUnion, primeFactors_of_isUnit hc]

Premises used: UniqueFactorizationMonoid.primeFactors_zero, Finset.empty_disjUnion, MulZeroClass.zero_mul, disjoint_bot_left, UniqueFactorizationMonoid.primeFactors_of_isUnit
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
inr : ∀ (hc : IsRelPrime a 0), primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯
inr₁ : ∀ (hb : b ≠ 0), primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
hc : IsRelPrime a 0
⊢ IsUnit a

Tactic:
rw [isRelPrime_zero_right] at hc

Premises used: isRelPrime_zero_right
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
hc_1 : IsRelPrime a 0
hc : IsUnit a
⊢ primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯

Tactic:
simp only [mul_zero, primeFactors_zero, primeFactors_of_isUnit hc, Finset.disjUnion_empty]

Premises used: UniqueFactorizationMonoid.primeFactors_zero, Finset.disjUnion_empty, disjoint_bot_right, MulZeroClass.mul_zero, UniqueFactorizationMonoid.primeFactors_of_isUnit
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
inr₁ inr₂ : primeFactors a ∪ primeFactors b = primeFactors a ∪ primeFactors b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]

Premises used: UniqueFactorizationMonoid.primeFactors_mul_eq_union, Finset.disjUnion_eq_union
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
inr₁ inr₂ : primeFactors a ∪ primeFactors b = primeFactors a ∪ primeFactors b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
classical
  rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]

Premises used: Finset.disjUnion_eq_union
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
⊢ Eq.{u_1 + 1} (α := M) (radical 0) 1

Tactic:
simp [radical]

Premises used: UniqueFactorizationMonoid.radical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
⊢ Eq.{u_1 + 1} (α := M) (radical 1) 1

Tactic:
simp [radical]

Premises used: UniqueFactorizationMonoid.radical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
h : Associated a b
rw : (primeFactors a).prod id = radical b
rw₁ : (primeFactors a).prod id = (primeFactors b).prod id
rw₂ rw₃ : (primeFactors b).prod id = (primeFactors b).prod id
⊢ radical a = radical b

Tactic:
rw [radical, radical, Associated.primeFactors_eq h]

Premises used: UniqueFactorizationMonoid.radical, Associated.primeFactors_eq
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
rw : Associated (normalizedFactors a).prod a
⊢ Associated (radical a) a

Tactic:
rw [radical, ← Finset.prod_val, primeFactors_val_eq_normalizedFactors ha]

Premises used: Finset.prod_val, UniqueFactorizationMonoid.radical, UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (normalizedFactors a).prod a

Tactic:
prod_normalizedFactors ha'

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (normalizedFactors a).prod a

Tactic:
exact prod_normalizedFactors ha'

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ a ∣ radical a

Tactic:
(radical_associated ha ha').dvd'

Premises used: UniqueFactorizationMonoid.radical_associated, Associated.dvd'
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : IsUnit a
⊢ radical a = 1

Tactic:
(radical_eq_of_associated (associated_one_iff_isUnit.mpr h)).trans radical_one

Premises used: Iff.mpr, associated_one_iff_isUnit, UniqueFactorizationMonoid.radical_eq_of_associated, UniqueFactorizationMonoid.radical_one, Eq.trans
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a u : M
h : IsUnit u
⊢ radical (u * a) = radical a

Tactic:
radical_eq_of_associated (associated_unit_mul_left _ _ h)

Premises used: UniqueFactorizationMonoid.radical_eq_of_associated, associated_unit_mul_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a u : M
h : IsUnit u
⊢ radical (a * u) = radical a

Tactic:
radical_eq_of_associated (associated_mul_unit_left _ _ h)

Premises used: UniqueFactorizationMonoid.radical_eq_of_associated, associated_mul_unit_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
n : ℕ
inl : radical (HPow.hPow (β := ℕ) a 0) ∣ radical a
inr : ∀ (hn : n ≠ 0), radical (a ^ n) ∣ radical a
⊢ radical (a ^ n) ∣ radical a

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ radical (HPow.hPow (β := ℕ) a 0) ∣ radical a

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : n ≠ 0
inr inr₁ : radical a ∣ radical a
⊢ radical (a ^ n) ∣ radical a

Tactic:
rw [radical_pow _ hn]

Premises used: UniqueFactorizationMonoid.radical_pow
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
pos : ∀ (ha : a = 0), radical a ∣ a
neg : ∀ (ha : ¬a = 0), radical a ∣ a
⊢ radical a ∣ a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a = 0
pos : Dvd.dvd.{u_1} (α := M) (radical 0) 0
⊢ radical a ∣ a

Tactic:
rw [ha]
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ Dvd.dvd.{u_1} (α := M) (radical 0) 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
neg : (primeFactors a).val.prod ∣ (normalizedFactors a).prod
⊢ radical a ∣ a

Tactic:
rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]

Premises used: Finset.prod_val, UniqueFactorizationMonoid.radical, UniqueFactorizationMonoid.prod_normalizedFactors, Associated.dvd_iff_dvd_right
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
neg : (primeFactors a).val ≤ normalizedFactors a
⊢ (primeFactors a).val.prod ∣ (normalizedFactors a).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (normalizedFactors a).dedup ≤ normalizedFactors a

Tactic:
apply Multiset.dedup_le

Premises used: Multiset.dedup_le
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
pos : ∀ (ha : a = 0), radical a ∣ a
neg neg₁ : ∀ (ha : ¬a = 0), radical a ∣ a
⊢ radical a ∣ a

Tactic:
classical
  by_cases ha : a = 0
  · rw [ha]
    apply dvd_zero
  · rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le
    rw [primeFactors, Multiset.toFinset_val]
    apply Multiset.dedup_le

Premises used: dvd_zero, Multiset.prod_dvd_prod_of_le, Finset.prod_val, UniqueFactorizationMonoid.radical, Multiset.dedup_le, UniqueFactorizationMonoid.primeFactors, Multiset.toFinset_val
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : Prime a
rw :
  Eq (α := M) (Finset.prod (Multiset.toFinset (singleton (α := M) ((normalize : (a : M) → M) a : M))) id : M)
    ((normalize : (a : M) → M) a : M)
⊢ (normalizedFactors a).toFinset.prod id = (normalize : (a : M) → M) a

Tactic:
rw [normalizedFactors_irreducible ha.irreducible]

Premises used: Prime.irreducible, UniqueFactorizationMonoid.normalizedFactors_irreducible
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ Eq (α := M) (Finset.prod (Multiset.toFinset (singleton (α := M) ((normalize : (a : M) → M) a : M))) id : M)
    ((normalize : (a : M) → M) a : M)

Tactic:
simp only [Multiset.toFinset_singleton, id, Finset.prod_singleton]

Premises used: Finset.prod_singleton, id, Multiset.toFinset_singleton
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : n ≠ 0
rw : radical a = (normalize : (a : M) → M) a
⊢ radical (a ^ n) = (normalize : (a : M) → M) a

Tactic:
rw [radical_pow a hn]

Premises used: UniqueFactorizationMonoid.radical_pow
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical a = (normalize : (a : M) → M) a

Tactic:
radical_of_prime ha

Premises used: UniqueFactorizationMonoid.radical_of_prime
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical a = (normalize : (a : M) → M) a

Tactic:
exact radical_of_prime ha

Premises used: UniqueFactorizationMonoid.radical_of_prime
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inst_3 : Nontrivial M
rw : (primeFactors a).val.prod ≠ 0
⊢ radical a ≠ 0

Tactic:
rw [radical, ← Finset.prod_val]

Premises used: Finset.prod_val, UniqueFactorizationMonoid.radical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inst_3 : Nontrivial M
h : 0 ∉ (primeFactors a).val
⊢ (primeFactors a).val.prod ≠ 0

Tactic:
apply Multiset.prod_ne_zero

Premises used: Multiset.prod_ne_zero
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inst_3 : Nontrivial M
h : 0 ∉ normalizedFactors a
⊢ 0 ∉ (normalizedFactors a).toFinset.val

Tactic:
simp only [Multiset.toFinset_val, Multiset.mem_dedup]

Premises used: Multiset.mem_dedup, Multiset.toFinset_val
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inst_3 : Nontrivial M
⊢ 0 ∉ normalizedFactors a

Tactic:
zero_notMem_normalizedFactors _

Premises used: UniqueFactorizationMonoid.zero_notMem_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inst_3 : Nontrivial M
⊢ 0 ∉ normalizedFactors a

Tactic:
exact zero_notMem_normalizedFactors _

Premises used: UniqueFactorizationMonoid.zero_notMem_normalizedFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
mp : a ∣ radical b → a ∣ b
mpr : a ∣ b → a ∣ radical b
⊢ a ∣ radical b ↔ a ∣ b

Tactic:
constructor
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha_1 : Irreducible a
hb : b ≠ 0
ha : a ∣ radical b
⊢ a ∣ b

Tactic:
ha.trans radical_dvd_self

Premises used: UniqueFactorizationMonoid.radical_dvd_self, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha_1 : Irreducible a
hb : b ≠ 0
ha : a ∣ radical b
⊢ a ∣ b

Tactic:
exact ha.trans radical_dvd_self

Premises used: UniqueFactorizationMonoid.radical_dvd_self, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
mpr : ∀ (c : M) (hc : c ∈ normalizedFactors b) (hc' : Associated a c), a ∣ radical b
⊢ a ∣ radical b

Tactic:
obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd hb ha ha'

Premises used: UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
c : M
hc : c ∈ normalizedFactors b
hc' : Associated a c
⊢ c ∈ primeFactors b

Tactic:
simpa [mem_primeFactors] using hc

Premises used: UniqueFactorizationMonoid.mem_primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
c : M
hc : c ∈ normalizedFactors b
hc' : Associated a c
⊢ a ∣ radical b

Tactic:
exact hc'.dvd.trans (Finset.dvd_prod_of_mem _ (by simpa [mem_primeFactors] using hc))

Premises used: Associated.dvd, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
rw : (primeFactors a).prod id ∣ p
⊢ radical a ∣ p

Tactic:
rw [radical]

Premises used: UniqueFactorizationMonoid.radical