awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesBelow = filter Prime (Ico 1 n)
have h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 1 n)
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesLE = filter Prime (Icc 1 n)
have h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 1 n)
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesBelow = filter Prime (Ico 2 n)
have h : ∀ (p : ℕ), p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 2 n)
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ n.primesLE = filter Prime (Icc 2 n)
have h : ∀ (p : ℕ), p ∈ n.primesLE ↔ p ∈ filter Prime (Icc 2 n)
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
⊢ p ∈ n.primesBelow → p ∈ m.primesBelow
have simp : p < n → Prime p → p < m ∧ Prime p
Tactic: simp [mem_primesBelow]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n m : ℕ
h : n ≤ m
p : ℕ
⊢ p ∈ n.primesLE → p ∈ m.primesLE
have simp : p ≤ n → Prime p → p ≤ m ∧ Prime p
Tactic: simp [mem_primesLE]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow
have rw : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n n.primesBelow else n.primesBelow
Tactic: rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
rw : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n n.primesBelow else n.primesBelow
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow
have rw₁ : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
Tactic: rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
rw : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n n.primesBelow else n.primesBelow
rw₁ : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow
have rw₂ : {p ∈ insert n (range n) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
Tactic: rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
n : ℕ
rw : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n n.primesBelow else n.primesBelow
rw₁ : {p ∈ range (n + 1) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
rw₂ :
  {p ∈ insert n (range n) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
⊢ (n + 1).primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow
have rw₃ : (if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}) =
  if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
Tactic: rw [primesBelow, primesBelow, Finset.range_add_one, Finset.filter_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' (k + n) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
have rw : #({x ∈ Ico 0 k | Prime x} ∪ {x ∈ Ico k (k + n) | Prime x}) ≤
  #({p ∈ Ico 0 k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Tactic: rw [primeCounting', count_eq_card_filter_range, range_eq_Ico, range_eq_Ico, ←
        Ico_union_Ico_eq_Ico (zero_le k) le_self_add, filter_union]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({p ∈ Ico k (k + n) | Prime p})
have rw : #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ count Prime k + #({p ∈ Ico k (k + n) | Prime p})
Tactic: rw [primeCounting', count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
rw : #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ count Prime k + #({p ∈ Ico k (k + n) | Prime p})
⊢ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({p ∈ Ico k (k + n) | Prime p})
have rw₁ : #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p}) ≤
  #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Tactic: rw [primeCounting', count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' k + #({p ∈ Ico k (k + n) | Prime p}) ≤ π' k + #({b ∈ Ico k (k + n) | a.Coprime b})
have bc : ∀ (p : ℕ) (hp : p ∈ Ico k (k + n)), Prime p → a.Coprime p
Tactic: gcongr with p hp
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n p : ℕ
hp : p ∈ Ico k (k + n)
⊢ Prime p → a.Coprime p
have bc : Prime p → p.Coprime a
Tactic: rw [coprime_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' k + #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ π' k + φ a * (n / a + 1)
have rw : #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)
Tactic: rw [add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimeCounting (goal)
Goal:
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π' (k + n + 1) ≤ π k + φ a * (n / a + 1)
have h : k + n + 1 = k + 1 + n
Tactic: convert! primeCounting'_add_le h0 (Order.lt_add_one_iff.mpr h1) n using 2
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have inl : ∀ (hk0 : Ne (α := ℕ) 1 0), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
Tactic: rcases (one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
Cleared hypotheses: k, hk0
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
inl : ∀ (hk0 : Ne (α := ℕ) 1 0), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have inr : ∀ (hk1 : 1 < k), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
Tactic: rcases (one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
n : ℕ
hk0 : Ne (α := ℕ) 1 0
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
have inl : ∀ (p : ℕ) (hnp : n + 1 ≤ p) (hp : Prime p), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]
Tactic: rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
have rcases : ∀ (k : ℕ) (hk0 : k + 1 ≠ 0) (hk1 : 1 < k + 1),
  let b := (k + 1) * n !;
  1 < (eval (↑b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs
Tactic: rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
Cleared hypotheses: k, hk0, hk1, b
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < (eval (↑b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs
have hb : 2 ≤ b
Tactic: have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
Tactic: have hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs := by
    rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
    have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
    calc
      1 ≤ b - 1 := le_tsub_of_add_le_left hb
      _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=
        sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have hprime : Fact (Prime p)
Tactic: haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
⊢ IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
have this : Eq (α := ZMod p) (↑(↑b : ℤ) : ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑b : ℤ))
Tactic: have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : Eq (α := ZMod p) (↑(↑b : ℤ) : ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑b : ℤ))
⊢ IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
have rw : (↑p : ℤ) ∣ eval (↑b : ℤ) (cyclotomic k ℤ)
Tactic: rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom,
      ← Int.cast_natCast, this, eval₂_hom, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : Eq (α := ZMod p) (↑(↑b : ℤ) : ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑b : ℤ))
⊢ (↑p : ℤ) ∣ eval (↑b : ℤ) (cyclotomic k ℤ)
have apply : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs : ℤ)
Tactic: apply Int.dvd_natAbs.1
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have hroot : IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
Tactic: have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) := by
    have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
    rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom,
      ← Int.cast_natCast, this, eval₂_hom, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]
    apply Int.dvd_natAbs.1
    exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have hpb : ¬p ∣ b
Tactic: have hpb : ¬p ∣ b :=
    hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have inr : ∀ (habs : p ≤ n), False
Tactic: refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
inr : ∀ (habs : p ≤ n), False
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
have inr₁ : p ≡ 1 [MOD k]
Tactic: refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
⊢ p ≡ 1 [MOD k]
have hdiv : orderOf (G := ZMod p) (↑b : ZMod p) ∣ p - 1
Tactic: have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=
      ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
hdiv : orderOf (G := ZMod p) (↑b : ZMod p) ∣ p - 1
⊢ p ≡ 1 [MOD k]
have this : NeZero (R := ZMod p) (↑k : ZMod p)
Tactic: haveI : NeZero (k : ZMod p) :=
      NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
hdiv : orderOf (G := ZMod p) (↑b : ZMod p) ∣ p - 1
this : NeZero (R := ZMod p) (↑k : ZMod p)
⊢ p ≡ 1 [MOD k]
have this₁ : k = orderOf (G := ZMod p) (↑b : ZMod p)
Tactic: have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (hypothesis)
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot :
  IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)
hpb : ¬p ∣ b
hdiv : orderOf (G := ZMod p) (↑b : ZMod p) ∣ p - 1
this_1 : NeZero (R := ZMod p) (↑k : ZMod p)
this : k = orderOf (G := ZMod p) (↑b : ZMod p)
⊢ p ≡ 1 [MOD k]
have hdiv₁ : k ∣ p - 1
Tactic: rw [← this] at hdiv
Cleared hypotheses: hdiv, this_1, this
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]
have refine : ∀ (n : ℕ), ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
Tactic: refine frequently_atTop.2 fun n => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.PrimesCongruentOne (goal)
Goal:
k : ℕ
hk0 : k ≠ 0
n : ℕ
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
have obtain : ∀ (p : ℕ) (hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]), ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
Tactic: obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#
have refine : {p ∈ range (n + 1 + 1) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}
Tactic: refine prod_congr ?_ fun _ _ ↦ rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ {p ∈ range (n + 1 + 1) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}
have rw : ∀ (h : Nat.Prime (n + 1)), Even n
Tactic: rw [range_add_one, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m n : ℕ
⊢ (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with Nat.Prime p, p
have simp_rw : ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
  HMul.hMul (α := ℕ) (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) (∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x)
Tactic: simp_rw [primorial, ← Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    HMul.hMul (α := ℕ) (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) (∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x)
have hab : 0 ≤ m + 1
Tactic: rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m n : ℕ
hab : 0 ≤ m + 1
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    HMul.hMul (α := ℕ) (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) (∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x)
have hbc : m + 1 ≤ m + n + 1
Tactic: rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m n : ℕ
hab : 0 ≤ m + 1
hbc : m + 1 ≤ m + n + 1
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    HMul.hMul (α := ℕ) (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) (∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x)
have rw : Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
Tactic: rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}
⊢ p ∣ (m + n).choose m
have hp₁ : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
Tactic: rw [mem_filter, mem_Ico] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
p n : ℕ
hp : Prime p
⊢ p ∣ n# ↔ p ≤ n
have refine : p ∣ n# → p ≤ n
Tactic: refine ⟨?_, fun h ↦ dvd_prod_of_mem _ (by grind)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n#
⊢ p ≤ n
have h₁ : ∃ (a : ℕ), (a ≤ n ∧ Prime a) ∧ p ∣ a
Tactic: simp only [primorial, hp.prime.dvd_finsetProd_iff, mem_filter, mem_range_succ_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
p n : ℕ
hp : Prime p
h : ∃ (a : ℕ), (a ≤ n ∧ Prime a) ∧ p ∣ a
⊢ p ≤ n
have obtain : ∀ (q : ℕ) (hpq : p ∣ q) (hqn : q ≤ n) (hq : Prime q), p ≤ n
Tactic: obtain ⟨q, ⟨hqn, hq⟩, hpq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
n : ℕ
hn : Squarefree n
⊢ n ∣ n#
have this : Dvd.dvd (α := ℕ) (∏ p ∈ n.primeFactors, p) (∏ p ∈ range (n + 1) with Nat.Prime p, p)
Tactic: have : (∏ p ∈ n.primeFactors, p) ∣ (∏ p ∈ range (n + 1) with p.Prime, p) :=
    Finset.prod_dvd_prod_of_subset _ _ _ (by grind [le_of_dvd])
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
hn : Squarefree n
this : Dvd.dvd (α := ℕ) (∏ p ∈ n.primeFactors, p) (∏ p ∈ range (n + 1) with Nat.Prime p, p)
⊢ n ∣ n#
have rwa : ∀ (this : n ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p), n ∣ n#
Tactic: rwa [Nat.prod_primeFactors_of_squarefree hn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
n : ℕ
hn : 2 < n
⊢ n < n#
have this : 3 ≤ n#
Tactic: have : 3 ≤ n# := single_le_prod' (f := id) (by grind [→ Prime.pos]) (by grind [prime_three])
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
⊢ n < q
have by_contra! : ∀ (h1 : q ≤ n), False
Tactic: by_contra! h1
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ≤ n
⊢ False
have h1₁ : q ∣ n#
Tactic: replace h1 : q ∣ n# := (minFac_prime (by lia)).dvd_primorial_iff.2 h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (hypothesis)
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
⊢ n < n#
have this₁ : n < q
Tactic: have : n < q := by
    by_contra! h1
    replace h1 : q ∣ n# := (minFac_prime (by lia)).dvd_primorial_iff.2 h1
    grind [minFac_eq_one_iff, dvd_one, dvd_sub_iff_right, minFac_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
⊢ n ≤ n#
have inl : ∀ (hn : n ≤ 2), n ≤ n#
Tactic: obtain hn | hn := le_or_gt n 2
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
inl : ∀ (hn : n ≤ 2), n ≤ n#
⊢ n ≤ n#
have inr : ∀ (hn : 2 < n), n ≤ n#
Tactic: obtain hn | hn := le_or_gt n 2
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n ≠ 0
⊢ n# < HPow.hPow (α := ℕ) 4 n
have h : ∀ (ihn : ∀ m < 0, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : Ne (α := ℕ) 0 0),
  0# < HPow.hPow (α := ℕ) (β := ℕ) 4 0
Tactic: rcases n with - | n
Cleared hypotheses: n, ihn, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n ≠ 0
h :
  ∀ (ihn : ∀ m < 0, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : Ne (α := ℕ) 0 0),
    0# < HPow.hPow (α := ℕ) (β := ℕ) 4 0
⊢ n# < HPow.hPow (α := ℕ) 4 n
have h₁ : ∀ (n : ℕ) (ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m) (hn : n + 1 ≠ 0),
  (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, ihn, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n + 1 ≠ 0
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
have h : ∀ (m : ℕ) (ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1) (hn : m + m + 1 ≠ 0),
  (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
Tactic: rcases n.even_or_odd with ⟨m, rfl⟩ | ho
Cleared hypotheses: n, ihn, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
n : ℕ
ihn : ∀ m < n + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m
hn : n + 1 ≠ 0
h :
  ∀ (m : ℕ) (ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1) (hn : m + m + 1 ≠ 0),
    (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
⊢ (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
have h₁ : ∀ (ho : Odd n), (n + 1)# < HPow.hPow (α := ℕ) 4 (n + 1)
Tactic: rcases n.even_or_odd with ⟨m, rfl⟩ | ho
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
have h : ∀ (ihn : ∀ m < HAdd.hAdd (α := ℕ) 0 0 + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m)
  (hn : HAdd.hAdd (α := ℕ) 0 0 + 1 ≠ 0),
  (HAdd.hAdd (α := ℕ) 0 0 + 1)# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 0 0 + 1)
Tactic: rcases m.eq_zero_or_pos with rfl | hm
Cleared hypotheses: m, ihn, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
h :
  ∀ (ihn : ∀ m < HAdd.hAdd (α := ℕ) 0 0 + 1, ∀ (hn : m ≠ 0), m# < HPow.hPow (α := ℕ) 4 m)
    (hn : HAdd.hAdd (α := ℕ) 0 0 + 1 ≠ 0),
    (HAdd.hAdd (α := ℕ) 0 0 + 1)# < HPow.hPow (α := ℕ) 4 (HAdd.hAdd (α := ℕ) 0 0 + 1)
⊢ (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
have h₁ : ∀ (hm : m > 0), (m + m + 1)# < HPow.hPow (α := ℕ) 4 (m + m + 1)
Tactic: rcases m.eq_zero_or_pos with rfl | hm
-- Lean 4 proof step from Mathlib.NumberTheory.Primorial (goal)
Goal:
m : ℕ
ihn : ∀ m_1 < m + m + 1, ∀ (hn : m_1 ≠ 0), m_1# < HPow.hPow (α := ℕ) 4 m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#
have rw : (m + 1 + m)# = (m + 1 + m)#
Tactic: rw [add_right_comm]