1. FormalConjectures
  2. Wikipedia
  3. RudinsConjecture
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Rudin's conjecture on squares in arithmetic progressions

References:

    Wikipedia

    [Ru60] Rudin, W., Trigonometric series with gaps, J. Math. Mech. 9 (1960), 203–227.

    González-Jiménez, E. and Xarles, X., On a conjecture of Rudin on squares in arithmetic progressions, LMS J. Comput. Math. 17 (2014), 58–76.

open Filter Asymptotics Real namespace RudinsConjecture

$Q(N; q, a)$ is the number of perfect squares among the first $N$ terms of the arithmetic progression ${q n + a : 0 \le n < N}$.

noncomputable abbrev Q (N q a : ℕ) : ℕ := {n : ℕ | n < N ∧ IsSquare (q * n + a)}.ncard

A pair $(q, a)$ describes a non-trivial arithmetic progression if $q, a \ge 1$, $\gcd(q, a) = 1$, and $(q, a) \neq (1, 1)$.

def IsNontrivial (q a : ℕ) : Prop := 1 ≤ q ∧ 1 ≤ a ∧ Nat.Coprime q a ∧ (q, a) ≠ (1, 1)

$Q(N) = \max Q(N; q, a)$, the largest number of perfect squares occurring among the first $N$ terms of any non-trivial arithmetic progression. The supremum is over a set of naturals that is bounded above by $N$ (each progression has only $N$ terms), so it is attained.

noncomputable def Qmax (N : ℕ) : ℕ := sSup {m : ℕ | ∃ q a : ℕ, IsNontrivial q a ∧ Q N q a = m}

Sanity check: the progression $24 n + 1$ is non-trivial.

@[category test, AMS 11] theorem isNontrivial_24_1 : IsNontrivial 24 1 := ⊢ IsNontrivial 24 1 refine ⟨⊢ 1 ≤ 24 All goals completed! 🐙, ⊢ 1 ≤ 1 All goals completed! 🐙, ⊢ Nat.Coprime 24 1 All goals completed! 🐙, ⊢ (24, 1) ≠ (1, 1) All goals completed! 🐙⟩

Sanity check: there are no squares among the first 0 terms of any progression.

@[category test, AMS 11] theorem Q_zero (q a : ℕ) : Q 0 q a = 0 := q:ℕa:ℕ⊢ Q 0 q a = 0 All goals completed! 🐙

Sanity check pinning Q to a concrete value: among the first 6 terms of 24 n + 1, namely 1, 25, 49, 73, 97, 121, exactly four are perfect squares (1, 25, 49, 121), so Q 6 24 1 = 4. This validates the definition of Q and matches the claim that 24 n + 1 is the extremal progression.

@[category test, AMS 11] theorem Q_six_twentyfour_one : Q 6 24 1 = 4 := ⊢ Q 6 24 1 = 4 ⊢ {n | n < 6 ∧ IsSquare (24 * n + 1)}.ncard = 4 have hset : {n : ℕ | n < 6 ∧ IsSquare (24 * n + 1)} = ({0, 1, 2, 5} : Set ℕ) := ⊢ Q 6 24 1 = 4 n:ℕ⊢ n ∈ {n | n < 6 ∧ IsSquare (24 * n + 1)} ↔ n ∈ {0, 1, 2, 5} n:ℕ⊢ n < 6 ∧ IsSquare (24 * n + 1) ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5 n:ℕ⊢ n < 6 ∧ IsSquare (24 * n + 1) → n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5n:ℕ⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5 → n < 6 ∧ IsSquare (24 * n + 1) n:ℕ⊢ n < 6 ∧ IsSquare (24 * n + 1) → n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5 n:ℕhn:n < 6hsq:IsSquare (24 * n + 1)⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5 n:ℕhn:0 < 6hsq:IsSquare (24 * 0 + 1)⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = 2 ∨ 0 = 5n:ℕhn:1 < 6hsq:IsSquare (24 * 1 + 1)⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 5n:ℕhn:2 < 6hsq:IsSquare (24 * 2 + 1)⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 5n:ℕhn:3 < 6hsq:IsSquare (24 * 3 + 1)⊢ 3 = 0 ∨ 3 = 1 ∨ 3 = 2 ∨ 3 = 5n:ℕhn:4 < 6hsq:IsSquare (24 * 4 + 1)⊢ 4 = 0 ∨ 4 = 1 ∨ 4 = 2 ∨ 4 = 5n:ℕhn:5 < 6hsq:IsSquare (24 * 5 + 1)⊢ 5 = 0 ∨ 5 = 1 ∨ 5 = 2 ∨ 5 = 5 n:ℕhn:0 < 6hsq:IsSquare (24 * 0 + 1)⊢ 0 = 0 ∨ 0 = 1 ∨ 0 = 2 ∨ 0 = 5 All goals completed! 🐙 n:ℕhn:1 < 6hsq:IsSquare (24 * 1 + 1)⊢ 1 = 0 ∨ 1 = 1 ∨ 1 = 2 ∨ 1 = 5 All goals completed! 🐙 n:ℕhn:2 < 6hsq:IsSquare (24 * 2 + 1)⊢ 2 = 0 ∨ 2 = 1 ∨ 2 = 2 ∨ 2 = 5 All goals completed! 🐙 n:ℕhn:3 < 6hsq:IsSquare (24 * 3 + 1)⊢ 3 = 0 ∨ 3 = 1 ∨ 3 = 2 ∨ 3 = 5 n:ℕhn:3 < 6hsq:IsSquare (24 * 3 + 1)⊢ False; n:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = r * r⊢ False have hb : r < 9 := ⊢ Q 6 24 1 = 4 All goals completed! 🐙 n:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 0 * 0hb:0 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 1 * 1hb:1 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 2 * 2hb:2 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 3 * 3hb:3 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 4 * 4hb:4 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 5 * 5hb:5 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 6 * 6hb:6 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 7 * 7hb:7 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 8 * 8hb:8 < 9⊢ False n:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 0 * 0hb:0 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 1 * 1hb:1 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 2 * 2hb:2 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 3 * 3hb:3 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 4 * 4hb:4 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 5 * 5hb:5 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 6 * 6hb:6 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 7 * 7hb:7 < 9⊢ Falsen:ℕhn:3 < 6r:ℕhr:24 * 3 + 1 = 8 * 8hb:8 < 9⊢ False All goals completed! 🐙 n:ℕhn:4 < 6hsq:IsSquare (24 * 4 + 1)⊢ 4 = 0 ∨ 4 = 1 ∨ 4 = 2 ∨ 4 = 5 n:ℕhn:4 < 6hsq:IsSquare (24 * 4 + 1)⊢ False; n:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = r * r⊢ False have hb : r < 10 := ⊢ Q 6 24 1 = 4 All goals completed! 🐙 n:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 0 * 0hb:0 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 1 * 1hb:1 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 2 * 2hb:2 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 3 * 3hb:3 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 4 * 4hb:4 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 5 * 5hb:5 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 6 * 6hb:6 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 7 * 7hb:7 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 8 * 8hb:8 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 9 * 9hb:9 < 10⊢ False n:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 0 * 0hb:0 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 1 * 1hb:1 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 2 * 2hb:2 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 3 * 3hb:3 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 4 * 4hb:4 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 5 * 5hb:5 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 6 * 6hb:6 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 7 * 7hb:7 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 8 * 8hb:8 < 10⊢ Falsen:ℕhn:4 < 6r:ℕhr:24 * 4 + 1 = 9 * 9hb:9 < 10⊢ False All goals completed! 🐙 n:ℕhn:5 < 6hsq:IsSquare (24 * 5 + 1)⊢ 5 = 0 ∨ 5 = 1 ∨ 5 = 2 ∨ 5 = 5 All goals completed! 🐙 n:ℕ⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 5 → n < 6 ∧ IsSquare (24 * n + 1) ⊢ 0 < 6 ∧ IsSquare (24 * 0 + 1)⊢ 1 < 6 ∧ IsSquare (24 * 1 + 1)⊢ 2 < 6 ∧ IsSquare (24 * 2 + 1)⊢ 5 < 6 ∧ IsSquare (24 * 5 + 1) ⊢ 0 < 6 ∧ IsSquare (24 * 0 + 1) exact ⟨⊢ 0 < 6 All goals completed! 🐙, 1, ⊢ 24 * 0 + 1 = 1 * 1 All goals completed! 🐙⟩ ⊢ 1 < 6 ∧ IsSquare (24 * 1 + 1) exact ⟨⊢ 1 < 6 All goals completed! 🐙, 5, ⊢ 24 * 1 + 1 = 5 * 5 All goals completed! 🐙⟩ ⊢ 2 < 6 ∧ IsSquare (24 * 2 + 1) exact ⟨⊢ 2 < 6 All goals completed! 🐙, 7, ⊢ 24 * 2 + 1 = 7 * 7 All goals completed! 🐙⟩ ⊢ 5 < 6 ∧ IsSquare (24 * 5 + 1) exact ⟨⊢ 5 < 6 All goals completed! 🐙, 11, ⊢ 24 * 5 + 1 = 11 * 11 All goals completed! 🐙⟩ hset:{n | n < 6 ∧ IsSquare (24 * n + 1)} = {0, 1, 2, 5} := Set.ext fun n => Eq.mpr (id (congrArg (Iff (n < 6 ∧ IsSquare (24 * n + 1))) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 0)) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 1)) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 2)) Q_six_twentyfour_one._simp_2)))))))) { mp := fun a => And.casesOn a fun hn hsq => if x : 3 ≤ n then if x : 4 ≤ n then if x : 5 ≤ n then Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_24 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hn (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))))) x)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => False.elim (Exists.casesOn hsq fun r hr => have hb := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 3)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 3)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 3).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 3).rawCast + 0)))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 24))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 4))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 24) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 4) (Eq.refl 96))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 24)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 96 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 96 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 96) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 97))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 97) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 97)) (Eq.refl (Int.negOfNat 97))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 3)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 97)) (Eq.refl (Int.negOfNat 100)))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 10) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10) (Eq.refl 100))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 10))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 10)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 100) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 10 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 100 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 100)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 100)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_gt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 10) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Eq.refl (Int.negOfNat 10))))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 10 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 10)) (Eq.refl (Int.ofNat 10))))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 10 + (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 10)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3)) (Eq.refl false))) (neg_eq_zero.mpr (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 (24 * 4 + 1) (r * r)) (congr (congrArg Eq (Eq.trans (Nat.cast_add (24 * 4) 1) (congr (congrArg HAdd.hAdd (Nat.cast_mul 24 4)) Nat.cast_one))) (Nat.cast_mul r r))) hr))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 10 r) a))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (mul_nonneg_of_nonpos_of_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℤ r)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 10 r) a))))))); if x : 5 ≤ r then if x : 7 ≤ r then if x : 8 ≤ r then if x : 9 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_23 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hb (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))))) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_22 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_21 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else if x_1 : 6 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_20 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_1)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_19 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else if x_1 : 2 ≤ r then if x_2 : 3 ≤ r then if x_3 : 4 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_18 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_3)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_17 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_3) x_2)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_16 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hr hb else if x : 1 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_15 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_14 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) (Nat.zero_le r))) hr hb)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => False.elim (Exists.casesOn hsq fun r hr => have hb := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 8))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 8)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 8)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 8)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 8).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 8).rawCast + 0)))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 24))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 24) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 3) (Eq.refl 72))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 24)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 72 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 72 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 72) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 73))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 73) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 73)) (Eq.refl (Int.negOfNat 73))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 8)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 73)) (Eq.refl (Int.negOfNat 81)))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9) (Eq.refl 81))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 9))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 9)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 81) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 9 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 81 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 81)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 81)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_gt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Eq.refl (Int.negOfNat 9))))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 9 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 9)) (Eq.refl (Int.ofNat 9))))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 9 + (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 9)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 8)) (Eq.refl false))) (neg_eq_zero.mpr (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 (24 * 3 + 1) (r * r)) (congr (congrArg Eq (Eq.trans (Nat.cast_add (24 * 3) 1) (congr (congrArg HAdd.hAdd (Nat.cast_mul 24 3)) Nat.cast_one))) (Nat.cast_mul r r))) hr))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 9 r) a))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (mul_nonneg_of_nonpos_of_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℤ r)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 9 r) a))))))); if x : 4 ≤ r then if x : 6 ≤ r then if x : 7 ≤ r then if x : 8 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_13 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hb (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))))) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_12 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_11 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else if x_1 : 5 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_10 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_1)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_9 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else if x_1 : 2 ≤ r then if x_2 : 3 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_8 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_2)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_7 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hr hb else if x : 1 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_6 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_5 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) (Nat.zero_le r))) hr hb)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hn hsq else if x_1 : 1 ≤ n then if x_2 : 2 ≤ n then Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_4 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_2)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_3 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_2 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) (Nat.zero_le n))) hn hsq, mpr := fun a => Or.casesOn a (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 1 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1)))⟩) fun h => Or.casesOn h (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 5 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 25)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Eq.refl 25)))⟩) fun h => Or.casesOn h (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 7 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 48)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 49)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7)) (Eq.refl 49)))⟩) fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 11 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Eq.refl 120)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 121)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 121)))⟩ }⊢ {0, 1, 2, 5}.ncard = 4 have hcoe : ({0, 1, 2, 5} : Set ℕ) = ↑({0, 1, 2, 5} : Finset ℕ) := ⊢ Q 6 24 1 = 4 All goals completed! 🐙 hset:{n | n < 6 ∧ IsSquare (24 * n + 1)} = {0, 1, 2, 5} := Set.ext fun n => Eq.mpr (id (congrArg (Iff (n < 6 ∧ IsSquare (24 * n + 1))) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 0)) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 1)) (Eq.trans Q_six_twentyfour_one._simp_1 (congrArg (Or (n = 2)) Q_six_twentyfour_one._simp_2)))))))) { mp := fun a => And.casesOn a fun hn hsq => if x : 3 ≤ n then if x : 4 ≤ n then if x : 5 ≤ n then Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_24 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hn (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6))))) x)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => False.elim (Exists.casesOn hsq fun r hr => have hb := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 3)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 3)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 3).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 3).rawCast + 0)))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 24))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 4))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 24) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 4) (Eq.refl 96))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 24)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 96 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 96 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 96) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 97))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 97) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 97)) (Eq.refl (Int.negOfNat 97))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 3)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 97)) (Eq.refl (Int.negOfNat 100)))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 10) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10) (Eq.refl 100))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 10))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 10)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 100) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 10 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 100 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 100)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 100)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_gt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 10) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Eq.refl (Int.negOfNat 10))))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 10 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 10).rawCast + (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 10)) (Eq.refl (Int.ofNat 10))))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 10 + (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 10)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 10)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3)) (Eq.refl false))) (neg_eq_zero.mpr (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 (24 * 4 + 1) (r * r)) (congr (congrArg Eq (Eq.trans (Nat.cast_add (24 * 4) 1) (congr (congrArg HAdd.hAdd (Nat.cast_mul 24 4)) Nat.cast_one))) (Nat.cast_mul r r))) hr))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 10 r) a))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 10)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (mul_nonneg_of_nonpos_of_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℤ r)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 10 r) a))))))); if x : 5 ≤ r then if x : 7 ≤ r then if x : 8 ≤ r then if x : 9 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_23 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hb (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))))) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_22 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_21 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else if x_1 : 6 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_20 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_1)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_19 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else if x_1 : 2 ≤ r then if x_2 : 3 ≤ r then if x_3 : 4 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_18 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_3)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_17 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_3) x_2)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_16 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hr hb else if x : 1 ≤ r then Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_15 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 4 + 1 = x * x → x < 10 → False) (fun hr hb => Q_six_twentyfour_one._proof_14 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) (Nat.zero_le r))) hr hb)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => False.elim (Exists.casesOn hsq fun r hr => have hb := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 8))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 8)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 8)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 8)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 8).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 8).rawCast + 0)))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 24))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 24) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 3) (Eq.refl 72))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 24)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 72 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 72 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 72) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 73))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (↑r ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 73) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 73)) (Eq.refl (Int.negOfNat 73))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 8)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 73)) (Eq.refl (Int.negOfNat 81)))) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9) (Eq.refl 81))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 9))))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 9)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 81) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 9 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 81 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 81)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 81)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_gt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9))) (Mathlib.Tactic.Ring.atom_pf ↑r) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 9) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Eq.refl (Int.negOfNat 9))))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pp_pf_overlap (↑r) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2))) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.mul_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 9 + (↑r ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑r ^ Nat.rawCast 1 * (Int.negOfNat 9).rawCast + (↑r ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 9)) (Eq.refl (Int.ofNat 9))))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑r) (Nat.rawCast 2) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_pf_zero_add (↑r ^ Nat.rawCast 1 * Nat.rawCast 9 + (↑r ^ Nat.rawCast 2 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 9)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 9)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑r) (Nat.rawCast 2) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 8)) (Eq.refl false))) (neg_eq_zero.mpr (sub_eq_zero_of_eq (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_eq._simp_1 (24 * 3 + 1) (r * r)) (congr (congrArg Eq (Eq.trans (Nat.cast_add (24 * 3) 1) (congr (congrArg HAdd.hAdd (Nat.cast_mul 24 3)) Nat.cast_one))) (Nat.cast_mul r r))) hr))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 9 r) a))) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 9)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (mul_nonneg_of_nonpos_of_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Mathlib.Tactic.Linarith.natCast_nonneg ℤ r)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (id (Eq.mp (Mathlib.Tactic.Zify.natCast_le._simp_1 9 r) a))))))); if x : 4 ≤ r then if x : 6 ≤ r then if x : 7 ≤ r then if x : 8 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_13 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right hb (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 9))))) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_12 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_11 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hr hb else if x_1 : 5 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_10 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_1)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_9 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else if x_1 : 2 ≤ r then if x_2 : 3 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_8 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_2)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_7 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hr hb else if x : 1 ≤ r then Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_6 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) x)) hr hb else Eq.ndrec (motive := fun x => 24 * 3 + 1 = x * x → x < 9 → False) (fun hr hb => Q_six_twentyfour_one._proof_5 hr) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) (Nat.zero_le r))) hr hb)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x)) hn hsq else if x_1 : 1 ≤ n then if x_2 : 2 ≤ n then Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_4 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x) x_2)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_3 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) x_1)) hn hsq else Eq.ndrec (motive := fun x => x < 6 → IsSquare (24 * x + 1) → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 5) (fun hn hsq => Decidable.byContradiction fun a => Q_six_twentyfour_one._proof_2 a) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_1) (Nat.zero_le n))) hn hsq, mpr := fun a => Or.casesOn a (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 1 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 0)) (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 1)))⟩) fun h => Or.casesOn h (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 5 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 25)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Eq.refl 25)))⟩) fun h => Or.casesOn h (fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 7 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 48)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 49)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 7)) (Eq.refl 49)))⟩) fun h => Eq.symm h ▸ ⟨Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 6)) (Eq.refl false), Exists.intro 11 (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 24)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5)) (Eq.refl 120)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl 121)) (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 11)) (Eq.refl 121)))⟩ }hcoe:{0, 1, 2, 5} = ↑{0, 1, 2, 5} := of_eq_true (Eq.trans (congrArg (Eq {0, 1, 2, 5}) (Eq.trans (Finset.coe_insert 0 {1, 2, 5}) (congrArg (insert 0) (Eq.trans (Finset.coe_insert 1 {2, 5}) (congrArg (insert 1) (Eq.trans (Finset.coe_insert 2 {5}) (congrArg (insert 2) (Finset.coe_singleton 5)))))))) (eq_self {0, 1, 2, 5}))⊢ {0, 1, 2, 5}.card = 4 All goals completed! 🐙

Rudin's conjecture. The maximal number of squares among the first $N$ terms of a non-trivial arithmetic progression grows at most like $\sqrt{N}$: $$Q(N) = O(\sqrt{N}).$$

@[category research open, AMS 11] theorem declaration uses 'sorry'rudins_conjecture : (fun N : ℕ => (Qmax N : ℝ)) =O[atTop] fun N : ℕ => Real.sqrt N := ⊢ (fun N => ↑(Qmax N)) =O[atTop] fun N => √↑N All goals completed! 🐙

A stronger form of Rudin's conjecture: for every $N \ge 6$, the arithmetic progression $24 n + 1$ attains the maximum $Q(N)$.

@[category research open, AMS 11] theorem declaration uses 'sorry'rudins_conjecture_strong (N : ℕ) (hN : 6 ≤ N) : Q N 24 1 = Qmax N := N:ℕhN:6 ≤ N⊢ Q N 24 1 = Qmax N All goals completed! 🐙

The strongest form of Rudin's conjecture also asserts uniqueness: for $N \ge 6$, any non-trivial arithmetic progression attaining the maximum $Q(N)$ has common difference $24$. (Its initial term is then forced by $\gcd(24, a) = 1$; the progression $24n + 1$ is the canonical representative.)

@[category research open, AMS 11] theorem declaration uses 'sorry'rudins_conjecture_unique (N : ℕ) (hN : 6 ≤ N) (q a : ℕ) (hqa : IsNontrivial q a) (hmax : Q N q a = Qmax N) : q = 24 := N:ℕhN:6 ≤ Nq:ℕa:ℕhqa:IsNontrivial q ahmax:Q N q a = Qmax N⊢ q = 24 All goals completed! 🐙 end RudinsConjecture