awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
⊢ p.count a.factors = 0 ∨ p.count b.factors = 0
have rw : p.count a.factors ≠ 0 → p.count b.factors = 0
Tactic: rw [or_iff_not_imp_left, ← Ne]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
p : Associates α
hp : Irreducible p
hca : p.count a.factors ≠ 0
⊢ p.count b.factors = 0
have contrapose! : ∀ (hcb : p.count b.factors ≠ 0), ∃ (d : Associates α), d ∣ a ∧ d ∣ b ∧ Prime d
Tactic: contrapose! hab with hcb
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have pos : ∀ (ha : a = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
pos : ∀ (ha : a = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have neg : ∀ (ha : ¬a = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have neg : ∀ (hz : p.count a.factors = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
Tactic: rcases count_of_coprime ha hb hab hp with hz | hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
neg : ∀ (hz : p.count a.factors = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have neg₁ : ∀ (hb0 : p.count b.factors = 0), p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
Tactic: rcases count_of_coprime ha hb hab hp with hz | hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have neg : ¬p.count a.factors = 0 → p.count a.factors = p.count (a * b).factors
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
have neg : p.count a.factors = p.count (a * b).factors
Tactic: apply Or.intro_right
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors = p.count (a * b).factors
have neg : p.count a.factors = p.count a.factors + p.count b.factors
Tactic: rw [count_mul ha hb hp, hb0, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
neg : p.count a.factors = p.count a.factors + p.count b.factors
⊢ p.count a.factors = p.count (a * b).factors
have neg₁ : p.count a.factors = p.count a.factors + 0
Tactic: rw [count_mul ha hb hp, hb0, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb0 : p.count b.factors = 0
neg : p.count a.factors = p.count a.factors + p.count b.factors
neg₁ : p.count a.factors = p.count a.factors + 0
⊢ p.count a.factors = p.count (a * b).factors
have neg₂ : p.count a.factors = p.count a.factors
Tactic: rw [count_mul ha hb hp, hb0, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
have pos : ∀ (ha : a = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
pos : ∀ (ha : a = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
have neg : ∀ (ha : ¬a = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
have pos : ∀ (hb : b = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
pos : ∀ (hb : b = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
have neg : ∀ (hb : ¬b = 0), p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
have neg : p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
Tactic: rw [count_mul ha hb hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
have neg : ∀ (ha0 : p.count a.factors = 0),
  p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
Tactic: rcases count_of_coprime ha hb hab hp with ha0 | hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
neg :
  ∀ (ha0 : p.count a.factors = 0),
    p.count a.factors + p.count b.factors = p.count a.factors ∨
      p.count a.factors + p.count b.factors = p.count b.factors
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
have neg₁ : ∀ (hb0 : p.count b.factors = 0),
  p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
Tactic: rcases count_of_coprime ha hb hab hp with ha0 | hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
have neg : p.count a.factors + p.count b.factors = p.count b.factors
Tactic: apply Or.intro_right
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count b.factors
have neg : 0 + p.count b.factors = p.count b.factors
Tactic: rw [ha0, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
ha0 : p.count a.factors = 0
neg : 0 + p.count b.factors = p.count b.factors
⊢ p.count a.factors + p.count b.factors = p.count b.factors
have neg₁ : p.count b.factors = p.count b.factors
Tactic: rw [ha0, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
have neg : p.count a.factors + p.count b.factors = p.count a.factors
Tactic: apply Or.intro_left
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors
have neg : p.count a.factors + 0 = p.count a.factors
Tactic: rw [hb0, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
hb0 : p.count b.factors = 0
neg : p.count a.factors + 0 = p.count a.factors
⊢ p.count a.factors + p.count b.factors = p.count a.factors
have neg₁ : p.count a.factors = p.count a.factors
Tactic: rw [hb0, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
⊢ k ∣ p.count a.factors
have pos : ∀ (ha : a = 0), k ∣ p.count a.factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
pos : ∀ (ha : a = 0), k ∣ p.count a.factors
⊢ k ∣ p.count a.factors
have neg : ∀ (ha : ¬a = 0), k ∣ p.count a.factors
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
⊢ k ∣ p.count a.factors
have neg : ∀ (hz : p.count a.factors = 0), k ∣ p.count a.factors
Tactic: rcases count_of_coprime ha hb hab hp with hz | h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
neg : ∀ (hz : p.count a.factors = 0), k ∣ p.count a.factors
⊢ k ∣ p.count a.factors
have neg₁ : ∀ (h : p.count b.factors = 0), k ∣ p.count a.factors
Tactic: rcases count_of_coprime ha hb hab hp with hz | h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ k ∣ p.count a.factors
have neg : k ∣ 0
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors
have habk₁ : k ∣ p.count a.factors + 0
Tactic: rw [count_mul ha hb hp, h] at habk
Cleared hypotheses: habk, ha, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
have zero : p.count (factors 1) = 0 * p.count a.factors
Tactic: rw [pow_zero, factors_one, zero_mul, count_zero hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
zero : p.count (factors 1) = 0 * p.count a.factors
⊢ p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
have zero₁ : p.count 0 = 0 * p.count a.factors
Tactic: rw [pow_zero, factors_one, zero_mul, count_zero hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
zero : p.count (factors 1) = 0 * p.count a.factors
zero₁ : p.count 0 = 0 * p.count a.factors
⊢ p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
have zero₂ : p.count 0 = 0
Tactic: rw [pow_zero, factors_one, zero_mul, count_zero hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
zero : p.count (factors 1) = 0 * p.count a.factors
zero₁ : p.count 0 = 0 * p.count a.factors
zero₂ : p.count 0 = 0
⊢ p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
have zero₃ : Eq (α := ℕ) 0 0
Tactic: rw [pow_zero, factors_one, zero_mul, count_zero hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
n : ℕ
h : p.count (a ^ n).factors = n * p.count a.factors
⊢ p.count (a ^ (n + 1)).factors = (n + 1) * p.count a.factors
have succ : p.count a.factors + n * p.count a.factors = (n + 1) * p.count a.factors
Tactic: rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ p.count (a ^ k).factors = k * p.count a.factors
have zero : p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
Tactic: induction k with
  | zero => rw [pow_zero, factors_one, zero_mul, count_zero hp]
  | succ n h => rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]; ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
zero : p.count (HPow.hPow (β := ℕ) a 0).factors = 0 * p.count a.factors
⊢ p.count (a ^ k).factors = k * p.count a.factors
have succ : ∀ (n : ℕ) (h : p.count (a ^ n).factors = n * p.count a.factors),
  p.count (a ^ (n + 1)).factors = (n + 1) * p.count a.factors
Tactic: induction k with
  | zero => rw [pow_zero, factors_one, zero_mul, count_zero hp]
  | succ n h => rw [pow_succ', count_mul ha (pow_ne_zero _ ha) hp, h]; ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
inst_4 : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ p.count (a ^ k).factors
have rw : k ∣ k * p.count a.factors
Tactic: rw [count_pow ha hp]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
k : ℕ
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors
⊢ ∃ (b : Associates α), a = b ^ k
have a₁ : Nontrivial α
Tactic: nontriviality α