From 5e9f400cbaf8a6ed5dce49ac8680fd7b2972d23c Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 7 Feb 2024 02:55:41 -0600
Subject: [PATCH] new: Added some more basic examples

---
 LeanTalkSP24.lean         |  1 +
 LeanTalkSP24/basics2.lean | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 LeanTalkSP24/basics2.lean

diff --git a/LeanTalkSP24.lean b/LeanTalkSP24.lean
index 870a651..c7928f8 100644
--- a/LeanTalkSP24.lean
+++ b/LeanTalkSP24.lean
@@ -1,5 +1,6 @@
 -- This module serves as the root of the `«LeanTalkSP24»` library.
 -- Import modules here that should be built as part of the library.
 import «LeanTalkSP24».basics
+import «LeanTalkSP24».basics2
 import «LeanTalkSP24».infinitely_many_primes
 import «LeanTalkSP24».polynomial_over_field_dim_one
diff --git a/LeanTalkSP24/basics2.lean b/LeanTalkSP24/basics2.lean
new file mode 100644
index 0000000..307fa2f
--- /dev/null
+++ b/LeanTalkSP24/basics2.lean
@@ -0,0 +1,20 @@
+import Mathlib.Tactic
+
+open Finset
+
+theorem sum_first_n {n : ℕ} : 2 * (range (n + 1)).sum id = n * (n + 1) := by
+  induction' n with d hd
+  · simp
+  · rw [sum_range_succ, mul_add, hd, id.def, Nat.succ_eq_add_one]
+    linarith
+
+open Set
+variable {α : Type _}
+variable {s t u : Set α}
+
+example : s ∪ s ∩ t = s := by
+  ext x; constructor
+  rintro (xs | xsti)
+  · trivial
+  · exact And.left xsti
+  exact Or.inl