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 : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors
have succ : (a ^ n * a).factors = (n + 1) • a.factors
Tactic: rw [pow_succ, succ_nsmul, factors_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
succ : (a ^ n * a).factors = (n + 1) • a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors
have succ₁ : (a ^ n * a).factors = n • a.factors + a.factors
Tactic: rw [pow_succ, succ_nsmul, factors_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
succ : (a ^ n * a).factors = (n + 1) • a.factors
succ₁ : (a ^ n * a).factors = n • a.factors + a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors
have succ₂ : (a ^ n).factors + a.factors = n • a.factors + a.factors
Tactic: rw [pow_succ, succ_nsmul, factors_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
succ : (a ^ n * a).factors = (n + 1) • a.factors
succ₁ : (a ^ n * a).factors = n • a.factors + a.factors
succ₂ : (a ^ n).factors + a.factors = n • a.factors + a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors
have succ₃ : n • a.factors + a.factors = n • a.factors + a.factors
Tactic: rw [pow_succ, succ_nsmul, factors_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Associates α
k : ℕ
⊢ (a ^ k).factors = k • a.factors
have zero : (HPow.hPow (β := ℕ) a 0).factors = HSMul.hSMul (α := ℕ) 0 a.factors
Tactic: induction k with
  | zero => rw [zero_nsmul, pow_zero]; exact factors_one
  | succ n h => rw [pow_succ, succ_nsmul, factors_mul, h]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Associates α
k : ℕ
zero : (HPow.hPow (β := ℕ) a 0).factors = HSMul.hSMul (α := ℕ) 0 a.factors
⊢ (a ^ k).factors = k • a.factors
have succ : ∀ (n : ℕ) (h : (a ^ n).factors = n • a.factors), (a ^ (n + 1)).factors = (n + 1) • a.factors
Tactic: induction k with
  | zero => rw [zero_nsmul, pow_zero]; exact factors_one
  | succ n h => rw [pow_succ, succ_nsmul, factors_mul, h]
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)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors
have rw : p ^ k ≤ m ↔
  k ≤
    (if hp : Irreducible p then bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) else 0) m.factors
Tactic: rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount 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)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
rw :
  p ^ k ≤ m ↔
    k ≤
      (if hp : Irreducible p then bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) else 0)
        m.factors
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors
have rw₁ : p ^ k ≤ m ↔ k ≤ bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p h₂) m.factors
Tactic: rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount 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)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
rw :
  p ^ k ≤ m ↔
    k ≤
      (if hp : Irreducible p then bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) else 0)
        m.factors
rw₁ : p ^ k ≤ m ↔ k ≤ bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p h₂) m.factors
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors
have rw₂ : k ≤ bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p h₂) m.factors ↔
  k ≤ bcount (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p h₂) m.factors
Tactic: rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount 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)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ p.count m.factors ≠ 0 → p ≤ m
have rw : 0 < p.count m.factors → p ≤ m
Tactic: rw [← pos_iff_ne_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)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ p ≤ m
have rw : HPow.hPow (β := ℕ) p 1 ≤ m
Tactic: rw [← pow_one p]
-- 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)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
h : 0 < p.count m.factors
⊢ HPow.hPow (β := ℕ) p 1 ≤ m
have apply : 1 ≤ p.count m.factors
Tactic: apply (prime_pow_dvd_iff_le h0 hp).2
-- 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 p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ p ∣ a
have rw : count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔ LE.le (α := Associates α) (Associates.mk p) (Associates.mk a)
Tactic: rw [← Associates.mk_le_mk_iff_dvd]
-- 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 p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0 ↔
    LE.le (α := Associates α) (Associates.mk p) (Associates.mk a)
have h : ∀ (h : LE.le (α := Associates α) (Associates.mk p) (Associates.mk a)),
  count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
Tactic: refine
    ⟨fun h =>
      Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0)
        (Associates.irreducible_mk.mpr hp) h,
      fun h => ?_⟩
-- 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 p : α
ha0 : a ≠ 0
hp : Irreducible p
h : LE.le (α := Associates α) (Associates.mk p) (Associates.mk a)
⊢ count (Associates.mk p) (factors (Associates.mk a)) ≠ 0
have h₁ : 1 ≤ count (Associates.mk p) (factors (Associates.mk a))
Tactic: rw [← pow_one (Associates.mk p),
    Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0)
      (Associates.irreducible_mk.mpr hp)] at h
Cleared hypotheses: 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 : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a * b).factors = p.count a.factors + p.count b.factors
have obtain : ∀ (a0 : α) (nza : a0 ≠ 0) (ha : Ne (α := Associates α) (Associates.mk a0) 0),
  p.count (Associates.mk a0 * b).factors = p.count (factors (Associates.mk a0)) + p.count b.factors
Tactic: obtain ⟨a0, nza, rfl⟩ := exists_non_zero_rep ha
Cleared hypotheses: a, ha
-- 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)
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
⊢ p.count (Associates.mk a0 * b).factors = p.count (factors (Associates.mk a0)) + p.count b.factors
have obtain : ∀ (b0 : α) (nzb : b0 ≠ 0) (hb : Ne (α := Associates α) (Associates.mk b0) 0),
  p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
Tactic: obtain ⟨b0, nzb, rfl⟩ := exists_non_zero_rep hb
Cleared hypotheses: b, hb
-- 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw : p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
  p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₁ : p.count
    (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
      (factors (Associates.mk b0))) =
  p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
    p.count (factors (Associates.mk b0))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₂ : p.count
    (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
      (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
  p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
    p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
rw₂ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₃ : p.count
    (↑(HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) :
      WithTop (Multiset { a : Associates α // Irreducible a })) =
  p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
    p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
rw₂ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  p.count
      (↑(HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) :
        WithTop (Multiset { a : Associates α // Irreducible a })) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₄ : Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
    (HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) =
  p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
    p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
rw₂ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  p.count
      (↑(HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) :
        WithTop (Multiset { a : Associates α // Irreducible a })) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₄ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
      (HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₅ : Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
  p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
    p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some 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)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Ne (α := Associates α) (Associates.mk a0) 0
b0 : α
nzb : b0 ≠ 0
hb : Ne (α := Associates α) (Associates.mk b0) 0
rw :
  p.count (HAdd.hAdd (α := FactorSet α) (factors (Associates.mk a0)) (factors (Associates.mk b0))) =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
rw₁ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (factors (Associates.mk b0))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (factors (Associates.mk b0))
rw₂ :
  p.count
      (HAdd.hAdd (α := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  p.count
      (↑(HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) :
        WithTop (Multiset { a : Associates α // Irreducible a })) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₄ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
      (HAdd.hAdd (α := Multiset { a : Associates α // Irreducible a }) (factors' a0) (factors' b0)) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₅ :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
      Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
    p.count (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) +
      p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ p.count (HMul.hMul (α := Associates α) (Associates.mk a0) (Associates.mk b0)).factors =
    p.count (factors (Associates.mk a0)) + p.count (factors (Associates.mk b0))
have rw₆ : Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' b0) =
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) (factors' a0) +
    p.count (↑(factors' b0) : WithTop (Multiset { a : Associates α // Irreducible a }))
Tactic: rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
    Multiset.count_add, count_some hp, count_some hp]