awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ i ∣ radical a
have ha₁ : Irreducible i
Tactic: rw [dvd_radical_iff_of_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ i ∣ radical a
have hb : a ≠ 0
Tactic: rw [dvd_radical_iff_of_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
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
⊢ id i ∣ p
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ Squarefree (radical a)
have a₁ : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ primeFactors (radical a) = primeFactors a
have inl : Eq.{u_1 + 1} (α := Finset M) (primeFactors (radical 0)) (primeFactors 0)
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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)
⊢ primeFactors (radical a) = primeFactors a
have inr : ∀ (ha₀ : a ≠ 0), primeFactors (radical a) = primeFactors a
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
⊢ primeFactors (radical a) = primeFactors a
have this : Nontrivial M
Tactic: have : Nontrivial M := ⟨a, 0, ha₀⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
this : Nontrivial M
⊢ primeFactors (radical a) = primeFactors a
have inr : ∀ (p : M), p ∈ primeFactors (radical a) ↔ p ∈ primeFactors a
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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 a = primeFactors b
have rw : primeFactors (radical b) = primeFactors b
Tactic: rw [← primeFactors_radical, h]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
⊢ radical a = 1 ↔ a = 0 ∨ IsUnit a
have refine : radical a = 1 → a = 0 ∨ IsUnit a
Tactic: refine ⟨?_, (Or.elim · (by simp +contextual) radical_of_isUnit)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a : M
h : radical a = 1
⊢ a = 0 ∨ IsUnit a
have rw : ¬a = 0 → IsUnit a
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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 = ∅
have rw : primeFactors (radical a) = ∅
Tactic: rw [← primeFactors_radical, h, primeFactors_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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) = ∅
⊢ primeFactors a = ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset M) (primeFactors 1) ∅
Tactic: rw [← primeFactors_radical, h, primeFactors_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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) ∅
⊢ primeFactors a = ∅
have rw₂ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
Tactic: rw [← primeFactors_radical, h, primeFactors_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
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
⊢ IsUnit a
have this : primeFactors a = ∅
Tactic: have : primeFactors a = ∅ := by rw [← primeFactors_radical, h, primeFactors_one]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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 = ∅
⊢ IsUnit a
have rwa : ∀ (this : IsUnit a), IsUnit a
Tactic: rwa [primeFactors_eq_empty_iff ha] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
have inl : radical 0 ∣ radical b ↔ normalizedFactors 0 ⊆ normalizedFactors b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
have inr : ∀ (ha₀ : a ≠ 0), radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha₀ : a ≠ 0
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
have this : Nontrivial M
Tactic: have : Nontrivial M := ⟨a, 0, ha₀⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ normalizedFactors a ⊆ normalizedFactors b
have inr : normalizedFactors (radical a) ⊆ normalizedFactors (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)]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw : normalizedFactors a ⊆ normalizedFactors b ↔ primeFactors a ⊆ primeFactors b
Tactic: rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₁ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ primeFactors b
Tactic: rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₂ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset
Tactic: rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₃ : normalizedFactors a ⊆ normalizedFactors b ↔ normalizedFactors a ⊆ normalizedFactors b
Tactic: rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw : normalizedFactors a ⊆ normalizedFactors b ↔ primeFactors a ⊆ primeFactors b
Tactic: classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₁ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ primeFactors b
Tactic: classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₂ : normalizedFactors a ⊆ normalizedFactors b ↔ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset
Tactic: classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
have rw₃ : normalizedFactors a ⊆ normalizedFactors b ↔ normalizedFactors a ⊆ normalizedFactors b
Tactic: classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b
have inl : ∀ (h : 0 ∣ b), radical 0 ∣ radical b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b
have inr : ∀ (ha₀ : a ≠ 0), radical a ∣ radical b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
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
⊢ radical a ∣ radical b
have h₁ : normalizedFactors a ≤ normalizedFactors b
Tactic: rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h
Cleared hypotheses: h, hb₀, ha₀
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ radical b
have inr : normalizedFactors a ⊆ normalizedFactors b
Tactic: rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
have refine : ∀ (hab : a ∣ b), a ∣ radical b
Tactic: refine ⟨fun ha' ↦ ha'.trans radical_dvd_self, fun hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ a ∣ radical b
have inl : ∀ (ha : IsRadical.{u_1} (R := M) 0) (hab : 0 ∣ b), 0 ∣ radical b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ a ∣ radical b
have inr : ∀ (ha₀ : a ≠ 0), a ∣ radical b
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hb : b ≠ 0
⊢ radical a ∣ b ↔ primeFactors a ⊆ primeFactors b
have rw : radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b
Tactic: rw [← dvd_radical_iff isRadical_radical hb,
    radical_dvd_radical_iff_primeFactors_subset_primeFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ radical a ∣ b ↔ primeFactors a ⊆ primeFactors b
have rw₁ : primeFactors a ⊆ primeFactors b ↔ primeFactors a ⊆ primeFactors b
Tactic: rw [← dvd_radical_iff isRadical_radical hb,
    radical_dvd_radical_iff_primeFactors_subset_primeFactors]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ radical (a * b) = radical a * radical b
have simp_rw : (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id
Tactic: simp_rw [radical]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id
have rw : ((primeFactors a).disjUnion (primeFactors b) sorry).prod id = (primeFactors a).prod id * (primeFactors b).prod id
Tactic: rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id
have rw₁ : HMul.hMul (α := M) (∏ x ∈ primeFactors a, id x) (∏ x ∈ primeFactors b, id x) =
  (primeFactors a).prod id * (primeFactors b).prod id
Tactic: rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ Finset.cons i s his, f i)) (∏ i ∈ Finset.cons i s his, radical (f i))
have cons : radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
Tactic: simp only [Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
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)
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
have h₁ : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b
Tactic: rw [Finset.coe_cons,
      Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
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 : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ (↑s : Set ι), Function.onFun IsRelPrime f i b
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
have cons : IsRelPrime (f i) (∏ i ∈ s, f i)
Tactic: rw [radical_mul, ih h.1]
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
s : Finset ι
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
have empty : ∀ (h : (↑∅ : Set ι).Pairwise (Function.onFun IsRelPrime f)),
  Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s his ih =>
    simp only [Finset.prod_cons]
    rw [Finset.coe_cons,
      Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h
    rw [radical_mul, ih h.1]
    exact IsRelPrime.prod_right h.2
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
s : Finset ι
h : (↑s : Set ι).Pairwise (Function.onFun IsRelPrime f)
empty :
  ∀ (h : (↑∅ : Set ι).Pairwise (Function.onFun IsRelPrime f)),
    Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ ∅, f i)) (∏ i ∈ ∅, radical (f i))
⊢ Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ s, f i)) (∏ i ∈ s, radical (f i))
have cons : ∀ (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)),
  Eq.{u_1 + 1} (α := M) (radical (∏ i ∈ Finset.cons i s his, f i)) (∏ i ∈ Finset.cons i s his, radical (f i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s his ih =>
    simp only [Finset.prod_cons]
    rw [Finset.coe_cons,
      Set.pairwise_insert_of_symmetric_of_notMem (symmetric_isRelPrime.comap _) (by simpa)] at h
    rw [radical_mul, ih h.1]
    exact IsRelPrime.prod_right h.2
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ radical (a * b) ∣ radical a * radical b
have inl : radical (0 * b) ∣ radical 0 * radical b
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
inl : radical (0 * b) ∣ radical 0 * radical b
⊢ radical (a * b) ∣ radical a * radical b
have inr : ∀ (ha : a ≠ 0), radical (a * b) ∣ radical a * radical b
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ radical (a * b) ∣ radical a * radical b
have inr : radical (a * 0) ∣ radical a * radical 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
inr : radical (a * 0) ∣ radical a * radical 0
⊢ radical (a * b) ∣ radical a * radical b
have inr₁ : ∀ (hb : b ≠ 0), radical (a * b) ∣ radical a * radical b
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
⊢ radical (a * b) ∣ radical a * radical b
have a₁ : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.Radical.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : NormalizationMonoid M
inst_2 : UniqueFactorizationMonoid M
a b : M
⊢ radical (a * b) ∣ radical a * radical b
have inl : radical (0 * b) ∣ radical 0 * radical b
Tactic: classical
  obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]
Cleared hypotheses: a