-- Mathlib/NumberTheory/PrimesCongruentOne.lean
theorem exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) :
    ∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Proof state:
case inr
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]

Tactic:
haveI hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩

Result:
case inr
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]

Proof state:
case inr.refine_2
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 : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : k ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]

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

Result:
no goals

Proof state:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs

Tactic:
rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩

Result:
case intro
n k : ℕ
hk0 : k + 1 ≠ 0
hk1 : 1 < k + 1
b : ℕ := (k + 1) * n !
⊢ 1 < (eval (↑b) (cyclotomic (k + 1) ℤ)).natAbs

Proof state:
case inr.refine_2
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 : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this : NeZero ↑k
⊢ p ≡ 1 [MOD k]

Tactic:
have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf

Result:
case inr.refine_2
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 : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]

Proof state:
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
let p := minFac (eval (↑b) (cyclotomic k ℤ)).natAbs

Result:
case inr
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]

Proof state:
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)
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)

Tactic:
have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp

Result:
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 : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)

Proof state:
case intro
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'

Result:
no goals

Proof state:
case inl
n : ℕ
hk0 : 1 ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩

Result:
case inl.intro.intro
n : ℕ
hk0 : 1 ≠ 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Proof state:
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 : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ ↑(eval (↑b) (cyclotomic k ℤ)).natAbs

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

Result:
no goals

Proof state:
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
let b := k * (n !)

Result:
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Proof state:
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 : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)

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]

Result:
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 : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ ↑p ∣ eval (↑b) (cyclotomic k ℤ)