awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ Dvd.dvd (α := ℕ) 0 ((a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
exact absurd (zero_dvd_iff.mp hea) ha_pos

Premises used: zero_dvd_iff, absurd, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hd : e.factorization ≤ a.factorization ⊓ b.factorization
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun (x1 x2 : ℕ) ↦ x1 ^ x2

Tactic:
apply dvd_prod_pow_of_factorization_le he_pos

Premises used: Nat.dvd_prod_pow_of_factorization_le
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e.factorization ≤ a.factorization

Tactic:
have hea' := (factorization_le_iff_dvd he_pos ha_pos).mpr hea
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
⊢ e.factorization ≤ b.factorization

Tactic:
have heb' := (factorization_le_iff_dvd he_pos hb_pos).mpr heb
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
hea' : e.factorization ≤ a.factorization
heb' : e.factorization ≤ b.factorization
⊢ e.factorization ≤ a.factorization ⊓ b.factorization

Tactic:
simp [hea', heb']
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
rw : a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization
⊢ (a.lcm b).factorization = a.factorization ⊔ b.factorization

Tactic:
rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]

Premises used: Nat.gcd, Nat.gcd_mul_lcm, Nat.factorization_mul, mt, Nat.lcm_ne_zero, And.left, Iff.mp, Nat.factorization_gcd, Nat.gcd_eq_zero_iff, add_right_inj, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h :
  ∀ (a_1 : ℕ),
    Eq (α := ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
      ((a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
⊢ a.factorization + b.factorization = a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization

Tactic:
ext1
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a_1 : ℕ
⊢ Eq (α := ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
    ((a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)

Tactic:
(min_add_max _ _).symm

Premises used: min_add_max, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a_1 : ℕ
⊢ Eq (α := ℕ) ((a.factorization + b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)
    ((a.factorization ⊓ b.factorization + a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) a_1 : ℕ)

Tactic:
exact (min_add_max _ _).symm

Premises used: min_add_max, Eq.symm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
inl : (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f
inr :
  ∀ (hm₀ : m ≠ 0),
    (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hm₀ := eq_or_ne m 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
β : Type u_1
inst : CommMonoid β
n : ℕ
f : ℕ → β
⊢ (gcd 0 n).primeFactors.prod f * (0 * n).primeFactors.prod f = (primeFactors 0).prod f * n.primeFactors.prod f

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
inr : (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f
inr₁ :
  ∀ (hn₀ : n ≠ 0),
    (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
obtain rfl | hn₀ := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
β : Type u_1
inst : CommMonoid β
m : ℕ
f : ℕ → β
hm₀ : m ≠ 0
⊢ (m.gcd 0).primeFactors.prod f * (m * 0).primeFactors.prod f = m.primeFactors.prod f * (primeFactors 0).prod f

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
β : Type u_1
inst : CommMonoid β
m n : ℕ
f : ℕ → β
hm₀ : m ≠ 0
hn₀ : n ≠ 0
inr :
  (m.gcd n).primeFactors.prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₁ :
  (m.primeFactors ∩ n.primeFactors).prod f * (m.primeFactors ∪ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₂ :
  (m.primeFactors ∪ n.primeFactors).prod f * (m.primeFactors ∩ n.primeFactors).prod f =
    m.primeFactors.prod f * n.primeFactors.prod f
inr₃ inr₄ :
  HMul.hMul (α := β) (∏ x ∈ m.primeFactors, f x) (∏ x ∈ n.primeFactors, f x) =
    m.primeFactors.prod f * n.primeFactors.prod f
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]

Premises used: Nat.primeFactors_gcd, mul_comm, Nat.primeFactors_mul, Finset.prod_union_inter
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
h :
  ∀ (x : ℕ),
    Membership.mem (γ := Set ℕ) {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} x ↔
      Membership.mem (γ := Set ℕ) (Set.Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Set ℕ) x
⊢ Eq (α := Set ℕ) ({i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} : Set ℕ) (Set.Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Set ℕ)

Tactic:
ext
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} x ↔
    Membership.mem (γ := Set ℕ) (Set.Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Set ℕ) x

Tactic:
simp [one_le_iff_ne_zero, pp.pow_dvd_iff_le_factorization hn]

Premises used: Nat.one_le_iff_ne_zero, Nat.Prime.pow_dvd_iff_le_factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
inl : Eq (α := Finset ℕ) (Icc 1 ((factorization 0 : (a : ℕ) → ℕ) p) : Finset ℕ) ({i ∈ Ico 1 0 | p ^ i ∣ 0} : Finset ℕ)
inr : ∀ (hn : n ≠ 0), Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}
⊢ Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p : ℕ
pp : Prime p
⊢ Eq (α := Finset ℕ) (Icc 1 ((factorization 0 : (a : ℕ) → ℕ) p) : Finset ℕ) ({i ∈ Ico 1 0 | p ^ i ∣ 0} : Finset ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
inr :
  ∀ (x : ℕ),
    Membership.mem (γ := Finset ℕ) (Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Finset ℕ) x ↔
      x ∈ {i ∈ Ico 1 n | p ^ i ∣ n}
⊢ Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
ext x
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
inr : 1 ≤ x → x ≤ (n.factorization : (a : ℕ) → ℕ) p → x < n
⊢ Membership.mem (γ := Finset ℕ) (Icc 1 ((n.factorization : (a : ℕ) → ℕ) p) : Finset ℕ) x ↔
    x ∈ {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
simp only [mem_Icc, Finset.mem_filter, mem_Ico, and_assoc, and_congr_right_iff,
    pp.pow_dvd_iff_le_factorization hn, iff_and_self]

Premises used: Finset.mem_Icc, and_congr_right_iff, and_assoc, Finset.mem_filter, Nat.Prime.pow_dvd_iff_le_factorization, iff_and_self, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ 1 ≤ x → x ≤ (n.factorization : (a : ℕ) → ℕ) p → x < n

Tactic:
fun _ H => lt_of_le_of_lt H (factorization_lt p hn)

Premises used: lt_of_le_of_lt, Nat.factorization_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
hn : n ≠ 0
x : ℕ
⊢ 1 ≤ x → x ≤ (n.factorization : (a : ℕ) → ℕ) p → x < n

Tactic:
exact fun _ H => lt_of_le_of_lt H (factorization_lt p hn)

Premises used: lt_of_le_of_lt, Nat.factorization_lt
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p : ℕ
pp : Prime p
⊢ (n.factorization : (a : ℕ) → ℕ) p = #({i ∈ Ico 1 n | p ^ i ∣ n})

Tactic:
simp [← Icc_factorization_eq_pow_dvd n pp]

Premises used: Nat.Icc_factorization_eq_pow_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
h : ∀ (x : ℕ), x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
ext x
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h : p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)
⊢ x ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ x ∈ {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]

Premises used: Finset.mem_Icc, and_congr_right_iff, and_congr_left_iff, Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b

Tactic:
iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
    (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb

Premises used: Nat.Prime.one_lt, iff_of_true, Iff.mp, Nat.Prime.two_le, Nat.pow_le_pow_iff_right, LE.le.trans, Nat.le_of_dvd, Ne.bot_lt, Nat.lt_of_pow_dvd_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b

Tactic:
exact iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
    (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb

Premises used: Nat.Prime.one_lt, iff_of_true, Iff.mp, Nat.Prime.two_le, Nat.pow_le_pow_iff_right, LE.le.trans, Nat.le_of_dvd, Ne.bot_lt, Nat.lt_of_pow_dvd_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
h : ∀ (i : ℕ), i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Ico 1 b | p ^ i ∣ n}

Tactic:
ext i
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h : p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)
⊢ i ∈ {i ∈ Ico 1 n | p ^ i ∣ n} ↔ i ∈ {i ∈ Ico 1 b | p ^ i ∣ n}

Tactic:
simp only [Finset.mem_filter, mem_Ico, and_congr_left_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, and_congr_left_iff, Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
⊢ p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)

Tactic:
fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩

Premises used: Nat.Prime.one_lt, Iff.intro, Nat.lt_of_pow_dvd_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h : ∀ (h1 : p ^ i ∣ n) (h2 : 1 ≤ i) (h : i < n), i < b
⊢ p ^ i ∣ n → 1 ≤ i → (i < n ↔ i < b)

Tactic:
refine fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
i : ℕ
h1 : p ^ i ∣ n
h2 : 1 ≤ i
h : i < n
h₁ : ∀ (pp : Prime 0) (hb : n < HPow.hPow (α := ℕ) 0 b) (h1 : HPow.hPow (α := ℕ) 0 i ∣ n), i < b
h₂ : ∀ (p : ℕ) (pp : Prime (p + 1)) (hb : n < (p + 1) ^ b) (h1 : (p + 1) ^ i ∣ n), i < b
⊢ i < b

Tactic:
rcases p with - | p
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < HPow.hPow (α := ℕ) 0 b
h1 : HPow.hPow (α := ℕ) 0 i ∣ n
⊢ i ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < HPow.hPow (α := ℕ) 0 b
h1 : HPow.hPow (α := ℕ) 0 i ∣ n
⊢ n = 0

Tactic:
rw [zero_pow (by lia), zero_dvd_iff] at h1

Premises used: zero_dvd_iff, zero_pow
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < HPow.hPow (α := ℕ) 0 b
h1 : n = 0
⊢ i < b

Tactic:
(hn h1).elim

Premises used: False.elim
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < HPow.hPow (α := ℕ) 0 b
h1 : n = 0
⊢ i < b

Tactic:
exact (hn h1).elim

Premises used: False.elim
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
h₁ : (p + 1) ^ i < (p + 1) ^ b
⊢ i < b

Tactic:
rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]

Premises used: Nat.Prime.one_lt, Nat.pow_lt_pow_iff_right
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
p : ℕ
pp : Prime (p + 1)
hb : n < (p + 1) ^ b
h1 : (p + 1) ^ i ∣ n
⊢ (p + 1) ^ i < (p + 1) ^ b

Tactic:
apply lt_of_le_of_lt (le_of_dvd (Nat.zero_lt_of_ne_zero hn) h1) hb

Premises used: lt_of_le_of_lt, Nat.zero_lt_of_ne_zero, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n ≠ 0

Tactic:
lia
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
rwa : #({i ∈ Ico 1 n | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
rwa₁ : #({i ∈ Ico 1 b | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
rwa₂ : n < m ^ b
rwa₃ : ℕ
rwa₄ : #({i ∈ Ico 1 b | m ^ i ∣ n}) = #({i ∈ Ico 1 b | m ^ i ∣ n})
rwa₅ : n < m ^ b
rwa₆ : ℕ
rwa₇ rwa₈ : n < m ^ b
⊢ (n.factorization : (a : ℕ) → ℕ) m = #({i ∈ Ico 1 b | m ^ i ∣ n})

Tactic:
rwa [factorization_eq_card_pow_dvd n hm, Ico_pow_dvd_eq_Ico_of_lt hm (by lia)]

Premises used: Nat.Ico_pow_dvd_eq_Ico_of_lt, Nat.factorization_eq_card_pow_dvd
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) =
    (a.factorization : (a : ℕ) → ℕ) p
rw₁ :
  HAdd.hAdd (β := ℕ) (count p a.primeFactorsList) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) = count p a.primeFactorsList
rw₂ : count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList
rw₃ : count p a.primeFactorsList + 0 = count p a.primeFactorsList
rw₄ rw₅ : count p a.primeFactorsList = count p a.primeFactorsList
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq,
    ← primeFactorsList_count_eq,
    count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]

Premises used: Nat.factorization_mul_apply_of_coprime, Nat.primeFactorsList_count_eq, List.count_eq_zero_of_not_mem, add_zero, Nat.coprime_primeFactorsList_disjoint
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
rw : Eq (α := ℕ) (((b * a).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) (((a * b).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ Eq (α := ℕ) (((b * a).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

Premises used: Nat.coprime_comm, Iff.mp, Nat.factorization_eq_of_coprime_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
p a b : ℕ
hab : a.Coprime b
hpb : p ∈ b.primeFactorsList
⊢ Eq (α := ℕ) (((b * a).factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

Premises used: Nat.coprime_comm, Iff.mp, Nat.factorization_eq_of_coprime_left
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
mp : a = b → ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
mpr : (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a : ℕ
ha hb : a ≠ 0
⊢ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p a

Tactic:
simp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
⊢ a = b

Tactic:
eq_of_factorization_eq ha hb fun p => ?_

Premises used: Nat.eq_of_factorization_eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
mpr : ∀ (p : ℕ), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ a = b

Tactic:
refine eq_of_factorization_eq ha hb fun p => ?_

Premises used: Nat.eq_of_factorization_eq
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pos : ∀ (pp : Prime p), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
neg : ∀ (pp : ¬Prime p), Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
by_cases pp : p.Prime

Premises used: Nat.Prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : Prime p
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [factorization_def, pp, h p pp]

Premises used: Nat.factorization_def
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b
p : ℕ
pp : ¬Prime p
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp [factorization_eq_zero_of_not_prime, pp]

Premises used: Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
nth_rw :
  Eq (α := ℕ) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n

Tactic:
nth_rw 2 [← prod_factorization_pow_eq_self hn]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
rw :
  Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)
⊢ Eq (α := ℕ) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
h : n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}
hg : ∀ x ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support, x ^ padicValNat x n = 1
hfg :
  ∀ x ∈ n.factorization.support, (fun (x1 x2 : ℕ) ↦ x1 ^ x2) x ((n.factorization : (a : ℕ) → ℕ) x) = x ^ padicValNat x n
⊢ Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n)

Tactic:
apply Finset.prod_subset_one_on_sdiff

Premises used: Finset.prod_subset_one_on_sdiff
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}

Tactic:
fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩

Premises used: Iff.mpr, Finset.mem_range, LT.lt.trans_le', Nat.prime_of_mem_primeFactors, And.intro, Finset.mem_filter, Nat.le_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ n.factorization.support ⊆ {p ∈ Finset.range m | Prime p}

Tactic:
exact fun p hp => Finset.mem_filter.mpr ⟨Finset.mem_range.2 <| pr.trans_le' <|
      le_of_mem_primeFactors hp, prime_of_mem_primeFactors hp⟩

Premises used: Iff.mpr, Finset.mem_range, LT.lt.trans_le', Nat.prime_of_mem_primeFactors, And.intro, Finset.mem_filter, Nat.le_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
⊢ p ∈ {p ∈ Finset.range m | Prime p}

Tactic:
obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp

Premises used: Finset.mem_sdiff, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
⊢ p ∉ n.factorization.support

Tactic:
obtain ⟨hp1, hp2⟩ := Finset.mem_sdiff.mp hp

Premises used: Finset.mem_sdiff, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
hg : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ p ^ padicValNat p n = 1

Tactic:
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]

Premises used: And.right, Iff.mp, Finset.mem_filter, Nat.factorization_def
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ {p ∈ Finset.range m | Prime p} \ n.factorization.support
hp1 : p ∈ {p ∈ Finset.range m | Prime p}
hp2 : p ∉ n.factorization.support
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
simp [Finsupp.notMem_support_iff.mp hp2]

Premises used: Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
p : ℕ
hp : p ∈ n.factorization.support
⊢ (fun (x1 x2 : ℕ) ↦ x1 ^ x2) p ((n.factorization : (a : ℕ) → ℕ) p) = p ^ padicValNat p n

Tactic:
simp [factorization_def n (prime_of_mem_primeFactors hp)]

Premises used: Nat.prime_of_mem_primeFactors, Nat.factorization_def
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
nth_rw :
  Eq (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
⊢ n = ∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ)

Tactic:
nth_rw 1 [← prod_factorization_pow_eq_self hn]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (∏ p ∈ n.primeFactors, HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))

Tactic:
prod_subtype n.primeFactors (fun _ ↦ Iff.rfl) fun a ↦ a ^ n.factorization a

Premises used: Iff.rfl, HPow.hPow, Nat.primeFactors, Finset.prod_subtype, DFunLike.coe, Nat.factorization
-- Module: Mathlib.Data.Nat.Factorization.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (∏ p ∈ n.primeFactors, HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p : ↥n.primeFactors, HPow.hPow (β := ℕ) (↑p : ℕ) ((n.factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))

Tactic:
exact prod_subtype n.primeFactors (fun _ ↦ Iff.rfl) fun a ↦ a ^ n.factorization a

Premises used: Iff.rfl, HPow.hPow, Nat.primeFactors, Finset.prod_subtype, DFunLike.coe, Nat.factorization