awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
hb : 2 ≤ b
⊢ 1 < (eval (↑b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs

Tactic:
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'

Premises used: Polynomial.eval, le_tsub_of_add_le_left, Polynomial.sub_one_lt_natAbs_cyclotomic_eval, Polynomial.cyclotomic, Int, Nat.cast, LT.lt.ne', HAdd.hAdd, Int.natAbs, Iff.mp, OfNat.ofNat, Nat.succ_le_iff
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 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'
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
⊢ Fact (Prime p)

Tactic:
haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
⊢ Eq (α := ZMod p) (↑(↑b : ℤ) : ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) (↑b : ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
⊢ 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
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : ℤ))
rw : (↑p : ℤ) ∣ eval (↑b : ℤ) (cyclotomic k ℤ)
⊢ IsRoot (R := ZMod p) (cyclotomic k (ZMod p) : (ZMod p)[X]) ((castRingHom (ZMod p) : (a : ℕ) → ZMod p) b : ZMod p)

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]

Premises used: Int.cast_natCast, Polynomial.eval_map, Polynomial.eval₂_hom, Int.coe_castRingHom, Polynomial.IsRoot.def, ZMod, ZMod.intCast_zmod_eq_zero_iff_dvd, Polynomial.map_cyclotomic_int, Nat.coe_castRingHom
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : ℤ))
apply : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs : ℤ)
⊢ (↑p : ℤ) ∣ eval (↑b : ℤ) (cyclotomic k ℤ)

Tactic:
apply Int.dvd_natAbs.1

Premises used: Int.dvd_natAbs, Iff.mp
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : ℤ))
⊢ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs : ℤ)

Tactic:
mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs

Premises used: Polynomial.eval, Polynomial.cyclotomic, cast, Nat.minFac_dvd, Int, Nat.cast, Int.natAbs, Eq.symm, Int.ofNat_dvd._simp_1
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : ℤ))
⊢ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(eval (↑b : ℤ) (cyclotomic k ℤ)).natAbs : ℤ)

Tactic:
exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs

Premises used: Polynomial.eval, Polynomial.cyclotomic, Nat.minFac_dvd, Int, Int.natAbs
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)

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
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 ∣ b

Tactic:
have hpb : ¬p ∣ b :=
    hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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]

Tactic:
⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩

Premises used: not_le, And.intro, Exists.intro, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
inr₁ : p ≡ 1 [MOD k]
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
habs : p ≤ n
⊢ False

Tactic:
hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)

Premises used: dvd_mul_of_dvd_right, Nat.dvd_factorial, Nat.minFac_pos
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
habs : p ≤ n
⊢ False

Tactic:
exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)

Premises used: dvd_mul_of_dvd_right, Nat.dvd_factorial, Nat.minFac_pos
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
⊢ 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)
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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
⊢ 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 _)
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
⊢ k = orderOf (G := ZMod p) (↑b : ZMod p)

Tactic:
have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
⊢ k ∣ p - 1

Tactic:
rw [← this] at hdiv
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
hdiv₁ : k ∣ p - 1
⊢ NeZero (R := ZMod p) (↑k : ZMod p)

Tactic:
rw [← this] at hdiv
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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)
hdiv₁ : k ∣ p - 1
this₁ : NeZero (R := ZMod p) (↑k : ZMod p)
⊢ k = orderOf (G := ZMod p) (↑b : ZMod p)

Tactic:
rw [← this] at hdiv
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : k ∣ p - 1
this_1 : NeZero (R := ZMod p) (↑k : ZMod p)
this : k = orderOf (G := ZMod p) (↑b : ZMod p)
⊢ p ≡ 1 [MOD k]

Tactic:
((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm

Premises used: Iff.mpr, Nat.Prime.pos, Nat.modEq_iff_dvd', Nat.ModEq.symm, Fact.out
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
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 : k ∣ p - 1
this_1 : NeZero (R := ZMod p) (↑k : ZMod p)
this : k = orderOf (G := ZMod p) (↑b : ZMod p)
⊢ p ≡ 1 [MOD k]

Tactic:
exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm

Premises used: Iff.mpr, Nat.Prime.pos, Nat.modEq_iff_dvd', Nat.ModEq.symm, Fact.out
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]

Tactic:
frequently_atTop.2 fun n => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
refine : ∀ (n : ℕ), ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ 1 [MOD k]

Tactic:
refine frequently_atTop.2 fun n => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
n : ℕ
obtain : ∀ (p : ℕ) (hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]), ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Tactic:
obtain ⟨p, hp⟩ := exists_prime_gt_modEq_one n hk0

Premises used: Nat.exists_prime_gt_modEq_one
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Tactic:
⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
n p : ℕ
hp : Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
⊢ ∃ b ≥ n, Prime b ∧ b ≡ 1 [MOD k]

Tactic:
exact ⟨p, ⟨hp.2.1.le, hp.1, hp.2.2⟩⟩
-- Module: Mathlib.NumberTheory.PrimesCongruentOne
Goal:
k : ℕ
hk0 : k ≠ 0
⊢ Set.Infinite (α := ℕ) {p : ℕ | Prime p ∧ p ≡ 1 [MOD k]}

Tactic:
frequently_atTop_iff_infinite.1 (frequently_atTop_modEq_one hk0)

Premises used: Nat.frequently_atTop_modEq_one, Nat.frequently_atTop_iff_infinite, Iff.mp
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
⊢ n# = ∏ p ∈ n.primesLE, p

Tactic:
rfl

Premises used: Nat.primesLE, primorial, rfl, Nat.primesBelow
-- Module: Mathlib.NumberTheory.Primorial
Goal:
⊢ 0# = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Primorial
Goal:
⊢ 1# = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Primorial
Goal:
⊢ 2# = 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
⊢ 0 < n#

Tactic:
prod_pos fun _p hp ↦ (mem_filter.1 hp).2.pos

Premises used: Nat.Prime.pos, And.right, Finset.prod_pos, Iff.mp, Finset.mem_filter, primorial
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : m ≤ n
⊢ {p ∈ range (m + 1) | Nat.Prime p} ⊆ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : m ≤ n
⊢ ∀ i ∈ {p ∈ range (n + 1) | Nat.Prime p}, i ∉ {p ∈ range (m + 1) | Nat.Prime p} → 1 ≤ i

Tactic:
grind
-- Module: Mathlib.NumberTheory.Primorial
Goal:
⊢ Monotone primorial

Tactic:
fun _ _ ↦ primorial_mono

Premises used: Monotone, primorial_mono
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#

Tactic:
prod_congr ?_ fun _ _ ↦ rfl

Premises used: Finset.prod_congr, primorial, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
refine : {p ∈ range (n + 1 + 1) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}
⊢ (n + 1)# = n#

Tactic:
refine prod_congr ?_ fun _ _ ↦ rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
rw : ∀ (h : Nat.Prime (n + 1)), Even n
⊢ {p ∈ range (n + 1 + 1) | Nat.Prime p} = {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
rw [range_add_one, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]

Premises used: Iff.mpr, Nat.not_even_iff_odd, Finset.range_add_one, Finset.filter_insert, if_neg
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ ∀ (h : Nat.Prime (n + 1)), Even n

Tactic:
fun h ↦ h.even_sub_one <| mt succ.inj hn1

Premises used: mt, Nat.Prime.even_sub_one, Nat.succ.inj, Nat.pred
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ ∀ (h : Nat.Prime (n + 1)), Even n

Tactic:
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
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)
⊢ (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with Nat.Prime p, p

Tactic:
simp_rw [primorial, ← Ico_zero_eq_range]

Premises used: Nat.Ico_zero_eq_range, primorial
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
hab : 0 ≤ m + 1
hbc : m + 1 ≤ m + n + 1
rw : Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
⊢ ∏ 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:
rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]

Premises used: Finset.prod_union, Finset.Ico_union_Ico_eq_Ico, Finset.filter_union
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
⊢ 0 ≤ m + 1

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
⊢ m + 1 ≤ m + n + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})

Tactic:
disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _

Premises used: Finset.Ico_disjoint_Ico_consecutive, Finset.disjoint_filter_filter
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
⊢ 0 ≤ m + 1

Tactic:
exacts [Nat.zero_le _, by lia, disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]

Premises used: Nat.zero_le, Finset.Ico_disjoint_Ico_consecutive, Finset.disjoint_filter_filter
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}
⊢ (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p

Tactic:
rw [mem_filter, mem_Ico] at hp

Premises used: Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Tactic:
hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
              (Nat.lt_succ_iff.1 hp.1.2)

Premises used: Nat.lt_succ_self, And.right, Nat.lt_succ_iff, And.left, LT.lt.trans_le, Nat.Prime.dvd_choose_add, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Tactic:
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1))
              (Nat.lt_succ_iff.1 hp.1.2)

Premises used: Nat.lt_succ_self, And.right, Nat.lt_succ_iff, And.left, LT.lt.trans_le, Nat.Prime.dvd_choose_add, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Primorial
Goal:
m n : ℕ
h : n ≤ m
⊢ (m + n)# ≤ m# * (m + n).choose m

Tactic:
le_of_dvd (mul_pos (primorial_pos _) (choose_pos <| Nat.le_add_right _ _)) (primorial_add_dvd h)

Premises used: Nat.le_add_right, primorial_pos, primorial_add_dvd, mul_pos, Nat.choose_pos, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
h : p ≤ n
⊢ p ∈ {p ∈ range (n + 1) | Prime p}

Tactic:
grind
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
refine : p ∣ n# → p ≤ n
⊢ p ∣ n# ↔ p ≤ n

Tactic:
refine ⟨?_, fun h ↦ dvd_prod_of_mem _ (by grind)⟩
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n#
⊢ ∃ (a : ℕ), (a ≤ n ∧ Prime a) ∧ p ∣ a

Tactic:
simp only [primorial, hp.prime.dvd_finsetProd_iff, mem_filter, mem_range_succ_iff] at h

Premises used: Finset.mem_range_succ_iff, Prime.dvd_finsetProd_iff, Nat.Prime.prime, Finset.mem_filter, primorial
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
h : ∃ (a : ℕ), (a ≤ n ∧ Prime a) ∧ p ∣ a
obtain : ∀ (q : ℕ) (hpq : p ∣ q) (hqn : q ≤ n) (hq : Prime q), p ≤ n
⊢ p ≤ n

Tactic:
obtain ⟨q, ⟨hqn, hq⟩, hpq⟩ := h
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
q : ℕ
hpq : p ∣ q
hqn : q ≤ n
hq : Prime q
⊢ p ≤ n

Tactic:
(Nat.le_of_dvd hq.pos hpq).trans hqn

Premises used: Nat.Prime.pos, LE.le.trans, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p n : ℕ
hp : Prime p
q : ℕ
hpq : p ∣ q
hqn : q ≤ n
hq : Prime q
⊢ p ≤ n

Tactic:
exact (Nat.le_of_dvd hq.pos hpq).trans hqn

Premises used: Nat.Prime.pos, LE.le.trans, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Primorial
Goal:
p : ℕ
hp : Prime p
⊢ p ∣ p#

Tactic:
hp.dvd_primorial_iff.2 le_rfl

Premises used: Iff.mpr, le_rfl, Nat.Prime.dvd_primorial_iff
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : Squarefree n
⊢ n.primeFactors ⊆ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
grind [le_of_dvd]

Premises used: Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : Squarefree n
⊢ 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])
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : Squarefree n
this : Dvd.dvd (α := ℕ) (∏ p ∈ n.primeFactors, p) (∏ p ∈ range (n + 1) with Nat.Prime p, p)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : n ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p), n ∣ n#
⊢ n ∣ n#

Tactic:
rwa [Nat.prod_primeFactors_of_squarefree hn] at this

Premises used: Nat.prod_primeFactors_of_squarefree
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
⊢ ∀ i ∈ {p ∈ range (n + 1) | Nat.Prime p}, 1 ≤ id i

Tactic:
grind [→ Prime.pos]

Premises used: Nat.Prime.pos
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
⊢ 3 ∈ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
grind [prime_three]

Premises used: Nat.prime_three
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
⊢ 3 ≤ n#

Tactic:
have : 3 ≤ n# := single_le_prod' (f := id) (by grind [→ Prime.pos]) (by grind [prime_three])
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
by_contra! : ∀ (h1 : q ≤ n), False
⊢ n < q

Tactic:
by_contra! h1
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ≤ n
⊢ n# - 1 ≠ 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ≤ n
⊢ q ∣ n#

Tactic:
replace h1 : q ∣ n# := (minFac_prime (by lia)).dvd_primorial_iff.2 h1
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ∣ n#
⊢ False

Tactic:
grind [minFac_eq_one_iff, dvd_one, dvd_sub_iff_right, minFac_dvd]

Premises used: Nat.dvd_one, Nat.minFac_dvd, Nat.minFac_eq_one_iff, Nat.dvd_sub_iff_right
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
⊢ 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]
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : 2 < n
this_1 : 3 ≤ n#
q : ℕ := (n# - 1).minFac
this : n < q
⊢ n < n#

Tactic:
grind [Nat.minFac_le]

Premises used: Nat.minFac_le
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
inl : ∀ (hn : n ≤ 2), n ≤ n#
inr : ∀ (hn : 2 < n), n ≤ n#
⊢ n ≤ n#

Tactic:
obtain hn | hn := le_or_gt n 2

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Primorial
Goal:
n : ℕ
hn : n ≤ 2
⊢ n ≤ n#

Tactic:
decide +revert