awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
rw : ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2
have rw₁ : (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2
Tactic: rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
rw : ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
rw₁ : (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2
have rw₂ : (k + 2).minFac * ((k + 2) / m) = k + 2
Tactic: rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
rw : ((k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList).prod = k + 2
rw₁ : (k + 2).minFac * ((k + 2) / (k + 2).minFac).primeFactorsList.prod = k + 2
rw₂ : (k + 2).minFac * ((k + 2) / m) = k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2
have rw₃ : k + 2 = k + 2
Tactic: rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
p : ℕ
hp : Prime p
⊢ p.primeFactorsList = [p]
have this : p = p - 2 + 2
Tactic: have : p = p - 2 + 2 := Nat.eq_add_of_sub_eq hp.two_le rfl
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.primeFactorsList = [p]
have rw : (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
Tactic: rw [this, primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
have simp : p.minFac :: (p / p.minFac).primeFactorsList = [p]
Tactic: simp only [Eq.symm this]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]
have this₁ : p.minFac = p
Tactic: have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
have this : (k + 2) / m < k + 2
Tactic: have : (k + 2) / m < (k + 2) := factors_lemma
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)
have rw : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
Tactic: rw [primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
have refine : ∀ (p : ℕ), Prime p → p ∣ (k + 2) / (k + 2).minFac → (k + 2).minFac ≤ p
Tactic: refine List.IsChain.cons_cons
        ((le_minFac.2 h).resolve_left (by simp)) (isChain_cons_primeFactorsList ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
have rw : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList =
  (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList
Tactic: rw [primeFactorsList]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
have mp : n.primeFactorsList = [] → n = 0 ∨ n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
mp : n.primeFactorsList = [] → n = 0 ∨ n = 1
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
have mpr : n = 0 ∨ n = 1 → n.primeFactorsList = []
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1
have mp : ∀ (h : primeFactorsList 0 = []), Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
h : n.primeFactorsList = []
mp : ∀ (h : primeFactorsList 0 = []), Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
⊢ n = 0 ∨ n = 1
have mp₁ : ∀ (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList = []), HAdd.hAdd (α := ℕ) 0 1 = 0 ∨ HAdd.hAdd (α := ℕ) 0 1 = 1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
h : n.primeFactorsList = []
mp : ∀ (h : primeFactorsList 0 = []), Eq (α := ℕ) 0 0 ∨ Eq (α := ℕ) 0 1
mp₁ : ∀ (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList = []), HAdd.hAdd (α := ℕ) 0 1 = 0 ∨ HAdd.hAdd (α := ℕ) 0 1 = 1
⊢ n = 0 ∨ n = 1
have mp₂ : ∀ (n : ℕ) (h : (n + 1 + 1).primeFactorsList = []), n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
have h₁ : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
Tactic: rw [primeFactorsList] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []
have mpr : primeFactorsList 0 = []
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
h : n = 0 ∨ n = 1
mpr : primeFactorsList 0 = []
⊢ n.primeFactorsList = []
have mpr₁ : primeFactorsList 1 = []
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ∣ n
have inl : ∀ (h : p ∈ primeFactorsList 0), p ∣ 0
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
inl : ∀ (h : p ∈ primeFactorsList 0), p ∣ 0
⊢ p ∣ n
have inr : ∀ (hn : n > 0), p ∣ n
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
have zero : p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ Ne (α := ℕ) 0 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
zero : p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ Ne (α := ℕ) 0 0
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0
have succ : ∀ (n : ℕ), p ∈ (n + 1).primeFactorsList ↔ Prime p ∧ p ∣ n + 1 ∧ n + 1 ≠ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ≤ n
have inl : ∀ (h : p ∈ primeFactorsList 0), p ≤ 0
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
h : p ∈ n.primeFactorsList
inl : ∀ (h : p ∈ primeFactorsList 0), p ≤ 0
⊢ p ≤ n
have inr : ∀ (hn : n > 0), p ≤ n
Tactic: rcases n.eq_zero_or_pos with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0
have h₁ : Membership.mem (γ := List ℕ) [] p
Tactic: rw [primeFactorsList_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ n.primeFactorsList
have refine_1 : l.prod = n.primeFactorsList.prod
Tactic: refine perm_of_prod_eq_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_1 : l.prod = n.primeFactorsList.prod
⊢ l ~ n.primeFactorsList
have refine_2 : ∀ (p : ℕ), p ∈ l → _root_.Prime p
Tactic: refine perm_of_prod_eq_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
refine_1 : l.prod = n.primeFactorsList.prod
refine_2 : ∀ (p : ℕ), p ∈ l → _root_.Prime p
⊢ l ~ n.primeFactorsList
have refine_3 : ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p
Tactic: refine perm_of_prod_eq_prod ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l.prod = n.primeFactorsList.prod
have refine_1 : n = n.primeFactorsList.prod
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = n.primeFactorsList.prod
have refine_1 : n ≠ 0
Tactic: refine (prod_primeFactorsList ?_).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : l.prod = 0
⊢ False
have h₃ : 0 ∈ l
Tactic: rw [prod_eq_zero_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p
have refine_3 : ∀ (p : ℕ), p ∈ n.primeFactorsList → Prime p
Tactic: simp_rw [← prime_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ (p ^ n).primeFactorsList = replicate n p
have symm : replicate n p = (p ^ n).primeFactorsList
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = (p ^ n).primeFactorsList
have rw : replicate n p ~ (p ^ n).primeFactorsList
Tactic: rw [← List.replicate_perm]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList
have apply : ∀ (p_1 : ℕ), p_1 ∈ replicate n p → Prime p_1
Tactic: apply Nat.primeFactorsList_unique (List.prod_replicate n p)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k
have rw : n.primeFactorsList.prod = p ^ k
Tactic: rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
rw : n.primeFactorsList.prod = p ^ k
⊢ n = p ^ k
have rw₁ : n.primeFactorsList.prod = (replicate k p).prod
Tactic: rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
rw : n.primeFactorsList.prod = p ^ k
rw₁ : n.primeFactorsList.prod = (replicate k p).prod
⊢ n = p ^ k
have rw₂ : (replicate n.primeFactorsList.length p).prod = (replicate k p).prod
Tactic: rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
    h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have refine_1 : (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
Tactic: refine (primeFactorsList_unique ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
refine_1 : (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have refine_2 : ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p
Tactic: refine (primeFactorsList_unique ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
have refine_1 : a.primeFactorsList.prod * b.primeFactorsList.prod = a * b
Tactic: rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
refine_1 : a.primeFactorsList.prod * b.primeFactorsList.prod = a * b
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
have refine_1₁ : a * b.primeFactorsList.prod = a * b
Tactic: rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
refine_1 : a.primeFactorsList.prod * b.primeFactorsList.prod = a * b
refine_1₁ : a * b.primeFactorsList.prod = a * b
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
have refine_1₂ : a * b = a * b
Tactic: rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ Prime p
have hp₁ : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
Tactic: rw [List.mem_append] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p
have refine_2 : ∀ (hp' : p ∈ a.primeFactorsList), Prime p
Tactic: rcases hp with hp' | hp'
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
refine_2 : ∀ (hp' : p ∈ a.primeFactorsList), Prime p
⊢ Prime p
have refine_2₁ : ∀ (hp' : p ∈ b.primeFactorsList), Prime p
Tactic: rcases hp with hp' | hp'
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have inl : ∀ (hab : Coprime 0 b), (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList
Tactic: rcases a.eq_zero_or_pos with (rfl | ha)
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
inl : ∀ (hab : Coprime 0 b), (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have inr : ∀ (ha : a > 0), (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
Tactic: rcases a.eq_zero_or_pos with (rfl | ha)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have inr : ∀ (hab : a.Coprime 0), (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
ha : a > 0
inr : ∀ (hab : a.Coprime 0), (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
have inr₁ : ∀ (hb : b > 0), (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList <+ (n * k).primeFactorsList
have zero : primeFactorsList 0 <+ (0 * k).primeFactorsList
Tactic: rcases n with - | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k : ℕ
h : k ≠ 0
zero : primeFactorsList 0 <+ (0 * k).primeFactorsList
⊢ n.primeFactorsList <+ (n * k).primeFactorsList
have succ : ∀ (hn : ℕ), (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList
Tactic: rcases n with - | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList
have apply : (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList
Tactic: apply sublist_of_subperm_of_pairwise _
    (primeFactorsList_sorted _).pairwise (primeFactorsList_sorted _).pairwise
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList
have simp : (hn + 1).primeFactorsList <+~ hn.succ.primeFactorsList ++ k.primeFactorsList
Tactic: simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ n.primeFactorsList <+ k.primeFactorsList
have obtain : ∀ (a : ℕ) (h' : n * a ≠ 0), n.primeFactorsList <+ (n * a).primeFactorsList
Tactic: obtain ⟨a, rfl⟩ := h
Cleared hypotheses: k, h, h'
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
⊢ a ∣ b
have inl : ∀ (h : a.primeFactorsList <+~ primeFactorsList 0), a ∣ 0
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
inl : ∀ (h : a.primeFactorsList <+~ primeFactorsList 0), a ∣ 0
⊢ a ∣ b
have inr : ∀ (hb : b > 0), a ∣ b
Tactic: rcases b.eq_zero_or_pos with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b
have inr : ∀ (ha : Ne (α := ℕ) 0 0) (h : primeFactorsList 0 <+~ b.primeFactorsList), 0 ∣ b
Tactic: rcases a with (_ | _ | a)
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
inr : ∀ (ha : Ne (α := ℕ) 0 0) (h : primeFactorsList 0 <+~ b.primeFactorsList), 0 ∣ b
⊢ a ∣ b
have inr₁ : ∀ (ha : HAdd.hAdd (α := ℕ) 0 1 ≠ 0) (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList <+~ b.primeFactorsList),
  HAdd.hAdd (α := ℕ) 0 1 ∣ b
Tactic: rcases a with (_ | _ | a)
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
inr : ∀ (ha : Ne (α := ℕ) 0 0) (h : primeFactorsList 0 <+~ b.primeFactorsList), 0 ∣ b
inr₁ :
  ∀ (ha : HAdd.hAdd (α := ℕ) 0 1 ≠ 0) (h : (HAdd.hAdd (α := ℕ) 0 1).primeFactorsList <+~ b.primeFactorsList),
    HAdd.hAdd (α := ℕ) 0 1 ∣ b
⊢ a ∣ b
have inr₂ : ∀ (a : ℕ) (ha : a + 1 + 1 ≠ 0) (h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList), a + 1 + 1 ∣ b
Tactic: rcases a with (_ | _ | a)
Cleared hypotheses: a, ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b
have h₁ : b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Tactic: use (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1) * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
have h₁ : b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Tactic: nth_rw 1 [← Nat.prod_primeFactorsList ha]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
have h₁ : b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Tactic: rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
h₁ : b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
have h₂ : b = b.primeFactorsList.prod
Tactic: rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
h₁ : b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
h₂ : b = b.primeFactorsList.prod
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
have h₃ : b = b
Tactic: rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b
have succ : replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
succ : replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b
⊢ replicate (n + 1) a <+~ b.primeFactorsList ↔ a ^ (n + 1) ∣ b
have succ₁ : a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b
have succ : (∃ (l : List ℕ), l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b
Tactic: rw [List.subperm_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b
have succ : (replicate (n + 1) a).prod ∣ u.prod
Tactic: rw [← Nat.prod_primeFactorsList hb, ← hu1.prod_eq, ← prod_replicate]
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (hypothesis)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : a ^ (n + 1) * c ≠ 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
have hb₁ : ¬a = 0 ∧ ¬a ^ n * c = 0
Tactic: rw [Ne, pow_succ', mul_assoc, mul_eq_zero, _root_.not_or] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Nat.Factors (goal)
Goal:
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ} (hb : b ≠ 0), replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
have succ : a ^ n ∣ a ^ n * c
Tactic: rw [pow_succ', mul_assoc, replicate_succ,
        (Nat.perm_primeFactorsList_mul hb.1 hb.2).subperm_left, primeFactorsList_prime ha,
        singleton_append, subperm_cons, ih hb.2]