awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ (HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)).Coprime
    (HPow.hPow (β := ℕ) q (((a.lcm b).factorization : (a : ℕ) → ℕ) q : ℕ))
have neg : p ≠ q
Tactic: refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
h' : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
⊢ p ≠ q
have neg : ∀ (h' : p = q), LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) ((a.factorization : (a : ℕ) → ℕ) q : ℕ)
Tactic: contrapose h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
have rw : Eq (α := ℕ)
  ((a.lcm b).factorization.prod fun (a_1 b_1 : ℕ) ↦
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
        a_1 ^ b_1
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
      else a_1 ^ b_1)
  ((a.lcm b).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
Tactic: rw [← prod_factorization_pow_eq_self (lcm_ne_zero ha hb), factorizationLCMLeft,
    factorizationLCMRight, ← prod_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Eq (α := ℕ)
    ((a.lcm b).factorization.prod fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    ((a.lcm b).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
have e_g : Eq (α := ℕ → ℕ → ℕ)
  (fun (a_1 b_1 : ℕ) ↦
    (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
        a_1 ^ b_1
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
      else a_1 ^ b_1)
  fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ Eq (α := ℕ → ℕ → ℕ)
    (fun (a_1 b_1 : ℕ) ↦
      (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then
          a_1 ^ b_1
        else 1) *
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) a_1 : ℕ) ((a.factorization : (a : ℕ) → ℕ) a_1 : ℕ) then 1
        else a_1 ^ b_1)
    fun (x1 x2 : ℕ) ↦ x1 ^ x2
have e_g : ∀ (p n : ℕ),
  ((if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n) =
    p ^ n
Tactic: ext p n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
⊢ ((if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n) =
    p ^ n
have pos : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) → p ^ n * 1 = p ^ n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p n : ℕ
pos : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) → p ^ n * 1 = p ^ n
⊢ ((if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
      else 1) *
      if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
      else p ^ n) =
    p ^ n
have neg : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) → 1 * p ^ n = p ^ n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ a.factorizationLCMLeft b ∣ a
have inl : factorizationLCMLeft 0 b ∣ 0
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
inl : factorizationLCMLeft 0 b ∣ 0
⊢ a.factorizationLCMLeft b ∣ a
have inr : ∀ (ha : a ≠ 0), a.factorizationLCMLeft b ∣ a
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMLeft b ∣ a
have inr : a.factorizationLCMLeft 0 ∣ a
Tactic: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
inr : a.factorizationLCMLeft 0 ∣ a
⊢ a.factorizationLCMLeft b ∣ a
have inr₁ : ∀ (hb : b ≠ 0), a.factorizationLCMLeft b ∣ a
Tactic: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a
have inr : a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: nth_rewrite 2 [← prod_factorization_pow_eq_self ha]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr : a.factorizationLCMLeft b ∣
  ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMLeft b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr₁ : a.factorization.support ⊆ (a.lcm b).factorization.support
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMLeft b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)
inr₁ : a.factorization.support ⊆ (a.lcm b).factorization.support
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr₂ : ∀ i ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) i 0 = 1
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((a.factorization : (a : ℕ) → ℕ) x : ℕ)
have inr : ∀ i ∈ (a.lcm b).factorization.support,
  (fun (p n : ℕ) ↦
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then p ^ n
        else 1)
      i (((a.lcm b).factorization : (a : ℕ) → ℕ) i) ∣
    HPow.hPow (β := ℕ) i ((a.factorization : (a : ℕ) → ℕ) i : ℕ)
Tactic: apply prod_dvd_prod_of_dvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
  HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: split_ifs with le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
pos :
  ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
      HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then
      HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)
    else 1) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : ∀ (le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
  1 ∣ HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: split_ifs with le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
  HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorization_lcm ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: apply pow_dvd_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
⊢ p ∈ (a.lcm b).factorization.support
have inr : ∀ (hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [mem_support_iff] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [factorization_lcm ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i : ℕ
h : i ∈ (a.lcm b).factorization.support
⊢ HPow.hPow (β := ℕ) i 0 = 1
have inr : Eq (α := ℕ) 1 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
⊢ a.factorizationLCMRight b ∣ b
have inl : factorizationLCMRight 0 b ∣ b
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
inl : factorizationLCMRight 0 b ∣ b
⊢ a.factorizationLCMRight b ∣ b
have inr : ∀ (ha : a ≠ 0), a.factorizationLCMRight b ∣ b
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight b ∣ b
have inr : a.factorizationLCMRight 0 ∣ 0
Tactic: rcases eq_or_ne b 0 with rfl | hb
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
inr : a.factorizationLCMRight 0 ∣ 0
⊢ a.factorizationLCMRight b ∣ b
have inr₁ : ∀ (hb : b ≠ 0), a.factorizationLCMRight b ∣ b
Tactic: rcases eq_or_ne b 0 with rfl | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b
have inr : a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: nth_rewrite 2 [← prod_factorization_pow_eq_self hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr : a.factorizationLCMRight b ∣
  ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMRight b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr₁ : b.factorization.support ⊆ (a.lcm b).factorization.support
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
inr :
  a.factorizationLCMRight b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)
inr₁ : b.factorization.support ⊆ (a.lcm b).factorization.support
⊢ a.factorizationLCMRight b ∣ b.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
have inr₂ : ∀ i ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) i 0 = 1
Tactic: rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMRight b ∣
    ∏ x ∈ (a.lcm b).factorization.support, HPow.hPow (β := ℕ) x ((b.factorization : (a : ℕ) → ℕ) x : ℕ)
have inr : ∀ i ∈ (a.lcm b).factorization.support,
  (fun (p n : ℕ) ↦
        if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
        else p ^ n)
      i (((a.lcm b).factorization : (a : ℕ) → ℕ) i) ∣
    HPow.hPow (β := ℕ) i ((b.factorization : (a : ℕ) → ℕ) i : ℕ)
Tactic: apply Finset.prod_dvd_prod_of_dvd
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have pos : ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
  1 ∣ HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: split_ifs with le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
pos :
  ∀ (le : LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
    1 ∣ HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ (if LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) then 1
    else HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ)) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : ∀ (le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)),
  HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: split_ifs with le
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
  HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [factorization_lcm ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬LE.le (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ HPow.hPow (β := ℕ) p ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ∣
    HPow.hPow (β := ℕ) p ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
have neg : LE.le (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: apply pow_dvd_pow
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ b.factorization.support
⊢ p ∈ (a.lcm b).factorization.support
have inr : ∀ (hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [mem_support_iff] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.LCM (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : Ne (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ Ne (α := ℕ) (((a.lcm b).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have inr : Ne (α := ℕ) ((a.factorization ⊔ b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: rw [factorization_lcm ha hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : IsPrimePow n
⊢ HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
have obtain : ∀ (p k : ℕ) (hp : Prime p) (hk : 0 < k),
  HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
Tactic: obtain ⟨p, k, hp, hk, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
have hp₁ : Nat.Prime p
Tactic: rw [← Nat.prime_iff] at hp
Cleared hypotheses: hp, hk
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
have rw : HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = p ^ k
Tactic: rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw : HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = p ^ k
⊢ HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
have rw₁ : HPow.hPow (β := ℕ) p ((Finsupp.single p k : (a : ℕ) → ℕ) p : ℕ) = p ^ k
Tactic: rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
rw : HPow.hPow (β := ℕ) p (((p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) = p ^ k
rw₁ : HPow.hPow (β := ℕ) p ((Finsupp.single p k : (a : ℕ) → ℕ) p : ℕ) = p ^ k
⊢ HPow.hPow (β := ℕ) (p ^ k).minFac (((p ^ k).factorization : (a : ℕ) → ℕ) (p ^ k).minFac : ℕ) = p ^ k
have rw₂ : p ^ k = p ^ k
Tactic: rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
⊢ IsPrimePow n
have inl : ∀ (h : HPow.hPow (β := ℕ) (Nat.minFac 0) ((Nat.factorization 0 : (a : ℕ) → ℕ) (Nat.minFac 0) : ℕ) = 0)
  (hn : Ne (α := ℕ) 0 1), IsPrimePow (R := ℕ) 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn')
Cleared hypotheses: n, h, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
inl :
  ∀ (h : HPow.hPow (β := ℕ) (Nat.minFac 0) ((Nat.factorization 0 : (a : ℕ) → ℕ) (Nat.minFac 0) : ℕ) = 0)
    (hn : Ne (α := ℕ) 0 1), IsPrimePow (R := ℕ) 0
⊢ IsPrimePow n
have inr : ∀ (hn' : n ≠ 0), IsPrimePow n
Tactic: rcases eq_or_ne n 0 with (rfl | hn')
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : HPow.hPow (β := ℕ) n.minFac ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ) = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n
have inr : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) n.minFac : ℕ)
Tactic: refine ⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k
have rw : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k
Tactic: rw [isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
⊢ (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k
have refine : ∀ (p k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k
Tactic: refine exists₂_congr fun p k => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k
have mp : Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p k : ℕ
mp : Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n ↔ 0 < k ∧ n.factorization = Finsupp.single p k
have mpr : 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ n.factorization = Finsupp.single p k
have rw : (p ^ k).factorization = Finsupp.single p k
Tactic: rw [← hn, Nat.Prime.factorization_pow hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
rw : (p ^ k).factorization = Finsupp.single p k
⊢ n.factorization = Finsupp.single p k
have rw₁ : Eq (α := ℕ →₀ ℕ) (Finsupp.single p k) (Finsupp.single p k)
Tactic: rw [← hn, Nat.Prime.factorization_pow hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have hn0 : n ≠ 0
Tactic: have hn0 : n ≠ 0 := by
      rintro rfl
      simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have mpr : Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k
Tactic: rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ n.primeFactors.card = 1
have simp_rw : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.primeFactors.card = 1
Tactic: simp_rw [isPrimePow_iff_factorization_eq_single, ← Nat.support_factorization,
    Finsupp.card_support_eq_one', pos_iff_ne_zero]