awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ f (a * b) = f a * f b
have neg : f
    (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
      p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ Multiset.count p (normalizedFactors a)) *
    f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ Multiset.count p (normalizedFactors b))
Tactic: suffices
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ ((normalizedFactors a).count p + (normalizedFactors b).count p)) =
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors a).count p) *
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors b).count p) by
    obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
    obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
    rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
    congr
    rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]
    · simp_rw [id, ← pow_add, this]
    all_goals simp only [Multiset.mem_toFinset]
    · intro p _ hpb
      simp [hpb]
    · intro p _ hpa
      simp [hpa]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
have neg : ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p
Tactic: refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p
⊢ f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
have neg₁ : ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
  ∀ q ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ∣ q → p = q
Tactic: refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p
have neg : ∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p
Tactic: simp only [Multiset.mem_toFinset, Finset.mem_union]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    ∀ q ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ∣ q → p = q
have neg : ∀ (p : α),
  p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
    ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
Tactic: simp only [Multiset.mem_toFinset, Finset.mem_union]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q
have neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
Tactic: rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ p = q
have neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
Tactic: rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = q
have neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
Tactic: rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
p : α
hp : p ∈ normalizedFactors b
q : α
hq : q ∈ normalizedFactors b
hdvd : p ∣ q
⊢ p = q
have neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
Tactic: rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ HPow.hPow (β := ℕ) x 0 * a₀ = a₀
have rw : 1 * a₀ = a₀
Tactic: rw [pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
rw : 1 * a₀ = a₀
⊢ HPow.hPow (β := ℕ) x 0 * a₀ = a₀
have rw₁ : a₀ = a₀
Tactic: rw [pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a
have obtain : ∀ (a : α) (n : ℕ) (h : x ^ n * a ≠ 0)
  (hm :
    ∀ (x_1 : α),
      Membership.mem (γ := Set α) {a_1 : α | ∃ (n_1 : ℕ), x ^ n_1 * a_1 = x ^ n * a} x_1 → ¬DvdNotUnit x_1 a),
  ∃ (n_1 : ℕ) (a_1 : α), ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1
Tactic: obtain ⟨a, ⟨n, rfl⟩, hm⟩ := wellFounded_dvdNotUnit.has_min
    {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩
Cleared hypotheses: a₀, h
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ (x_1 : α), Membership.mem (γ := Set α) {a_1 : α | ∃ (n_1 : ℕ), x ^ n_1 * a_1 = x ^ n * a} x_1 → ¬DvdNotUnit x_1 a
⊢ ∃ (n_1 : ℕ) (a_1 : α), ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1
have refine : ¬x ∣ a
Tactic: refine ⟨n, a, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α) {a : α | ∃ (n_1 : ℕ), x ^ n_1 * a = x ^ n * (x * d)} x_1 → ¬DvdNotUnit x_1 (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)
have rw : x ^ n * x * d = x ^ n * (x * d)
Tactic: rw [pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm :
  ∀ (x_1 : α),
    Membership.mem (γ := Set α) {a : α | ∃ (n_1 : ℕ), x ^ n_1 * a = x ^ n * (x * d)} x_1 → ¬DvdNotUnit x_1 (x * d)
rw : x ^ n * x * d = x ^ n * (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)
have rw₁ : x ^ n * (x * d) = x ^ n * (x * d)
Tactic: rw [pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : WfDvdMonoid α
a b : α
ha : ¬IsUnit a
hb : b ≠ 0
⊢ FiniteMultiplicity a b
have obtain : ∀ (n : ℕ) (c : α) (ndvd : ¬a ∣ c) (hb : a ^ n * c ≠ 0), FiniteMultiplicity a (a ^ n * c)
Tactic: obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ (n + 1) ∣ a ^ n * c
have rwa : ¬a ^ n * a ∣ a ^ n * c
Tactic: rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ (↑n : ℕ∞) ≤ emultiplicity a b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
have rw : a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
Tactic: rw [← pow_dvd_iff_le_emultiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a b : R
n : ℕ
ha : Irreducible a
hb : b ≠ 0
⊢ a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
have revert : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
Tactic: revert b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
n : ℕ
ha : Irreducible a
⊢ ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
have succ : ∀ (n : ℕ) (ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b)
  {b : R} (hb : b ≠ 0), a ^ (n + 1) ∣ b ↔ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b
Tactic: induction n with
  | zero => simp
  | succ n ih => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b
have succ : a ^ (n + 1) ∣ b → replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
b : R
hb : b ≠ 0
succ : a ^ (n + 1) ∣ b → replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b
have succ₁ : replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (hypothesis)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
c : R
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors (a ^ (n + 1) * c)
have hb₁ : ¬a = 0 ∧ ¬a ^ n * c = 0
Tactic: rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors (a ^ (n + 1) * c)
have succ : a ^ n ∣ a ^ n * c
Tactic: rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
      normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
b : R
hb : b ≠ 0
⊢ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
have succ : (∃ (u : Multiset R),
    normalizedFactors b =
      HAdd.hAdd (α := Multiset R) (replicate (n + 1) ((normalize : (a : R) → R) a) : Multiset R) u) →
  a ^ (n + 1) ∣ b
Tactic: rw [Multiset.le_iff_exists_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = HAdd.hAdd (α := Multiset R) (replicate (n + 1) ((normalize : (a : R) → R) a) : Multiset R) u
⊢ a ^ (n + 1) ∣ b
have succ : a ^ (n + 1) ∣ HPow.hPow (α := R) ((normalize : (a : R) → R) a : R) (n + 1) * u.prod
Tactic: rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b = (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
have a₁ : emultiplicity a b ≤ (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
a₁ : emultiplicity a b ≤ (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
⊢ emultiplicity a b = (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
have a₂ : (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞) ≤ emultiplicity a b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b ≤ (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
have a₁ : emultiplicity a b < HAdd.hAdd (α := ℕ∞) (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞) 1
Tactic: apply Order.le_of_lt_add_one
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b < HAdd.hAdd (α := ℕ∞) (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞) 1
have a₁ : ¬count ((normalize : (a : R) → R) a) (normalizedFactors b) + 1 ≤
    count ((normalize : (a : R) → R) a) (normalizedFactors b)
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge,
      le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞) ≤ emultiplicity a b
have a₁ : replicate (count ((normalize : (a : R) → R) a) (normalizedFactors b)) ((normalize : (a : R) → R) a) ≤
  normalizedFactors b
Tactic: rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
a₁ :
  replicate (count ((normalize : (a : R) → R) a) (normalizedFactors b)) ((normalize : (a : R) → R) a) ≤
    normalizedFactors b
⊢ (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞) ≤ emultiplicity a b
have a₂ : count ((normalize : (a : R) → R) a) (normalizedFactors b) ≤ count ((normalize : (a : R) → R) a) (normalizedFactors b)
Tactic: rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (hypothesis)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ multiplicity a b = count ((normalize : (a : R) → R) a) (normalizedFactors b)
have this : emultiplicity a b = (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
Tactic: have := emultiplicity_eq_count_normalizedFactors ha hb
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity (goal)
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
inst_3 : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
this : emultiplicity a b = (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)
⊢ multiplicity a b = count ((normalize : (a : R) → R) a) (normalizedFactors b)
have rwa : ∀ (this : Eq (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑(count ((normalize : (a : R) → R) a) (normalizedFactors b)) : ℕ∞)),
  multiplicity a b = count ((normalize : (a : R) → R) a) (normalizedFactors b)
Tactic: rwa [(finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity,
    ENat.coe_inj] at this
Cleared hypotheses: this