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
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
a₁ : (↑(primeFactors a) : Set M).Pairwise (Function.onFun IsRelPrime id)
a₂ : ∀ i ∈ primeFactors a, id i ∣ p
⊢ (primeFactors a).prod id ∣ p

Tactic:
apply Finset.prod_dvd_of_isRelPrime

Premises used: Finset.prod_dvd_of_isRelPrime
-- 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
⊢ (↑(primeFactors a) : Set M).Pairwise (Function.onFun IsRelPrime id)

Tactic:
pairwise_primeFactors_isRelPrime

Premises used: UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime
-- 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
⊢ (↑(primeFactors a) : Set M).Pairwise (Function.onFun IsRelPrime id)

Tactic:
exact pairwise_primeFactors_isRelPrime

Premises used: UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime
-- 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
i : M
hi : i ∈ primeFactors a
⊢ i ∈ normalizedFactors a

Tactic:
simp only [mem_primeFactors] at hi

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 : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
rw : i ∣ a
ha₁ : Irreducible i
hb : a ≠ 0
⊢ i ∣ radical a

Tactic:
rw [dvd_radical_iff_of_irreducible]

Premises used: UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible
-- 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
i : M
hi : i ∈ normalizedFactors a
⊢ i ∣ a

Tactic:
dvd_of_mem_normalizedFactors hi

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
-- 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
i : M
hi : i ∈ normalizedFactors a
⊢ i ∣ a

Tactic:
exact dvd_of_mem_normalizedFactors hi

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
-- 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
i : M
hi : i ∈ normalizedFactors a
⊢ Irreducible i

Tactic:
irreducible_of_normalized_factor i hi

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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
i : M
hi : i ∈ normalizedFactors a
⊢ Irreducible i

Tactic:
exact irreducible_of_normalized_factor i hi

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
n : ℕ
p i : M
ha : radical 0 ∣ p ^ n
hi : Membership.mem (γ := Multiset M) (normalizedFactors 0) i
⊢ False

Tactic:
simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi

Premises used: Multiset.notMem_zero, UniqueFactorizationMonoid.normalizedFactors_zero
-- 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
i : M
hi : i ∈ normalizedFactors a
⊢ i ∣ radical a

Tactic:
have : i ∣ radical a := by
    rw [dvd_radical_iff_of_irreducible]
    · exact dvd_of_mem_normalizedFactors hi
    · exact irreducible_of_normalized_factor i hi
    · rintro rfl
      simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi
-- 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
i : M
hi : i ∈ normalizedFactors a
this : i ∣ radical a
⊢ id i ∣ p

Tactic:
(prime_of_normalized_factor i hi).isRadical n p (this.trans ha)

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor, Prime.isRadical, 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
i : M
hi : i ∈ normalizedFactors a
this : i ∣ radical a
⊢ id i ∣ p

Tactic:
exact (prime_of_normalized_factor i hi).isRadical n p (this.trans ha)

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor, Prime.isRadical, 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
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : Nontrivial M
⊢ radical a ≠ 0

Tactic:
simp [radical_ne_zero]

Premises used: UniqueFactorizationMonoid.radical_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
h : Nontrivial M
⊢ Squarefree (radical a)

Tactic:
exact isRadical_radical.squarefree (by simp [radical_ne_zero])

Premises used: UniqueFactorizationMonoid.isRadical_radical, IsRadical.squarefree
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
inl : Eq.{u_1 + 1} (α := Finset M) (primeFactors (radical 0)) (primeFactors 0)
inr : ∀ (ha₀ : a ≠ 0), primeFactors (radical a) = primeFactors a
⊢ primeFactors (radical a) = primeFactors a

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
⊢ Eq.{u_1 + 1} (α := Finset M) (primeFactors (radical 0)) (primeFactors 0)

Tactic:
simp [primeFactors]

Premises used: 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
⊢ Nontrivial M

Tactic:
have : Nontrivial M := ⟨a, 0, 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
this : Nontrivial M
inr : ∀ (p : M), p ∈ primeFactors (radical a) ↔ p ∈ primeFactors a
⊢ primeFactors (radical a) = primeFactors a

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 : M
ha₀ : a ≠ 0
this : Nontrivial M
p : M
⊢ p ∈ primeFactors (radical a) ↔ p ∈ primeFactors a

Tactic:
simp +contextual [mem_primeFactors, mem_normalizedFactors_iff',
    dvd_radical_iff_of_irreducible, ha₀]

Premises used: UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible, 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
h : radical a = radical b
rw : primeFactors (radical b) = primeFactors b
⊢ primeFactors a = primeFactors b

Tactic:
rw [← primeFactors_radical, h]

Premises used: UniqueFactorizationMonoid.primeFactors_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 : radical a = radical b
⊢ primeFactors (radical b) = primeFactors b

Tactic:
primeFactors_radical

Premises used: UniqueFactorizationMonoid.primeFactors_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 : radical a = radical b
⊢ primeFactors (radical b) = primeFactors b

Tactic:
exact primeFactors_radical

Premises used: UniqueFactorizationMonoid.primeFactors_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 : primeFactors a = primeFactors b
⊢ radical a = radical b

Tactic:
simp [radical, h]

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 : M
h : a = 0 ∨ IsUnit a
⊢ a = 0 → radical a = 1

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
refine : radical a = 1 → a = 0 ∨ IsUnit a
⊢ radical a = 1 ↔ a = 0 ∨ IsUnit a

Tactic:
refine ⟨?_, (Or.elim · (by simp +contextual) radical_of_isUnit)⟩
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : radical a = 1
rw : ¬a = 0 → IsUnit a
⊢ a = 0 ∨ IsUnit a

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
rw : primeFactors (radical a) = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset M) (primeFactors 1) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
⊢ primeFactors a = ∅

Tactic:
rw [← primeFactors_radical, h, primeFactors_one]

Premises used: UniqueFactorizationMonoid.primeFactors_one, UniqueFactorizationMonoid.primeFactors_radical
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ primeFactors a = ∅

Tactic:
have : primeFactors a = ∅ := by rw [← primeFactors_radical, h, primeFactors_one]
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
this : primeFactors a = ∅
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : IsUnit a), IsUnit a
⊢ IsUnit a

Tactic:
rwa [primeFactors_eq_empty_iff ha] at this

Premises used: UniqueFactorizationMonoid.primeFactors_eq_empty_iff
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ radical (radical a) = radical a

Tactic:
radical_eq_iff_primeFactors_eq.mpr primeFactors_radical

Premises used: Iff.mpr, UniqueFactorizationMonoid.primeFactors_radical, UniqueFactorizationMonoid.radical_eq_iff_primeFactors_eq
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical 0 ∣ radical b ↔ normalizedFactors 0 ⊆ normalizedFactors b
inr : ∀ (ha₀ : a ≠ 0), radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors 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
⊢ radical 0 ∣ radical b ↔ normalizedFactors 0 ⊆ normalizedFactors b

Tactic:
simp
-- 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₀ : a ≠ 0
⊢ Nontrivial M

Tactic:
have : Nontrivial M := ⟨a, 0, ha₀⟩
-- 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₀ : a ≠ 0
this : Nontrivial M
inr : normalizedFactors (radical a) ⊆ normalizedFactors (radical b) ↔ normalizedFactors a ⊆ normalizedFactors b
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors radical_ne_zero radical_ne_zero,
    Multiset.le_iff_subset (normalizedFactors_nodup isRadical_radical)]

Premises used: Multiset.le_iff_subset, UniqueFactorizationMonoid.isRadical_radical, UniqueFactorizationMonoid.radical_ne_zero, UniqueFactorizationMonoid.normalizedFactors_nodup, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_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₀ : a ≠ 0
this : Nontrivial M
⊢ normalizedFactors (radical a) ⊆ normalizedFactors (radical b) ↔ normalizedFactors a ⊆ normalizedFactors b

Tactic:
simp only [Multiset.subset_iff, ← mem_primeFactors, primeFactors_radical]

Premises used: UniqueFactorizationMonoid.mem_primeFactors, Multiset.subset_iff, UniqueFactorizationMonoid.primeFactors_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
rw : normalizedFactors a ⊆ normalizedFactors b ↔ primeFactors a ⊆ primeFactors b
rw₁ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ primeFactors b
rw₂ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset
rw₃ rw₄ : normalizedFactors a ⊆ normalizedFactors b ↔ normalizedFactors a ⊆ normalizedFactors b
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

Tactic:
rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]

Premises used: UniqueFactorizationMonoid.primeFactors, Multiset.toFinset_subset, UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_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
rw : normalizedFactors a ⊆ normalizedFactors b ↔ primeFactors a ⊆ primeFactors b
rw₁ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ primeFactors b
rw₂ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset
rw₃ rw₄ : normalizedFactors a ⊆ normalizedFactors b ↔ normalizedFactors a ⊆ normalizedFactors b
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

Tactic:
classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]

Premises used: UniqueFactorizationMonoid.primeFactors, Multiset.toFinset_subset, UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_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
h : a ∣ b
hb₀ : b ≠ 0
inl : ∀ (h : 0 ∣ b), radical 0 ∣ radical b
inr : ∀ (ha₀ : a ≠ 0), radical a ∣ radical b
⊢ radical a ∣ radical 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
hb₀ : b ≠ 0
h : 0 ∣ b
⊢ radical 0 ∣ radical b

Tactic:
simp
-- 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 : a ∣ b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ normalizedFactors a ≤ normalizedFactors b

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h

Premises used: UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_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
h : a ∣ b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
h₁ : normalizedFactors a ≤ normalizedFactors b
⊢ b ≠ 0

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h

Premises used: UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_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
h : a ∣ b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
h₁ : normalizedFactors a ≤ normalizedFactors b
hb₁ : b ≠ 0
⊢ a ≠ 0

Tactic:
rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h

Premises used: UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_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
h : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
inr : normalizedFactors a ⊆ normalizedFactors b
⊢ radical a ∣ radical b

Tactic:
rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]

Premises used: UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_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
h : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors b

Tactic:
Multiset.subset_of_le h

Premises used: Multiset.subset_of_le
-- 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 : normalizedFactors a ≤ normalizedFactors b
hb₀ : b ≠ 0
ha₀ : a ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors b

Tactic:
exact Multiset.subset_of_le h

Premises used: Multiset.subset_of_le
-- 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 : IsRadical a
hb₀ : b ≠ 0
⊢ a ∣ radical b ↔ a ∣ b

Tactic:
⟨fun ha' ↦ ha'.trans radical_dvd_self, fun hab ↦ ?_⟩

Premises used: UniqueFactorizationMonoid.radical_dvd_self, Iff.intro, 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 : IsRadical a
hb₀ : b ≠ 0
refine : ∀ (hab : a ∣ b), a ∣ radical b
⊢ a ∣ radical b ↔ a ∣ b

Tactic:
refine ⟨fun ha' ↦ ha'.trans radical_dvd_self, fun hab ↦ ?_⟩
-- 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 : IsRadical a
hb₀ : b ≠ 0
hab : a ∣ b
inl : ∀ (ha : IsRadical.{u_1} (R := M) 0) (hab : 0 ∣ b), 0 ∣ radical b
inr : ∀ (ha₀ : a ≠ 0), a ∣ radical b
⊢ a ∣ radical 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
hb₀ : b ≠ 0
ha : IsRadical.{u_1} (R := M) 0
hab : 0 ∣ b
⊢ 0 ∣ radical b

Tactic:
simp_all
-- 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 : IsRadical a
hb₀ : b ≠ 0
hab : a ∣ b
ha₀ : a ≠ 0
⊢ a ∣ radical b

Tactic:
(ha.dvd_radical ha₀).trans (radical_dvd_radical hab hb₀)

Premises used: IsRadical.dvd_radical, UniqueFactorizationMonoid.radical_dvd_radical, 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 : IsRadical a
hb₀ : b ≠ 0
hab : a ∣ b
ha₀ : a ≠ 0
⊢ a ∣ radical b

Tactic:
exact (ha.dvd_radical ha₀).trans (radical_dvd_radical hab hb₀)

Premises used: IsRadical.dvd_radical, UniqueFactorizationMonoid.radical_dvd_radical, 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
hb : b ≠ 0
rw : radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
rw₁ rw₂ : primeFactors a ⊆ primeFactors b ↔ primeFactors a ⊆ primeFactors b
⊢ radical a ∣ b ↔ primeFactors a ⊆ primeFactors b

Tactic:
rw [← dvd_radical_iff isRadical_radical hb,
    radical_dvd_radical_iff_primeFactors_subset_primeFactors]

Premises used: UniqueFactorizationMonoid.dvd_radical_iff, UniqueFactorizationMonoid.isRadical_radical, UniqueFactorizationMonoid.radical_dvd_radical_iff_primeFactors_subset_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
simp_rw : (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id
⊢ radical (a * b) = radical a * radical b

Tactic:
simp_rw [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
hc : IsRelPrime a b
rw : ((primeFactors a).disjUnion (primeFactors b) ⋯).prod id = (primeFactors a).prod id * (primeFactors b).prod id
rw₁ rw₂ :
  HMul.hMul (α := M) (∏ x ∈ primeFactors a, id x) (∏ x ∈ primeFactors b, id x) =
    (primeFactors a).prod id * (primeFactors b).prod id
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Tactic:
rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]

Premises used: UniqueFactorizationMonoid.primeFactors_mul_eq_disjUnion, Finset.prod_disjUnion, UniqueFactorizationMonoid.disjoint_primeFactors
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
h : (↑∅ : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))

Tactic:
simp
-- Module: Mathlib.RingTheory.Radical.Basic
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih :
  ∀ (h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
h : (↑(Finset.cons i s his) : Set ι).Pairwise (Function.onFun IsRelPrime f)
cons : radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ Finset.cons i s his, f i)) (∏ i ∈ Finset.cons i s his, radical (f i))

Tactic:
simp only [Finset.prod_cons]

Premises used: Finset.prod_cons