gistfile1.lean

import Mathlib.Data.PNat.Basic
import Mathlib.Data.Nat.Digits

theorem repunit_mod_4 : ∀ n : ℕ+,
    (Nat.ofDigits 10 (List.replicate ((2 * n) : ℕ) 1)) % 4 = 3 := by
  intros n
  induction' n with n Hn
  · reduce
    rfl
  · push_cast
    rw [two_mul, Nat.add_add_add_comm]
    simp only [List.replicate_succ, Nat.ofDigits_cons]
    ring_nf
    rw [Nat.add_mod, Nat.mul_mod]
    simp only [Nat.reduceMod, mul_zero, Nat.zero_mod, add_zero]

theorem square_mod_4 : ∀ n : ℕ,
    (n * n) % 4 = 0 ∨ (n * n) % 4 = 1 := by
  intros n
  by_cases H : Even n
  · obtain ⟨x, Hx⟩ := H
    rw [Hx]; ring_nf; left
    simp only [Nat.mul_mod_left]
  · rw [Nat.not_even_iff_odd] at H
    obtain ⟨x, Hx⟩ := H
    rw [Hx]; ring_nf
    simp only [Nat.add_mul_mod_self_right,
               Nat.reduceMod, Nat.zero_mod, add_zero]
    right; trivial

theorem crux_ma176 : ∀ n : ℕ+,
    ¬ IsSquare (Nat.ofDigits 10 (List.replicate (2 * n) 1)) := by
  intros n
  let x := (Nat.ofDigits 10 (List.replicate (2 * n) 1))
  have Hx : x % 4 = 3 := repunit_mod_4 n
  rw [IsSquare, Not]
  intros H
  obtain ⟨sq, Hsq⟩ := H
  have Hy : x % 4 = (sq * sq) % 4 := by
    rw [← Hsq]
  have Hz : (sq * sq) % 4 = 0 ∨ (sq * sq) % 4 = 1 := 
    square_mod_4 sq
  cases Hz
  · linarith
  · linarith