awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
apply : c ≠ 0
⊢ k ∣ p.count (c ^ k).factors

Tactic:
apply dvd_count_pow _ hp

Premises used: Associates.dvd_count_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h_1 : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = HPow.hPow (α := Associates α) 0 k
⊢ a * b = 0

Tactic:
rw [zero_pow hk0] at h

Premises used: zero_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h_1 : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
inl : a = 0 → False
inr : b = 0 → False
⊢ False

Tactic:
cases mul_eq_zero.mp h

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h_1 : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h_2 : a = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h_1 : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
h : a * b = 0
h_2 : b = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
nontriviality : Subsingleton α → ∃ (d : Associates α), a = d ^ k
nontriviality₁ : Nontrivial α → ∃ (d : Associates α), a = d ^ k
pos : Nontrivial α → ∀ (hk0 : k = 0), ∃ (d : Associates α), a = d ^ k
neg neg₁ : Nontrivial α → ∀ (hk0 : ¬k = 0), ∃ (d : Associates α), a = d ^ k
⊢ ∃ (d : Associates α), a = d ^ k

Tactic:
classical
  nontriviality α
  by_cases hk0 : k = 0
  · use 1
    rw [hk0, pow_zero] at h ⊢
    apply (mul_eq_one.1 h).1
  · refine is_pow_of_dvd_count ha fun p hp ↦ ?_
    apply dvd_count_of_dvd_count_mul hb hp hab
    rw [h]
    apply dvd_count_pow _ hp
    rintro rfl
    rw [zero_pow hk0] at h
    cases mul_eq_zero.mp h <;> contradiction

Premises used: mul_eq_zero, pow_zero, mul_eq_one, And.left, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst_2 : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h rw : a ∣ p ^ n
rw₁ : ℕ
⊢ a = p ^ Nat.find (p := fun (n : ℕ) ↦ a ∣ p ^ n) ⋯

Tactic:
rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]

Premises used: Associates.eq_pow_count_factors_of_dvd_pow, Associates.count_factors_eq_find_of_dvd_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst_2 : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h classical : a ∣ p ^ n
classical₁ : ℕ
⊢ a = p ^ Nat.find (p := fun (n : ℕ) ↦ a ∣ p ^ n) ⋯

Tactic:
classical rw [count_factors_eq_find_of_dvd_pow hp, ← eq_pow_count_factors_of_dvd_pow hp h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst_2 : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a ∣ p ^ n

Tactic:
h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
⊢ Nontrivial M

Tactic:
haveI : Nontrivial M := ⟨⟨y, 0, hy⟩⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this : Nontrivial M
haveI : (this : NormalizationMonoid M) → Fintype { x : M // x ∣ y }
⊢ Fintype { x : M // x ∣ y }

Tactic:
haveI : NormalizationMonoid M := UniqueFactorizationMonoid.normalizationMonoid
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this : NormalizationMonoid M
haveI : (this : DecidableEq M) → Fintype { x : M // x ∣ y }
⊢ Fintype { x : M // x ∣ y }

Tactic:
haveI := Classical.decEq M
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this : DecidableEq M
haveI : (this : DecidableEq (Associates M)) → Fintype { x : M // x ∣ y }
⊢ Fintype { x : M // x ∣ y }

Tactic:
haveI := Classical.decEq (Associates M)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
Finset :
  ∀ (x : M),
    Membership.mem (γ := _root_.Finset M)
        (_root_.Finset.image (fun (s : Multiset M × Mˣ) ↦ (↑s.2 : M) * s.1.prod)
          (SProd.sprod (β := _root_.Finset Mˣ) (normalizedFactors y).powerset.toFinset _root_.Finset.univ))
        x ↔
      x ∣ y
⊢ Fintype { x : M // x ∣ y }

Tactic:
refine
    Fintype.subtype
      (((normalizedFactors y).powerset.toFinset ×ˢ (Finset.univ : Finset Mˣ)).image fun s =>
        (s.snd : M) * s.fst.prod)
      fun x => ?_

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.toFinset, HMul.hMul, Finset.univ, SProd.sprod, Multiset.powerset, Fintype.subtype, Finset.image
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
simp : (∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x) ↔ x ∣ y
⊢ Membership.mem (γ := Finset M)
      (Finset.image (fun (s : Multiset M × Mˣ) ↦ (↑s.2 : M) * s.1.prod)
        (SProd.sprod (β := Finset Mˣ) (normalizedFactors y).powerset.toFinset Finset.univ))
      x ↔
    x ∣ y

Tactic:
simp only [Finset.mem_image, Finset.mem_product, Finset.mem_univ, and_true,
    Multiset.mem_toFinset, Multiset.mem_powerset]

Premises used: Finset.mem_univ, Multiset.mem_powerset, and_true, Finset.mem_image, Finset.mem_product, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
mp : (∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x) → x ∣ y
mpr : x ∣ y → ∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x
⊢ (∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x) ↔ x ∣ y

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
mp : s.1.prod ∣ (normalizedFactors y).prod
⊢ (↑s.2 : M) * s.1.prod ∣ y

Tactic:
rw [(unit_associated_one.mul_right s.fst.prod).dvd_iff_dvd_left, one_mul,
      ← (prod_normalizedFactors hy).dvd_iff_dvd_right]

Premises used: Multiset.prod, Prod.fst, unit_associated_one, UniqueFactorizationMonoid.prod_normalizedFactors, Associated.dvd_iff_dvd_left, Associated.mul_right, Associated.dvd_iff_dvd_right, one_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ (normalizedFactors y).prod

Tactic:
Multiset.prod_dvd_prod_of_le hs

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
s : Multiset M × Mˣ
hs : s.1 ≤ normalizedFactors y
⊢ s.1.prod ∣ (normalizedFactors y).prod

Tactic:
exact Multiset.prod_dvd_prod_of_le hs

Premises used: Multiset.prod_dvd_prod_of_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
⊢ x ≠ 0

Tactic:
mt (fun hx => ?_) hy

Premises used: mt
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
refine : ∀ (hx : x = 0), y = 0
⊢ x ≠ 0

Tactic:
refine mt (fun hx => ?_) hy

Premises used: mt
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x = 0
rwa : ∀ (h : 0 ∣ y) (hx : x = 0), y = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : y = 0) (hx : x = 0), y = 0
⊢ y = 0

Tactic:
rwa [hx, zero_dvd_iff] at h

Premises used: zero_dvd_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by
      refine mt (fun hx => ?_) hy
      rwa [hx, zero_dvd_iff] at h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x ≠ 0
mpr :
  ∀ (u : Mˣ) (hu : (normalizedFactors x).prod * (↑u : M) = x),
    ∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x
⊢ ∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x

Tactic:
obtain ⟨u, hu⟩ := prod_normalizedFactors hx

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x ≠ 0
u : Mˣ
hu : (normalizedFactors x).prod * (↑u : M) = x
⊢ ∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x

Tactic:
⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩

Premises used: UniqueFactorizationMonoid.normalizedFactors, Prod.mk, And.intro, Exists.intro, mul_comm, Eq.trans
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x ≠ 0
u : Mˣ
hu : (normalizedFactors x).prod * (↑u : M) = x
mpr : (normalizedFactors x, u).1 ≤ normalizedFactors y
⊢ ∃ (a : Multiset M × Mˣ), a.1 ≤ normalizedFactors y ∧ (↑a.2 : M) * a.1.prod = x

Tactic:
refine ⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x ≠ 0
u : Mˣ
hu : (normalizedFactors x).prod * (↑u : M) = x
⊢ (normalizedFactors x, u).1 ≤ normalizedFactors y

Tactic:
(dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.map, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : UniqueFactorizationMonoid M
inst_2 : Fintype Mˣ
y : M
hy : y ≠ 0
this_1 : Nontrivial M
this_2 : NormalizationMonoid M
this_3 : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : x ∣ y
hx : x ≠ 0
u : Mˣ
hu : (normalizedFactors x).prod * (↑u : M) = x
⊢ (normalizedFactors x, u).1 ≤ normalizedFactors y

Tactic:
exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

Premises used: Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
n p : α
⊢ (factorization n : (a : α) → ℕ) p = Multiset.count p (normalizedFactors n)

Tactic:
simp [factorization]

Premises used: factorization
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := α →₀ ℕ) (factorization 0) 0

Tactic:
simp [factorization]

Premises used: factorization
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := α →₀ ℕ) (factorization 1) 0

Tactic:
simp [factorization]

Premises used: factorization
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
n : α
⊢ (factorization n).support = (normalizedFactors n).toFinset

Tactic:
simp [factorization, Multiset.toFinsupp_support]

Premises used: factorization, Multiset.toFinsupp_support
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (a * b) = factorization a + factorization b

Tactic:
simp [factorization, normalizedFactors_mul ha hb]

Premises used: UniqueFactorizationMonoid.normalizedFactors_mul, factorization
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
x : α
n : ℕ
h : ∀ (a : α), Eq (α := ℕ) ((factorization (x ^ n) : (a : α) → ℕ) a : ℕ) ((n • factorization x : (a : α) → ℕ) a : ℕ)
⊢ factorization (x ^ n) = n • factorization x

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
x : α
n : ℕ
a : α
⊢ Eq (α := ℕ) ((factorization (x ^ n) : (a : α) → ℕ) a : ℕ) ((n • factorization x : (a : α) → ℕ) a : ℕ)

Tactic:
simp [factorization]

Premises used: factorization
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : factorization a = factorization b
⊢ normalizedFactors a = normalizedFactors b

Tactic:
simp_rw [factorization, AddEquiv.apply_eq_iff_eq] at h

Premises used: factorization, AddEquiv.apply_eq_iff_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h rwa rwa₁ rwa₂ rwa₃ : normalizedFactors a = normalizedFactors b
⊢ a ~ᵤ b

Tactic:
rwa [associated_iff_normalizedFactors_eq_normalizedFactors ha hb]

Premises used: UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw : LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) ∣ a

Tactic:
rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le]

Premises used: Associates.dvd_eq_le, congr_fun₂, Associates.mk_dvd_mk, Associates.quot_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
⊢ LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a)

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
⊢ LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a)

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw : LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk b)
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) ∣ b

Tactic:
rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le]

Premises used: Associates.dvd_eq_le, congr_fun₂, Associates.mk_dvd_mk, Associates.quot_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
⊢ LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk b)

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
⊢ LE.le (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk b)

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
rw : a ∣ c ∧ a ∣ b
⊢ a ∣ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk c ⊓ Associates.mk b)

Tactic:
rw [← mk_dvd_mk, Associates.quot_out, congr_fun₂ dvd_eq_le, le_inf_iff,
      mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]

Premises used: Associates.mk_le_mk_iff_dvd, Associates.dvd_eq_le, congr_fun₂, le_inf_iff, Associates.mk_dvd_mk, Associates.quot_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b

Tactic:
⟨hac, hab⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b

Tactic:
exact ⟨hac, hab⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
rw :
  Eq (α := Associates α)
    (Associates.mk
      (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
        Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b)))
    (Associates.mk (a * b))
rw₁ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) =
    Associates.mk (a * b)
rw₂ :
  HMul.hMul (α := Associates α)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b)))
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₃ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b)
      (Associates.mk (Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b))) ~ᵤ
    Associates.mk (a * b)
rw₄ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊓ Associates.mk b) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
rw₅ :
  HMul.hMul (α := Associates α) (Associates.mk a ⊔ Associates.mk b) (Associates.mk a ⊓ Associates.mk b) ~ᵤ
    Associates.mk (a * b)
rw₆ : HMul.hMul (α := Associates α) (Associates.mk a) (Associates.mk b) ~ᵤ Associates.mk (a * b)
rw₇ rw₈ : Associated (M := Associates α) (Associates.mk (a * b)) (Associates.mk (a * b))
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊓ Associates.mk b) *
      Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk b) ~ᵤ
    a * b

Tactic:
rw [← mk_eq_mk_iff_associated, ← Associates.mk_mul_mk, ← associated_iff_eq, Associates.quot_out,
      Associates.quot_out, mul_comm, sup_mul_inf, Associates.mk_mul_mk]

Premises used: Associates.mk_eq_mk_iff_associated, associated_iff_eq, Associates.mk_mul_mk, Associates.sup_mul_inf, mul_comm, Associates.quot_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk 0 ⊔ Associates.mk a) = 0

Tactic:
simp