awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
simp_rw : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.primeFactors.card = 1
⊢ IsPrimePow n ↔ n.primeFactors.card = 1
have simp_rw₁ : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.factorization.support.card = 1
Tactic: simp_rw [isPrimePow_iff_factorization_eq_single, ← Nat.support_factorization,
    Finsupp.card_support_eq_one', pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
simp_rw : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.primeFactors.card = 1
simp_rw₁ : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔ n.factorization.support.card = 1
⊢ IsPrimePow n ↔ n.primeFactors.card = 1
have simp_rw₂ : (∃ (p : ℕ) (k : ℕ), 0 < k ∧ n.factorization = Finsupp.single p k) ↔
  ∃ (a : ℕ) (b : ℕ), b ≠ 0 ∧ n.factorization = Finsupp.single a b
Tactic: simp_rw [isPrimePow_iff_factorization_eq_single, ← Nat.support_factorization,
    Finsupp.card_support_eq_one', pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : 2 ≤ n
⊢ ¬IsPrimePow n ↔ n.primeFactors.Nontrivial
have rw : ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card
Tactic: rw [isPrimePow_iff_card_primeFactors_eq_one, ← Finset.one_lt_card_iff_nontrivial]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inl : ∀ (h : IsPrimePow (R := ℕ) 0),
  ∃ (p : ℕ), Nat.Prime p ∧ 0 / HPow.hPow (β := ℕ) p ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn0)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
inl :
  ∀ (h : IsPrimePow (R := ℕ) 0),
    ∃ (p : ℕ), Nat.Prime p ∧ 0 / HPow.hPow (β := ℕ) p ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : ∀ (hn0 : n ≠ 0), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rcases eq_or_ne n 0 with (rfl | hn0)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : ∀ (p k : ℕ) (hk0 : 0 < k) (h1 : n.factorization = Finsupp.single p k),
  ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rcases isPrimePow_iff_factorization_eq_single.mp h with ⟨p, k, hk0, h1⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : ∀ (pp : ¬Nat.Prime p), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
inr :
  ∀ (pp : ¬Nat.Prime p), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr₁ : ∀ (pp : Nat.Prime p), ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: rcases em' p.Prime with (pp | pp)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : k = 0
Tactic: refine absurd ?_ hk0.ne'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: refine ⟨p, pp, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have inr : ∀ (q : ℕ),
  Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)
Tactic: refine Nat.eq_of_factorization_eq (Nat.ordCompl_pos p hn0).ne' (by simp) fun q => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ Eq (α := ℕ) (((n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).factorization : (a : ℕ) → ℕ) q : ℕ)
    ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)
have inr : Eq (α := ℕ) ((Finsupp.erase p (Finsupp.single p k) : (a : ℕ) → ℕ) q : ℕ) ((Nat.factorization 1 : (a : ℕ) → ℕ) q : ℕ)
Tactic: rw [Nat.factorization_ordCompl n p, h1]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : n ≠ 1
⊢ IsPrimePow n ↔ ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have refine : ∀ (h : ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1), IsPrimePow n
Tactic: refine ⟨fun h => IsPrimePow.exists_ordCompl_eq_one h, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : n ≠ 1
h : ∃ (p : ℕ), Nat.Prime p ∧ n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ IsPrimePow n
have rcases : ∀ (p : ℕ) (pp : Nat.Prime p) (h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1), IsPrimePow n
Tactic: rcases h with ⟨p, pp, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ IsPrimePow n
have rw : ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: rw [isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have rw : ∀ (hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1) (pp : Nat.Prime p)
  (h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1),
  ∃ (p_1 : ℕ) (k : ℕ), Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← Nat.eq_of_dvd_of_div_eq_one (Nat.ordProj_dvd n p) h] at hn ⊢
Cleared hypotheses: hn, pp, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ ∃ (p_1 : ℕ) (k : ℕ), Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have refine : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: refine ⟨p, n.factorization p, pp, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hn : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) ≠ 1
pp : Nat.Prime p
h : n / HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have contrapose! : ∀ (hn : LE.le (α := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
⊢ IsPrimePow n ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
have rw : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
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 : ℕ, Nat.Prime p ∧ p ∣ n
have mp : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : ℕ
mp : (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
⊢ (∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
have mpr : (∃! p : ℕ, Nat.Prime p ∧ p ∣ n) → ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃! p_1 : ℕ, Nat.Prime p_1 ∧ p_1 ∣ p ^ k
have mp : ∀ (y : ℕ), (fun (p_1 : ℕ) ↦ Nat.Prime p_1 ∧ p_1 ∣ p ^ k) y → y = p
Tactic: refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have mpr : ∀ (hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ 0) y → y = p) (hn : p ∣ 0),
  ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
Tactic: rcases eq_or_ne n 0 with (rfl | hn₀)
Cleared hypotheses: n, hq, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
mpr :
  ∀ (hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ 0) y → y = p) (hn : p ∣ 0),
    ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have mpr₁ : ∀ (hn₀ : n ≠ 0), ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Tactic: rcases eq_or_ne n 0 with (rfl | hn₀)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
have mpr : HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
Tactic: refine ⟨p, n.factorization p, hp, hp.factorization_pos_of_dvd hn₀ hn, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
n p : ℕ
hq : ∀ (y : ℕ), (fun (p : ℕ) ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
have hq₁ : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
Tactic: simp only [and_imp] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) = n
have mpr : n ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: apply Nat.dvd_antisymm (Nat.ordProj_dvd _ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n ∣ HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
have mpr : n.primeFactorsList.Subperm (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).primeFactorsList
Tactic: apply Nat.dvd_of_primeFactorsList_subperm hn₀
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ n.primeFactorsList.Subperm (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)).primeFactorsList
have mpr : ∀ x ∈ n.primeFactorsList,
  List.count x n.primeFactorsList ≤ List.count x (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
Tactic: rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : q ∈ n.primeFactorsList
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
have hq'₁ : Nat.Prime q ∧ q ∣ n
Tactic: rw [Nat.mem_primeFactorsList hn₀] at hq'
Cleared hypotheses: hq'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
have mpr : ∀ (hq' : Nat.Prime p ∧ p ∣ n),
  List.count p n.primeFactorsList ≤ List.count p (List.replicate ((n.factorization : (a : ℕ) → ℕ) p) p)
Tactic: cases hq _ hq'.1 hq'.2
Cleared hypotheses: q, hq'
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n k : ℕ
hk : k ≠ 0
⊢ IsPrimePow (n ^ k) ↔ IsPrimePow n
have simp : (∃! p : ℕ, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
Tactic: simp only [isPrimePow_iff_unique_prime_dvd]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n k : ℕ
hk : k ≠ 0
⊢ (∃! p : ℕ, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p : ℕ, Nat.Prime p ∧ p ∣ n
have h : ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
Tactic: apply existsUnique_congr
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
have inl : ∀ (hab : Coprime 0 b), n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
inl : ∀ (hab : Coprime 0 b), n ∣ 0 * b ↔ n ∣ 0 ∨ n ∣ b
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
have inr : ∀ (ha : a ≠ 0), n ∣ a * b ↔ n ∣ a ∨ n ∣ b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
have inr : ∀ (hab : a.Coprime 0), n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
inr : ∀ (hab : a.Coprime 0), n ∣ a * 0 ↔ n ∣ a ∨ n ∣ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
have inr₁ : ∀ (hb : b ≠ 0), n ∣ a * b ↔ n ∣ a ∨ n ∣ b
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b ↔ n ∣ a ∨ n ∣ b
have inr : n ∣ a * b → n ∣ a ∨ n ∣ b
Tactic: refine
    ⟨?_, fun h =>
      Or.elim h (fun i => i.trans ((@dvd_mul_right a b a hab).mpr (dvd_refl a)))
          fun i => i.trans ((@dvd_mul_left a b b hab.symm).mpr (dvd_refl b))⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n a b : ℕ
hab : a.Coprime b
hn : IsPrimePow n
ha : a ≠ 0
hb : b ≠ 0
⊢ n ∣ a * b → n ∣ a ∨ n ∣ b
have inr : ∀ (p k : ℕ) (hp : Prime p), 0 < k → ∀ (hn : IsPrimePow (p ^ k)), p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
Tactic: obtain ⟨p, k, hp, _, rfl⟩ := (isPrimePow_nat_iff _).1 hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
⊢ p ^ k ∣ a * b → p ^ k ∣ a ∨ p ^ k ∣ b
have inr : k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
  k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
Tactic: simp only [hp.pow_dvd_iff_le_factorization (mul_ne_zero ha hb), Nat.factorization_mul ha hb,
    hp.pow_dvd_iff_le_factorization ha, hp.pow_dvd_iff_le_factorization hb, Pi.add_apply,
    Finsupp.coe_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
⊢ Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
have rw : p ∉ a.factorization.support ∩ b.factorization.support
Tactic: rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ←
      Finset.mem_inter]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
have this : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
  Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
Tactic: have : a.factorization p = 0 ∨ b.factorization p = 0 := by
    rw [← Finsupp.notMem_support_iff, ← Finsupp.notMem_support_iff, ← not_and_or, ←
      Finset.mem_inter]
    intro t
    simpa using hab.disjoint_primeFactors.le_bot t
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
this :
  Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
have inr : ∀ (h : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
p k : ℕ
hp : Prime p
left : 0 < k
hn : IsPrimePow (p ^ k)
this :
  Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ) ∨
    Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
inr :
  ∀ (h : Eq (α := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
      k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
⊢ k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
have inr₁ : ∀ (h : Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
  k ≤ HAdd.hAdd (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) →
    k ≤ (a.factorization : (a : ℕ) → ℕ) p ∨ k ≤ (b.factorization : (a : ℕ) → ℕ) p
Tactic: rcases this with h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inl : ∀ (hab : Coprime 0 b), {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
inl : ∀ (hab : Coprime 0 b), {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inr : ∀ (ha : a ≠ 0), {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
b : ℕ
hab : Coprime 0 b
⊢ {d ∈ (0 * b).divisors | IsPrimePow d} = {d ∈ divisors 0 ∪ b.divisors | IsPrimePow d}
have hab₁ : b = 1
Tactic: simp only [Nat.coprime_zero_left] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inr : ∀ (hab : a.Coprime 0), {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
inr : ∀ (hab : a.Coprime 0), {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inr₁ : ∀ (hb : b ≠ 0), {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (hypothesis)
Goal:
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}
have hab₁ : a = 1
Tactic: simp only [Nat.coprime_zero_right] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
⊢ {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inr : ∀ (n : ℕ), n ∈ {d ∈ (a * b).divisors | IsPrimePow d} ↔ n ∈ {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a ≠ 0
hb : b ≠ 0
n : ℕ
⊢ n ∈ {d ∈ (a * b).divisors | IsPrimePow d} ↔ n ∈ {d ∈ a.divisors ∪ b.divisors | IsPrimePow d}
have inr : IsPrimePow n → (n ∣ a * b ↔ n ∣ a ∨ n ∣ b)
Tactic: simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true, Ne,
    and_congr_left_iff, not_false_iff, Nat.mem_divisors, or_self_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factorization.PrimePow (goal)
Goal:
n : { n : ℕ // IsPrimePow n }
⊢ (fun (pk : Primes × ℕ) ↦
        (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) ⋯ : { n : ℕ // IsPrimePow n }))
      ((fun (n : { n : ℕ // IsPrimePow n }) ↦
          (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac ⋯,
            HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
        n) =
    n
have a : (↑((fun (pk : Primes × ℕ) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ IsPrimePow n) ((↑pk.1 : ℕ) ^ (pk.2 + 1)) sorry : { n : ℕ // IsPrimePow n }))
        ((fun (n : { n : ℕ // IsPrimePow n }) ↦
            (Subtype.mk (p := fun (p : ℕ) ↦ Prime p) (↑n : ℕ).minFac sorry,
              HSub.hSub (α := ℕ) (β := ℕ) (((↑n : ℕ).factorization : (a : ℕ) → ℕ) (↑n : ℕ).minFac : ℕ) (1 : ℕ)))
          n)) :
    ℕ) =
  (↑n : ℕ)
Tactic: ext1