awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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 : α
hpa neg : p ∈ normalizedFactors a
neg₁ : α
⊢ Prime p

Tactic:
apply prime_of_normalized_factor

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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 : α
hpb neg : p ∈ normalizedFactors b
neg₁ : α
⊢ Prime p

Tactic:
apply prime_of_normalized_factor

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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 : α
hpa : p ∈ normalizedFactors a
⊢ p ∈ normalizedFactors a

Tactic:
assumption
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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 : α
hpb : p ∈ normalizedFactors b
⊢ p ∈ normalizedFactors b

Tactic:
assumption
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
neg : Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)
⊢ p = q

Tactic:
rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
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
⊢ Eq (α := α) ((normalize : (a : α) → α) p : α) ((normalize : (a : α) → α) q : α)

Tactic:
exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Premises used: Prime.irreducible, normalize_eq_normalize, Irreducible.dvd_symm, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
rw : 1 * a₀ = a₀
rw₁ rw₂ : a₀ = a₀
⊢ HPow.hPow (β := ℕ) x 0 * a₀ = a₀

Tactic:
rw [pow_zero, one_mul]

Premises used: pow_zero, one_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
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
⊢ ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

Tactic:
obtain ⟨a, ⟨n, rfl⟩, hm⟩ := wellFounded_dvdNotUnit.has_min
    {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩

Premises used: HMul.hMul, setOf, wellFounded_dvdNotUnit, Exists, HPow.hPow, Exists.intro, WellFounded.has_min, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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

Tactic:
⟨n, a, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
refine : ¬x ∣ a
⊢ ∃ (n_1 : ℕ) (a_1 : α), ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1

Tactic:
refine ⟨n, a, ?_, rfl⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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)
rw₁ rw₂ : x ^ n * (x * d) = x ^ n * (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)

Tactic:
rw [pow_succ, mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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)
⊢ False

Tactic:
exact hm d ⟨n + 1, by rw [pow_succ, mul_assoc]⟩
    ⟨(right_ne_zero_of_mul <| right_ne_zero_of_mul h), x, hx, mul_comm _ _⟩

Premises used: right_ne_zero_of_mul, HAdd.hAdd, And.intro, Exists.intro, mul_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : Irreducible x
⊢ ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

Tactic:
max_power_factor' h hx.not_isUnit

Premises used: Irreducible.not_isUnit, WfDvdMonoid.max_power_factor'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : WfDvdMonoid α
a b : α
ha : ¬IsUnit a
hb : b ≠ 0
obtain : ∀ (n : ℕ) (c : α) (ndvd : ¬a ∣ c) (hb : a ^ n * c ≠ 0), FiniteMultiplicity a (a ^ n * c)
⊢ FiniteMultiplicity a b

Tactic:
obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha

Premises used: WfDvdMonoid.max_power_factor', rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
rwa : ¬a ^ n * a ∣ a ^ n * c
rwa₁ rwa₂ rwa₃ rwa₄ : ¬a ∣ c
⊢ ¬a ^ (n + 1) ∣ a ^ n * c

Tactic:
rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]

Premises used: pow_succ, mul_dvd_mul_iff_left, left_ne_zero_of_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
⊢ FiniteMultiplicity a (a ^ n * c)

Tactic:
exact ⟨n, by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : WfDvdMonoid α
a b : α
ha : Prime a
hb : b ≠ 0
⊢ FiniteMultiplicity a b

Tactic:
.of_not_isUnit ha.not_unit hb

Premises used: Prime.not_unit, FiniteMultiplicity.of_not_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
rw : a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
⊢ (↑n : ℕ∞) ≤ emultiplicity a b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b

Tactic:
rw [← pow_dvd_iff_le_emultiplicity]

Premises used: pow_dvd_iff_le_emultiplicity
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
revert : ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b
⊢ a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b

Tactic:
revert b
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
ha : Irreducible a
⊢ ∀ {b : R} (hb : b ≠ 0), HPow.hPow (β := ℕ) a 0 ∣ b ↔ replicate 0 ((normalize : (a : R) → R) a) ≤ normalizedFactors b

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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

Tactic:
?_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
a : R
n : ℕ
ha : Irreducible a
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
⊢ ∀ {b : R} (hb : b ≠ 0), a ^ n ∣ b ↔ replicate n ((normalize : (a : R) → R) a) ≤ normalizedFactors b

Tactic:
induction n with
  | zero => simp
  | succ n ih => ?_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
succ₁ : replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
⊢ a ^ (n + 1) ∣ b ↔ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors b

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
⊢ ¬a = 0 ∧ ¬a ^ n * c = 0

Tactic:
rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb

Premises used: mul_assoc, Ne, mul_eq_zero, not_or, pow_succ'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
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
succ : a ^ n ∣ a ^ n * c
⊢ replicate (n + 1) ((normalize : (a : R) → R) a) ≤ normalizedFactors (a ^ (n + 1) * 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]

Premises used: Multiset.singleton_add, mul_assoc, Multiset.replicate_succ, UniqueFactorizationMonoid.normalizedFactors_mul, And.right, And.left, UniqueFactorizationMonoid.normalizedFactors_irreducible, Multiset.cons_le_cons_iff, pow_succ'