awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : M
hx : Irreducible x ∧ (normalize : (a : M) → M) x = x ∧ x ∣ a
hy : Irreducible y ∧ (normalize : (a : M) → M) y = y ∧ y ∣ a
hxy : x ∣ y
⊢ x = y
have this : Associated x y
Tactic: have : Associated x y := hx.1.associated_of_dvd hy.1 hxy
-- 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 : ℕ
hn : n ≠ 0
⊢ primeFactors (a ^ n) = primeFactors a
have simp_rw : (normalizedFactors (a ^ n)).toFinset = (normalizedFactors a).toFinset
Tactic: simp_rw [primeFactors, normalizedFactors_pow, Multiset.toFinset_nsmul _ _ hn]
-- 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 : ℕ
hn : n ≠ 0
simp_rw : (normalizedFactors (a ^ n)).toFinset = (normalizedFactors a).toFinset
⊢ primeFactors (a ^ n) = primeFactors a
have simp_rw₁ : (n • normalizedFactors a).toFinset = (normalizedFactors a).toFinset
Tactic: simp_rw [primeFactors, normalizedFactors_pow, Multiset.toFinset_nsmul _ _ hn]
-- 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 : IsRadical a
⊢ (normalizedFactors a).Nodup
have inl : ∀ (ha : IsRadical.{u_1} (R := M) 0), Multiset.Nodup.{u_1} (α := M) (normalizedFactors 0)
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, 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 : IsRadical a
inl : ∀ (ha : IsRadical.{u_1} (R := M) 0), Multiset.Nodup.{u_1} (α := M) (normalizedFactors 0)
⊢ (normalizedFactors a).Nodup
have inr : ∀ (ha₀ : a ≠ 0), (normalizedFactors a).Nodup
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 : M
ha : IsRadical a
ha₀ : a ≠ 0
⊢ (normalizedFactors a).Nodup
have inr : Squarefree a
Tactic: rwa [← squarefree_iff_nodup_normalizedFactors ha₀, ← isRadical_iff_squarefree_of_ne_zero 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
h : IsUnit a
⊢ primeFactors a = ∅
have rw : (normalizedFactors a).toFinset = ∅
Tactic: rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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 : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
⊢ primeFactors a = ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
Tactic: rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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 : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
⊢ primeFactors a = ∅
have rw₂ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
Tactic: rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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 : IsUnit a
⊢ primeFactors a = ∅
have rw : (normalizedFactors a).toFinset = ∅
Tactic: classical
  rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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 : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
⊢ primeFactors a = ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
Tactic: classical
  rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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 : IsUnit a
rw : (normalizedFactors a).toFinset = ∅
rw₁ : Eq.{u_1 + 1} (α := Finset M) (Multiset.toFinset 0) ∅
⊢ primeFactors a = ∅
have rw₂ : Eq.{u_1 + 1} (α := Finset M) ∅ ∅
Tactic: classical
  rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]
-- 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
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
Tactic: rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw₁ : normalizedFactors a = 0 ↔ IsUnit a
Tactic: rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
rw₁ : normalizedFactors a = 0 ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw₂ : IsUnit a ↔ IsUnit a
Tactic: rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
Tactic: classical
  rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw₁ : normalizedFactors a = 0 ↔ IsUnit a
Tactic: classical
  rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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
rw : (normalizedFactors a).toFinset = ∅ ↔ IsUnit a
rw₁ : normalizedFactors a = 0 ↔ IsUnit a
⊢ primeFactors a = ∅ ↔ IsUnit a
have rw₂ : IsUnit a ↔ IsUnit a
Tactic: classical
  rw [primeFactors, Multiset.toFinset_eq_empty, normalizedFactors_eq_zero_iff 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 : IsRadical a
⊢ (primeFactors a).val = normalizedFactors a
have rw : (normalizedFactors a).Nodup
Tactic: rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
-- 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 : IsRadical a
⊢ (primeFactors a).val = normalizedFactors a
have rw : (normalizedFactors a).toFinset.val = normalizedFactors a
Tactic: classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup 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 : IsRadical a
rw : (normalizedFactors a).toFinset.val = normalizedFactors a
⊢ (primeFactors a).val = normalizedFactors a
have rw₁ : (normalizedFactors a).dedup = normalizedFactors a
Tactic: classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup 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 : IsRadical a
rw : (normalizedFactors a).toFinset.val = normalizedFactors a
rw₁ : (normalizedFactors a).dedup = normalizedFactors a
⊢ (primeFactors a).val = normalizedFactors a
have rw₂ : (normalizedFactors a).Nodup
Tactic: classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup 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
inst_3 : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b
have h : ∀ (p : M), p ∈ primeFactors (a * b) ↔ p ∈ primeFactors a ∪ primeFactors b
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
hc : IsRelPrime a b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inl : ∀ (hc : IsRelPrime 0 b), primeFactors (0 * b) = Finset.disjUnion (primeFactors 0) (primeFactors b) sorry
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a, 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
inl : ∀ (hc : IsRelPrime 0 b), primeFactors (0 * b) = Finset.disjUnion (primeFactors 0) (primeFactors b) ⋯
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr : ∀ (ha : a ≠ 0), primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) sorry
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
b : M
hc : IsRelPrime 0 b
⊢ primeFactors (0 * b) = Finset.disjUnion (primeFactors 0) (primeFactors b) ⋯
have hc₁ : IsUnit b
Tactic: rw [isRelPrime_zero_left] at 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
ha : a ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr : ∀ (hc : IsRelPrime a 0), primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) sorry
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, 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
ha : a ≠ 0
inr : ∀ (hc : IsRelPrime a 0), primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr₁ : ∀ (hb : b ≠ 0), primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) sorry
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 : M
ha : a ≠ 0
hc : IsRelPrime a 0
⊢ primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯
have hc₁ : IsUnit a
Tactic: rw [isRelPrime_zero_right] at 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
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
Tactic: rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]
-- 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
ha : a ≠ 0
hb : b ≠ 0
inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr₁ : primeFactors a ∪ primeFactors b = primeFactors a ∪ primeFactors b
Tactic: rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]
-- 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
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
Tactic: classical
  rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]
-- 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
ha : a ≠ 0
hb : b ≠ 0
inr : primeFactors (a * b) = primeFactors a ∪ primeFactors b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯
have inr₁ : primeFactors a ∪ primeFactors b = primeFactors a ∪ primeFactors b
Tactic: classical
  rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]
-- 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 : Associated a b
⊢ radical a = radical b
have rw : (primeFactors a).prod id = radical b
Tactic: rw [radical, radical, Associated.primeFactors_eq 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 : Associated a b
rw : (primeFactors a).prod id = radical b
⊢ radical a = radical b
have rw₁ : (primeFactors a).prod id = (primeFactors b).prod id
Tactic: rw [radical, radical, Associated.primeFactors_eq 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 : Associated a b
rw : (primeFactors a).prod id = radical b
rw₁ : (primeFactors a).prod id = (primeFactors b).prod id
⊢ radical a = radical b
have rw₂ : (primeFactors b).prod id = (primeFactors b).prod id
Tactic: rw [radical, radical, Associated.primeFactors_eq 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
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (radical a) a
have rw : Associated (normalizedFactors a).prod a
Tactic: rw [radical, ← Finset.prod_val, primeFactors_val_eq_normalizedFactors 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
n : ℕ
⊢ radical (a ^ n) ∣ radical a
have inl : radical (HPow.hPow (β := ℕ) a 0) ∣ radical a
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- 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 : ℕ
inl : radical (HPow.hPow (β := ℕ) a 0) ∣ radical a
⊢ radical (a ^ n) ∣ radical a
have inr : ∀ (hn : n ≠ 0), radical (a ^ n) ∣ radical a
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- 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 : ℕ
hn : n ≠ 0
⊢ radical (a ^ n) ∣ radical a
have inr : radical a ∣ radical a
Tactic: rw [radical_pow _ hn]
-- 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 ∣ a
have pos : ∀ (ha : a = 0), radical a ∣ a
Tactic: by_cases ha : 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 : M
pos : ∀ (ha : a = 0), radical a ∣ a
⊢ radical a ∣ a
have neg : ∀ (ha : ¬a = 0), radical a ∣ a
Tactic: by_cases ha : 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 : M
ha : a = 0
⊢ radical a ∣ a
have pos : Dvd.dvd.{u_1} (α := M) (radical 0) 0
Tactic: rw [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
⊢ radical a ∣ a
have neg : (primeFactors a).val.prod ∣ (normalizedFactors a).prod
Tactic: rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]
-- 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
⊢ (primeFactors a).val.prod ∣ (normalizedFactors a).prod
have neg : (primeFactors a).val ≤ normalizedFactors a
Tactic: apply Multiset.prod_dvd_prod_of_le
-- 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 ∣ a
have pos : ∀ (ha : a = 0), 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
-- 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
pos : ∀ (ha : a = 0), radical a ∣ a
⊢ radical a ∣ a
have neg : ∀ (ha : ¬a = 0), 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
-- 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 : Prime a
⊢ (normalizedFactors a).toFinset.prod id = (normalize : (a : M) → M) a
have rw : Eq (α := M) (Finset.prod (Multiset.toFinset (singleton (α := M) ((normalize : (a : M) → M) a : M))) id : M)
  ((normalize : (a : M) → M) a : M)
Tactic: rw [normalizedFactors_irreducible ha.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
ha : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical (a ^ n) = (normalize : (a : M) → M) a
have rw : radical a = (normalize : (a : M) → M) a
Tactic: rw [radical_pow a hn]
-- 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
inst_3 : Nontrivial M
⊢ radical a ≠ 0
have rw : (primeFactors a).val.prod ≠ 0
Tactic: rw [radical, ← Finset.prod_val]
-- 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
inst_3 : Nontrivial M
⊢ (primeFactors a).val.prod ≠ 0
have h : 0 ∉ (primeFactors a).val
Tactic: apply Multiset.prod_ne_zero
-- 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
inst_3 : Nontrivial M
⊢ 0 ∉ (normalizedFactors a).toFinset.val
have h : 0 ∉ normalizedFactors a
Tactic: simp only [Multiset.toFinset_val, Multiset.mem_dedup]
-- 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 : Irreducible a
hb : b ≠ 0
⊢ a ∣ radical b ↔ a ∣ b
have mp : a ∣ radical b → a ∣ b
Tactic: constructor
-- 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 : Irreducible a
hb : b ≠ 0
mp : a ∣ radical b → a ∣ b
⊢ a ∣ radical b ↔ a ∣ b
have mpr : a ∣ b → a ∣ radical b
Tactic: constructor
-- 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 : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
⊢ a ∣ radical b
have mpr : ∀ (c : M) (hc : c ∈ normalizedFactors b) (hc' : Associated a c), a ∣ radical b
Tactic: obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd hb ha 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
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ radical a ∣ p
have rw : (primeFactors a).prod id ∣ p
Tactic: 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 : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ (primeFactors a).prod id ∣ p
have a₁ : (↑(primeFactors a) : Set M).Pairwise (Function.onFun IsRelPrime id)
Tactic: apply Finset.prod_dvd_of_isRelPrime
-- 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
a₁ : (↑(primeFactors a) : Set M).Pairwise (Function.onFun IsRelPrime id)
⊢ (primeFactors a).prod id ∣ p
have a₂ : ∀ i ∈ primeFactors a, id i ∣ p
Tactic: apply Finset.prod_dvd_of_isRelPrime
-- 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 ∈ primeFactors a
⊢ id i ∣ p
have hi₁ : i ∈ normalizedFactors a
Tactic: simp only [mem_primeFactors] at hi
Cleared hypotheses: hi
-- 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
⊢ i ∣ radical a
have rw : i ∣ a
Tactic: rw [dvd_radical_iff_of_irreducible]