Theorem: Imo2008P3.p_lemma (Compfiles/Imo2008P3.lean)

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
haveI := Fact.mk hpp
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1]
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
let m := ZMod.valMinAbs y
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
let n := Int.natAbs m
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₁ : p ∣ n ^ 2 + 1 := by
  refine Int.natCast_dvd_natCast.mp ?_
  simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
  refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
  simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
  rw [pow_two, ← hy]; exact add_left_neg 1
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₃ : p ≥ 2 * n := by omega
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
set k : ℕ := p - 2 * n with hnat₄
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₅ : p ∣ k ^ 2 + 4 := by
  cases' hnat₁ with x hx
  have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
    use (p : ℤ) - 4 * n + 4 * x
    have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
    have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
    linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
  assumption_mod_cast
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hnat₆ : k ^ 2 + 4 ≥ p := Nat.le_of_dvd (k ^ 2 + 3).succ_pos hnat₅
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₁ : (k : ℝ) = p - 2 * n := by assumption_mod_cast
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₂ : (p : ℝ) > 20 := by assumption_mod_cast
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₅ : (k : ℝ) > 4 := by
  refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
  linarith only [hreal₂, hreal₃]
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
have hreal₆ : (k : ℝ) > sqrt (2 * n) := by
  refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
  rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
  linarith only [hreal₁, hreal₃, hreal₅]
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ∃ n, p ∣ n ^ 2 + 1 ∧ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
⊢ p % 4 ≠ 3
Tactic:
linarith [show p % 4 = 1 from hp_mod_4_eq_1]
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ p ∣ n ^ 2 + 1
Tactic:
refine Int.natCast_dvd_natCast.mp ?_
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ ↑(n ^ 2 + 1)

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ ↑(n ^ 2 + 1)
Tactic:
simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ m ^ 2 + 1

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑p ∣ m ^ 2 + 1
Tactic:
refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑(m ^ 2 + 1) = 0

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ ↑(m ^ 2 + 1) = 0
Tactic:
simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ y ^ 2 + 1 = 0

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ y ^ 2 + 1 = 0
Tactic:
rw [pow_two, ← hy]
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ -1 + 1 = 0

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
⊢ -1 + 1 = 0
Tactic:
exact add_left_neg 1
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
⊢ p ≥ 2 * n
Tactic:
omega
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
⊢ p ∣ k ^ 2 + 4
Tactic:
cases' hnat₁ with x hx
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ p ∣ k ^ 2 + 4

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ p ∣ k ^ 2 + 4
Tactic:
have : (p : ℤ) ∣ (k : ℤ) ^ 2 + 4 := by
  use (p : ℤ) - 4 * n + 4 * x
  have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
  have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
  linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
State after:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this✝ : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
this : ↑p ∣ ↑k ^ 2 + 4
⊢ p ∣ k ^ 2 + 4

State before:
case intro
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this✝ : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
this : ↑p ∣ ↑k ^ 2 + 4
⊢ p ∣ k ^ 2 + 4
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑p ∣ ↑k ^ 2 + 4
Tactic:
use (p : ℤ) - 4 * n + 4 * x
State after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)

State before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
have hcast₁ : (k : ℤ) = p - 2 * n := by assumption_mod_cast
State after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)

State before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
have hcast₂ : (n : ℤ) ^ 2 + 1 = p * x := by assumption_mod_cast
State after:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
hcast₂ : ↑n ^ 2 + 1 = ↑p * ↑x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)

State before:
case h
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
hcast₂ : ↑n ^ 2 + 1 = ↑p * ↑x
⊢ ↑k ^ 2 + 4 = ↑p * (↑p - 4 * ↑n + 4 * ↑x)
Tactic:
linear_combination ((k : ℤ) + p - 2 * n) * hcast₁ + 4 * hcast₂
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
⊢ ↑k = ↑p - 2 * ↑n
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
x : ℕ
hx : n ^ 2 + 1 = p * x
hcast₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑n ^ 2 + 1 = ↑p * ↑x
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
⊢ ↑k = ↑p - 2 * ↑n
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
⊢ ↑p > 20
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
⊢ ↑k ^ 2 + 4 ≥ ↑p
Tactic:
assumption_mod_cast
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ ↑k > 4
Tactic:
refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ 4 ^ 2 < ↑k ^ 2

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
⊢ 4 ^ 2 < ↑k ^ 2
Tactic:
linarith only [hreal₂, hreal₃]
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ ↑k > √(2 * ↑n)
Tactic:
refine lt_of_pow_lt_pow_left 2 k.cast_nonneg ?_
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ √(2 * ↑n) ^ 2 < ↑k ^ 2

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ √(2 * ↑n) ^ 2 < ↑k ^ 2
Tactic:
rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
State after:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ 2 * ↑n < ↑k ^ 2

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
⊢ 2 * ↑n < ↑k ^ 2
Tactic:
linarith only [hreal₁, hreal₃, hreal₅]
State after:
no goals

State before:
p : ℕ
hpp : p.Prime
hp_mod_4_eq_1 : p ≡ 1 [MOD 4]
hp_gt_20 : p > 20
this : Fact p.Prime
hp_mod_4_ne_3 : p % 4 ≠ 3
y : ZMod p
hy : -1 = y * y
m : ℤ := y.valMinAbs
n : ℕ := m.natAbs
hnat₁ : p ∣ n ^ 2 + 1
hnat₂ : n ≤ p / 2
hnat₃ : p ≥ 2 * n
k : ℕ := p - 2 * n
hnat₄ : k = p - 2 * n
hnat₅ : p ∣ k ^ 2 + 4
hnat₆ : k ^ 2 + 4 ≥ p
hreal₁ : ↑k = ↑p - 2 * ↑n
hreal₂ : ↑p > 20
hreal₃ : ↑k ^ 2 + 4 ≥ ↑p
hreal₅ : ↑k > 4
hreal₆ : ↑k > √(2 * ↑n)
⊢ ↑p > 2 * ↑n + √(2 * ↑n)
Tactic:
linarith only [hreal₆, hreal₁]
State after:
no goals