diff --git a/LeanCourse25/Assignments/Assignment1.lean b/LeanCourse25/Assignments/Assignment1.lean
index 1f42172..6d04f52 100644
--- a/LeanCourse25/Assignments/Assignment1.lean
+++ b/LeanCourse25/Assignments/Assignment1.lean
@@ -42,7 +42,7 @@ your proof is finished.
 -/
 
 example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by
-  sorry
+  ring
   done
 
 /- In the first example above, take a closer look at where Lean displays parentheses.
@@ -90,7 +90,8 @@ but it doesn't use the assumptions `h` and `h'`
 -/
 
 example (a b c d : ℝ) (h : b = d + d) (h' : a = b + c) : a + b = c + 4 * d := by
-  sorry
+  rw [h', h]
+  ring
   done
 
 /- ## Rewriting with a lemma
@@ -128,7 +129,8 @@ right-hand side.
 -/
 
 example (a b c : ℝ) : exp (a + b - c) = (exp a * exp b) / (exp c * exp 0) := by
-  sorry
+  rw[exp_sub, exp_add, exp_zero]
+  ring
   done
 
 
@@ -139,7 +141,7 @@ The two lemmas below express the associativity and commutativity of multiplicati
 #check (mul_comm : ∀ a b : ℝ, a * b = b * a)
 
 example (a b c : ℝ) : a * b * c = b * (a * c) := by
-  sorry
+  rw [mul_comm  a b, mul_assoc b a c]
   done
 
 
@@ -163,13 +165,17 @@ variable {G : Type*} [Group G] (g h : G)
 #check inv_inv g
 
 lemma inverse_of_a_commutator : ⁅g, h⁆⁻¹ = ⁅h, g⁆ := by
-  sorry
+  rw [commutatorElement_def g h, commutatorElement_def h g]
+  rw [mul_inv_rev (g*h*g⁻¹) (h⁻¹),mul_inv_rev (g*h) g⁻¹, mul_inv_rev g h]
+  rw [inv_inv g,inv_inv h]
+  rw [mul_assoc,mul_assoc]
   done
 
-end
 
-/-
-## Rewriting from right to left
+
+
+
+/-## Rewriting from right to left
 
 Since equality is a symmetric relation, we can also replace the right-hand side of an
 equality by the left-hand side using `←` as in the following example.
@@ -189,11 +195,11 @@ In the case of ←, you can type it by typing "\l ", so backslash-l-space.
 -/
 
 example (a b c d : ℝ) (h : a = b + b) (h' : b = c) (h'' : a = d) : b + c = d := by
-  sorry
+  rw [← h'', h , h']
   done
 
 example (a b c d : ℝ) (h : a*d - 1 = c) (h' : a*d = b) : c = b - 1 := by
-  sorry
+  rw [← h', h]
   done
 
 /- ## Rewriting in a local assumption
@@ -235,11 +241,11 @@ Let's do some exercises using `calc`. Feel free to use `ring` in some steps.
 
 example (a b c : ℝ) (h : a = b + c) : exp (2 * a) = (exp b) ^ 2 * (exp c) ^ 2 := by
   calc
-    exp (2 * a) = exp (2 * (b + c))                 := by sorry
-              _ = exp ((b + b) + (c + c))           := by sorry
-              _ = exp (b + b) * exp (c + c)         := by sorry
-              _ = (exp b * exp b) * (exp c * exp c) := by sorry
-              _ = (exp b) ^ 2 * (exp c)^2           := by sorry
+    exp (2 * a) = exp (2 * (b + c))                 := by rw [h]
+              _ = exp ((b + b) + (c + c))           := by ring_nf
+              _ = exp (b + b) * exp (c + c)         := by rw[exp_add (b + b) (c+c)]
+              _ = (exp b * exp b) * (exp c * exp c) := by rw[exp_add b b, exp_add c c]
+              _ = (exp b) ^ 2 * (exp c)^2           := by ring
 
 /-
 From a practical point of view, when writing such a proof, it is sometimes convenient to:
@@ -254,29 +260,41 @@ Aligning the equal signs and `:=` signs is not necessary but looks tidy.
 
 /- Prove the following using a `calc` block. -/
 example (a b c d : ℝ) (h : c = a * d + b) (h' : b = a*d) : c = 2*d*a := by
-  sorry
-  done
+  calc
+    c = a*d + b := by rw [h]
+    _ = a*d + a*d := by rw [h']
+    _ = 2*d*a  := by ring
+
 
 
 
 /- Prove the following using a `calc` block. -/
 
 example (a b c d : ℝ) : a + b + c + d = d + (b + a) + c := by
-  sorry
-  done
+  calc
+    a + b + c + d = (a + b) + c + d := by rw[add_assoc (a+b) c d]
+                _ = d + (a + b + c) := by rw[add_comm (a + b + c) d]
+                _ = d + (b + a + c) := by rw[add_comm a b]
+                _ = d + (b + a) + c := by ring
+
+
+
 
 /- Prove the following using a `calc` block. -/
 
 #check sub_self
 
 example (a b c d : ℝ) (h : c + a = b*a - d) (h' : d = a * b) : a + c = 0 := by
-  sorry
-  done
-
+  calc
+    a + c = c + a             := by rw [add_comm a c]
+    _     = b * a - d         := by rw [h]
+    _     = b * a - a * b     := by rw [h']
+    _     = 0                 := by ring
 
 /- A ring is a collection of objects `R` with operations `+`, `*`,
 constants `0` and `1` and negation `-` satisfying the following axioms. -/
 section
+
 variable (R : Type*) [Ring R]
 
 #check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
@@ -293,10 +311,14 @@ variable (R : Type*) [Ring R]
 /- Use `calc` to prove the following from the axioms of rings, without using `ring`. -/
 
 example {a b c : R} (h : a + b = a + c) : b = c := by
-  sorry
-  done
-
-end
+  calc
+     b = 0 + b := by rw[zero_add]
+     _ = -a + a + b :=by rw[← neg_add_cancel]
+     _ = -a + (a + b) := by rw[add_assoc]
+     _ = -a + (a + c) := by rw[h]
+     _ = (-a + a) + c := by rw[← add_assoc ]
+     _ = 0 + c := by rw[neg_add_cancel]
+     _ =  c := by rw[zero_add]
 
 
 /- Prove the following equalities using `ring` (recall that `ring` doesn't use local hypotheses). -/
@@ -330,15 +352,21 @@ variable (a b c x : ℝ)
 #check (zero_add a      : 0 + a = a)
 
 example : (a + b) * (a - b) = a^2 - b^2 := by
-  sorry
+  rw[mul_sub (a + b) a b]
+  rw [add_mul a b a, add_mul a b b]
+  rw [mul_comm a b]
+  rw [← sub_sub (a*a + b*a) (b*a) (b*b)]
+  rw [← add_sub (a*a) (b*a) (b*a)]
+  rw [sub_self (b*a)]
+  rw [add_zero (a*a)]
+  rw [pow_two a, pow_two b]
   done
 
 
 -- Now redo it with `ring`.
 
 example : (a + b) * (a - b) = a^2 - b^2 := by
-  sorry
+  ring
   done
 
 end
-
diff --git a/LeanCourse25/Assignments/Assignment2.lean b/LeanCourse25/Assignments/Assignment2.lean
index 3017b8b..0dfc230 100644
--- a/LeanCourse25/Assignments/Assignment2.lean
+++ b/LeanCourse25/Assignments/Assignment2.lean
@@ -13,7 +13,10 @@ open Real Function Set Nat
 /-! # Exercises to practice. -/
 
 example (p q r s : Prop) (h : p ∧ q → r) (hp : p) (h' : q → s) : q → r ∧ s := by
-  sorry
+  intro hq
+  constructor
+  · apply h ⟨hp, hq⟩
+  · apply h' hq
   done
 
 example {α : Type*} {p q : α → Prop} (h : ∀ x, p x → q x) :
diff --git a/LeanCourse25/Assignments/Assignment2Fixed.lean b/LeanCourse25/Assignments/Assignment2Fixed.lean
index 619776c..dd3ca64 100644
--- a/LeanCourse25/Assignments/Assignment2Fixed.lean
+++ b/LeanCourse25/Assignments/Assignment2Fixed.lean
@@ -1,6 +1,7 @@
 import Mathlib.Analysis.Complex.Exponential
 import Mathlib.FieldTheory.Finite.Basic
-
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Algebra.Order.Group.Abs
 open Real Function Set Nat
 
 /-
@@ -15,45 +16,83 @@ open Real Function Set Nat
 /-! # Exercises to practice. -/
 
 example (p q r s : Prop) (h : p ∧ q → r) (hp : p) (h' : q → s) : q → r ∧ s := by
-  sorry
+  intro hq
+  constructor
+  · exact h ⟨hp, hq⟩
+  · exact h' hq
   done
 
 example {α : Type*} {p q : α → Prop} (h : ∀ x, p x → q x) :
     (∃ x, p x) → (∃ x, q x) := by
-  sorry
+  intro hx
+  obtain ⟨x, hpx⟩ := hx
+  use x
+  apply h x hpx
   done
 
 -- Exercise: prove this by contraposition.
 example : 2 ≠ 4 → 1 ≠ 2 := by
-  sorry
-  done
+  contrapose!
+  simp!
 
 /- Prove the following with basic tactics,
 in particular without using `tauto`, `grind` or lemmas from Mathlib. -/
 example {α : Type*} {p : α → Prop} {r : Prop} :
     ((∃ x, p x) → r) ↔ (∀ x, p x → r) := by
-  sorry
+  constructor
+  · intro h x hx
+    apply h ⟨x, hx⟩
+  · intro h hx
+    obtain ⟨x, hx'⟩:= hx
+    apply h x hx'
   done
 
 /- Prove the following with basic tactics,
 in particular without using `tauto`, `grind` or lemmas from Mathlib. -/
 example {α : Type*} {p : α → Prop} {r : Prop} :
     (∃ x, p x ∧ r) ↔ ((∃ x, p x) ∧ r) := by
-  sorry
+  constructor
+  · intro h
+    obtain ⟨x, hx, hr⟩ := h
+    exact ⟨ ⟨x, hx⟩, hr⟩
+  · intro h'
+    obtain ⟨ hx, hr⟩ := h'
+    obtain ⟨x, hp ⟩ := hx
+    exact ⟨x, hp, hr⟩
   done
 
 /- Prove the following without using `push_neg` or lemmas from Mathlib.
 You will need to use `by_contra` in the proof. -/
 example {α : Type*} (p : α → Prop) : (∃ x, p x) ↔ (¬ ∀ x, ¬ p x) := by
-  sorry
-  done
+  constructor
+  · intro hx
+    obtain ⟨x,hp⟩ := hx  -- hx : ∃ x, p x  → pick witness x with hp : p x
+    intro hx'  -- hx' : ∀ x, ¬ p x
+    specialize hx' x  -- specialize to this witness
+    contradiction
+
+  · intro h
+    by_contra hpx -- ¬ ∃ x, p x
+     -- From ¬∃x, p x, build ∀x, ¬p x
+    have hpx': ∀x, ¬p x := by
+      intro x hx
+      exact hpx ⟨x, hx⟩
+    exact h hpx'   -- contradicts h : ¬ ∀ x, ¬ p x
+
+
 
 def SequentialLimit (u : ℕ → ℝ) (l : ℝ) : Prop :=
   ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε
 
+set_option linter.unusedVariables false
+
 example (a : ℝ) : SequentialLimit (fun n : ℕ ↦ a) a := by
-  sorry
-  done
+  unfold SequentialLimit
+  intro ε hε
+  use 0
+  intro n hn
+  simp
+  linarith
 
 /-
 `(n)!` denotes the factorial function on the natural numbers.
@@ -61,14 +100,27 @@ The parentheses are mandatory when writing.
 Use `calc` to prove this.
 You can use `exact?` to find lemmas from the library,
 such as the fact that factorial is monotone. -/
-example (n m k : ℕ) (h : n ≤ m) : (n)! ∣ (m + 1)! := by
-  sorry
-  done
+example (n m  : ℕ) (h : n ≤ m) : (n)! ∣ (m + 1)! := by
+calc
+  (n)! ∣ (m)! := by solve_by_elim [Nat.factorial_dvd_factorial]
+  _ ∣ (m+1)! := by
+       -- first, produce `m! ∣ (m+1)!`
+      have hm : (m)!∣ (m+1)! :=by
+        -- (m+1)! = (m+1) * m!
+        simp [Nat.factorial_succ, Nat.mul_comm]
+      -- now `solve_by_elim` can use `hm`
+      solve_by_elim
 
 example (a b c x y : ℝ) (h : a ≤ b) (h2 : b < c) (h3 : x ≤ y) :
     a + exp x ≤ c + exp (y + 2) := by
-  sorry
-  done
+calc
+  a + exp x ≤ b + exp x := by gcongr        -- use a ≤ b
+  _         ≤ c + exp x := by gcongr        -- use b < c
+  _         ≤ c + exp y := by gcongr        -- use x ≤ y
+  _         ≤ c + exp (y+2):= by
+    have hy: y ≤ y+2 := by linarith
+    gcongr  -- y ≤ y+2 ⇒ exp y ≤ exp (y+2)
+
 
 -- Use `rw?` or `rw??` to help you in the following calculation.
 -- Alternatively, write out a calc block by hand.
@@ -79,7 +131,11 @@ example {G : Type*} [Group G] {a b c d : G}
 /-- Prove the following using `linarith`.
 Note that `linarith` cannot deal with implication or if and only if statements. -/
 example (a b c : ℝ) : a + b ≤ c ↔ a ≤ c - b := by
-  sorry
+  constructor
+  intro h1
+  linarith
+  intro h2
+  linarith
   done
 
 
@@ -112,14 +168,18 @@ example {a₁ a₂ b₁ b₂ c₁ c₂ : ℝ} (hab : a₁ + a₂ = b₁ + b₂)
 
 
 example {m n : ℤ} : n - m ^ 2 ≤ n + 3 := by
-  sorry
-  done
-
-example {a : ℝ} (h : ∀ b : ℝ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ 1 := by
-  sorry
-  done
+have  h: 0 ≤  m ^ 2:= by exact sq_nonneg m
+calc
+  n - m ^ 2 ≤ n + 0 := by linarith
+  _        ≤ n + 3 := by linarith
 
 
+example {a : ℝ} (h : ∀ b : ℝ, a ≥ -3 + 4 * b - b ^ 2) : a ≥ 1 := by
+  -- Work pointwise in an arbitrary b, then conclude.
+  have h2:= h 2
+  calc
+   a ≥ -3 + 4 * 2 - 2 ^ 2 := by exact h2
+   _ ≥ 1 := by linarith
 
 /-! # Exercises to hand-in. -/
 
@@ -136,8 +196,8 @@ def Continuous' (f : ℝ → ℝ) := ∀ x, ContinuousAtPoint f x
 -- Exercise for you. Remember that you can use `unfold` to expand a definition.
 example (f g : ℝ → ℝ) (hfg : ∀ x, ContinuousAtPoint f x ↔ ContinuousAtPoint g x) :
     Continuous' f ↔ Continuous' g := by
-  sorry
-  done
+  unfold Continuous'
+  simp[hfg]
 
 def All (p : ℝ → Prop) := ∀ x, p x
 
@@ -152,13 +212,51 @@ example (p q : ℝ → Prop) (h : ∀ x, p x ↔ q x) :
 
 -- Is the following true? If yes, prove it in Lean.
 -- If not, give a counterexample and prove it. (What do you have to do to do so?)
-example (p q : ℕ → Prop) (h: (∃ x, p x) ↔ (∃ x, q x)) : ∀ x, p x ↔ q x := by
-  sorry
+-- The schema is false in general:
+
+
+
+example:
+  ¬ (∀( p q : ℕ → Prop),
+      ((∃ x, p x) ↔ (∃ x, q x)) → ∀ x, p x ↔ q x) := by
+  intro H
+ -- Counterexample
+  let p : ℕ → Prop := fun x => x ≠ 0
+  let q : ℕ → Prop := fun _ => True
+ -- It satisfies the condition (∃ x, p x) ↔ (∃ x, q x)
+  have h: (∃ x, p x) ↔ (∃ x, q x) := by
+    constructor
+    ·intro ⟨x, hpx⟩ -- p: (∃ x, x ≠ 0)
+     use x
+    ·intro hx'   --  q: (∀ x, True)
+     exact ⟨1, Nat.one_ne_zero⟩  -- 1 ≠ 0
+ -- Assume the condition
+  have h' := H p q h -- Assume ∀ (x : ℕ), p x ↔ q x
+  have h'0 : p 0 ↔ q 0 := h' 0
+  have q0 : q 0 := trivial --  q: (∀ x, True) is trival for x = 0
+  rw [← h'0] at q0   --  q 0 implies p 0, i.e. we get 0 ≠ 0
+  exact q0 rfl       -- 0 ≠ 0 contradicts reflexivity
 
 /- Prove the following with basic tactics, without using `tauto` or lemmas from Mathlib. -/
 lemma exists_distributes_over_or {α : Type*} {p q : α → Prop} :
     (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) := by
-  sorry
+  constructor
+  · intro h -- Assume (∃ x, p x ∨ q x)
+    obtain ⟨x, hx⟩ := h -- x and hx: p x ∨ q x
+    obtain hp | hq := hx
+    · left
+      exact ⟨x, hp⟩ -- Cases of (∃ x, p x): px
+    · right
+      exact ⟨x, hq⟩ -- Cases of (∃ x, q x): qx
+  · intro h' -- Assume (∃ x, p x) ∨ (∃ x, q x)
+    obtain hp' | hq'  := h'  -- Cases hp': (∃ x, p x) and hq': (∃ x, q x)
+    · obtain ⟨x, hp⟩ := hp'   -- from ∃ x, p x, build ∃ x, p x ∨ q x
+      use x
+      left; exact hp
+    · obtain ⟨x, hq⟩ := hq'  -- from ∃ x, q x, build ∃ x, p x ∨ q x
+      use x
+      right; exact hq
+
   done
 
 end Logic
@@ -177,7 +275,7 @@ section Functions
 -- Use `exact?`, `apply?` or `rw??` to find this theorem in mathlib.
 -- Describe what you are doing.
 example (p : ℕ) [hp: Fact (Nat.Prime p)] (x : ZMod p) : x ^ p = x := by
-  sorry
+  exact ZMod.pow_card x -- A variation on Fermat's little theorem is euqivalent to this argument
   done
 
 -- The above theorem has a name. What is it?
@@ -186,46 +284,176 @@ example (p : ℕ) [hp: Fact (Nat.Prime p)] (x : ZMod p) : x ^ p = x := by
 
 -- Use `rw??` to find the following theorem in mathlib.
 example (p : ℕ) [hp: Fact (Nat.Prime p)] (k : ZMod p) (hk : k ≠ 0) : k ^ (p - 1) = 1 := by
-  sorry
+  rw [ZMod.pow_card_sub_one_eq_one hk]  -- Rewriting by a variation on Fermat's little theorem
   done
 
 -- Prove the following.
 example (p : ℕ) [Fact (Nat.Prime p)] :
     (fun k ↦ k ^ p + 2 * k ^ (2 * (p - 1) + 1) : ZMod p → ZMod p) = (fun k ↦ 3 * k) := by
-  sorry
-  done
+  ext k
+  -- Fermat's little theorem: k^p = k in ZMod p
+  have h1 : k ^ p = k := ZMod.pow_card k
+  by_cases hk : k = 0
+  · subst hk
+    -- both sides are 0
+    simp [h1]
+  · -- k ≠ 0 : use the “p−1” lemma on units and come back to ZMod
+    have hphi : k ^ (p - 1) = (1 : ZMod p) := by
+      -- move back from units and rewrite the exponent
+      rw [ZMod.pow_card_sub_one_eq_one hk]
+    have h2 : k ^ (2 * (p - 1) + 1) = k := by
+      calc
+        k ^ (2 * (p - 1) + 1)
+            = k ^ (2 * (p - 1)) * k := by
+                -- (n+1)-th power
+                ring
+        _   = (k ^ (p - 1)) ^ 2 * k := by
+                -- 2*(p-1) = (p-1)*2 and pow_mul
+                ring
+        _   = (1 : ZMod p) ^ 2 * k := by simp [hphi] -- k ^ (p - 1) = (1 : ZMod p)
+        _   = k := by simp
+    calc
+      k ^ p + 2 * k ^ (2 * (p - 1) + 1)
+          = k + 2 * k ^ (2 * (p - 1) + 1) := by simp[h1] -- k ^ p = k
+      _ = k + 2 * k := by simp[h2] --k ^ (2 * (p - 1) + 1) = k
+      _ = 3 * k := by ring
 
 -- Prove the following.
 example (p : ℕ) [Fact (Nat.Prime p)] (k : ZMod p) : k ^ (3 * (p - 1) + 1) = k := by
-  sorry
+  by_cases hk : k = 0
+  · subst hk
+    -- both sides are 0
+    simp
+  · -- k ≠ 0 : use the “p−1” lemma on units and come back to ZMod
+    have hphi : k ^ (p - 1) = (1 : ZMod p) := by
+      -- move back from units and rewrite the exponent
+      rw [ZMod.pow_card_sub_one_eq_one hk]
+    calc
+      k ^ (3 * (p - 1) + 1)
+              = k ^ (3 * (p - 1)) * k := by
+                -- (n+1)-th power
+                ring_nf
+        _   = (k ^ (p - 1)) ^ 3 * k := by
+                -- 3*(p-1) = (p-1)*3 and pow_mul
+                ring
+        _   = (1 : ZMod p) ^ 3 * k := by simp [hphi] -- k ^ (p - 1) = (1 : ZMod p)
+        _   = k := by simp
   done
 
 example (p : ℕ) [Fact (Nat.Prime p)] (k : ZMod p) : k ^ (5 * (p - 1) + 1) = k := by
-  sorry
+  by_cases hk : k = 0
+  · subst hk
+    -- both sides are 0
+    simp
+  · -- k ≠ 0 : use the “p−1” lemma on units and come back to ZMod
+    have hphi : k ^ (p - 1) = (1 : ZMod p) := by
+      -- move back from units and rewrite the exponent
+      rw [ZMod.pow_card_sub_one_eq_one hk]
+    calc
+      k ^ (5 * (p - 1) + 1)
+              = k ^ (5 * (p - 1)) * k := by
+                -- (n+1)-th power
+                ring
+        _   = (k ^ (p - 1)) ^ 5 * k := by
+                -- 5*(p-1) = (p-1)*5 and pow_mul
+                ring
+        _   = (1 : ZMod p) ^ 5 * k := by simp [hphi] -- k ^ (p - 1) = (1 : ZMod p)
+        _   = k := by simp
   done
-
 end Functions
 
+#check (abs_add_le: ∀ a b : ℝ, |a + b| ≤ |a| + |b|)
 
 /- Prove that the sum of two converging sequences converges. -/
 lemma sequentialLimit_add {s t : ℕ → ℝ} {a b : ℝ}
       (hs : SequentialLimit s a) (ht : SequentialLimit t b) :
     SequentialLimit (fun n ↦ s n + t n) (a + b) := by
-  sorry
-  done
+    -- Unfold the definition and do an ε/2 argument.
+  unfold SequentialLimit at hs ht ⊢
+  intro ε hε
+  have hε2: 0 < ε / 2 := by linarith
+  -- get indices for ε/2 for each sequence
+  obtain ⟨ Ns, hNs ⟩ := hs (ε / 2) hε2
+  obtain ⟨ Nt, hNt ⟩ := ht (ε / 2) hε2
+  refine ⟨ max Ns Nt,?_ ⟩
+  intro n hn
+-- hn : max Ns Nt ≤ n
+  have ⟨hn1, hn2⟩ := (max_le_iff.mp hn)
+-- now hn1 : Ns ≤ n, hn2 : Nt ≤ n
+  have hslt : |s n - a| < ε / 2 := hNs n hn1
+  have htlt : |t n - b| < ε / 2 := hNt n hn2
+  -- apply the triangle inequality
+  calc
+    |(s n + t n) - (a + b)|
+      = |(s n - a) + (t n - b)| := by ring_nf
+    _ ≤ |s n - a| + |t n - b|   := by apply abs_add_le (s n - a) (t n - b)
+    _ < ε / 2 + ε / 2           := add_lt_add hslt htlt
+    _ = ε                       := by ring
 
 /- It may be useful to case split on whether `c = 0` is true. -/
 lemma sequentialLimit_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (hs : SequentialLimit s a) :
     SequentialLimit (fun n ↦ c * s n) (c * a) := by
-  sorry
+  by_cases hc : c = 0
+  · -- trivial constant case
+    subst hc
+    unfold SequentialLimit at hs ⊢
+    intro ε hε
+    exact ⟨0, by
+      intro n hn
+      -- |0 * s n - 0 * a| = 0 < ε
+      simpa [zero_mul] using hε⟩
+  · -- scale ε by |c|
+    have hc_pos : 0 < |c| := abs_pos.mpr hc
+    unfold SequentialLimit at hs ⊢
+    intro ε hε
+    have hε' : 0 < ε / |c| := by exact div_pos hε hc_pos
+    obtain ⟨N, hN⟩ := hs (ε / |c|) hε'
+    refine ⟨N, ?_⟩
+    intro n hn
+    have hsn : |s n - a| < ε / |c| := hN n hn
+    calc
+      |c * s n - c * a|
+          = |c * (s n - a)| := by ring_nf
+      _   = |c| * |s n - a| := by rw [@abs_mul]
+      _   < |c| * (ε / |c|) := by exact mul_lt_mul_of_pos_left hsn hc_pos
+      _   = ε := by
+        have h' : |c| ≠ 0 := abs_ne_zero.mpr hc
+        -- |c| * (ε / |c|) = ε
+        simpa [one_div, mul_comm, mul_left_comm, mul_assoc]
+          using (by
+            calc
+              |c| * (ε / |c|)
+                  = (|c| * ε) * (1 / |c|) := by ring
+              _ = ε * (|c| * (1 / |c|)) := by ring
+              _ = ε * 1 := by
+                   rw [mul_one_div_cancel h']
+              _ = ε := by simp)
   done
 
-/-- Prove this using a calculation. -/
-lemma exercise_square {m n k : ℤ} (h : m ^ 2 + n ≤ 2) : n + 1 ≤ 3 + k ^ 2 := by
-  sorry
-  done
 
 
+/-- Prove this using a calculation. -/
+lemma exercise_square {m n k : ℤ} (h : m ^ 2 + n ≤ 2) :
+    n + 1 ≤ 3 + k ^ 2 := by
+    -- From h, isolate n
+  have hn : n ≤ 2 - m ^ 2 := by
+    linarith
+  -- Squares are nonnegative over ℤ
+  have hsq : 0 ≤ m ^ 2 := by exact sq_nonneg (m : ℤ)
+  -- Hence 2 - m^2 ≤ 2, so n ≤ 2
+  have hn2 : n ≤ 2 := by
+    have : 2 - m ^ 2 ≤ 2 := by linarith [hsq]
+    apply le_trans hn this
+  -- Also k^2 ≥ 0, so 3 ≤ 3 + k^2
+  have hk0 : 0 ≤ k ^ 2 := by exact sq_nonneg (k : ℤ)
+  have h3 : 3 ≤ 3 + k ^ 2 := by
+    simpa using add_le_add_left hk0 3
+  -- Chain the inequalities
+  calc
+    n + 1 ≤ 2 + 1 := add_le_add_right hn2 1
+    _ = 3 := by norm_num
+    _ ≤ 3 + k ^ 2 := h3
+
 section Growth
 
 variable {s t : ℕ → ℕ} {k : ℕ}
@@ -243,21 +471,79 @@ def EventuallyGrowsFaster (s t : ℕ → ℕ) : Prop :=
 /- show that `n * s n` grows (eventually) faster than `s n`. -/
 lemma eventuallyGrowsFaster_mul_left :
     EventuallyGrowsFaster (fun n ↦ n * s n) s := by
-  sorry
-  done
+intro k
+use k
+intro n hn
+calc
+  k * s n ≤ n * s n := by gcongr
+
+
+
+
 
 /- Show that if `sᵢ` grows eventually faster than `tᵢ` then
 `s₁ + s₂` grows eventually faster than `t₁ + t₂`. -/
 lemma eventuallyGrowsFaster_add {s₁ s₂ t₁ t₂ : ℕ → ℕ}
     (h₁ : EventuallyGrowsFaster s₁ t₁) (h₂ : EventuallyGrowsFaster s₂ t₂) :
     EventuallyGrowsFaster (s₁ + s₂) (t₁ + t₂) := by
-  sorry
+  -- unfold the definition so we can see the quantifiers and inequalities
+  unfold EventuallyGrowsFaster at h₁ h₂ ⊢
+  -- fix an arbitrary multiplier k
+  intro k
+  -- from h₁, obtain a threshold N₁ such that for all n ≥ N₁, k * t₁ n ≤ s₁ n
+  obtain ⟨N₁,hN₁⟩ := h₁ k
+  -- from h₂, obtain a threshold N₂ such that for all n ≥ N₂, k * t₂ n ≤ s₂ n
+  obtain ⟨N₂,hN₂⟩ := h₂ k
+  -- propose a single threshold large enough for both conditions
+  refine ⟨ max N₁ N₂ ,?_ ⟩
+  -- now fix an arbitrary n ≥ max N₁ N₂
+  intro n hn
+  -- from n ≥ max N₁ N₂, deduce n ≥ N₁ and n ≥ N₂
+  have h1: k * t₁ n ≤ s₁ n := hN₁ n (le_of_max_le_left hn)
+  have h2: k * t₂ n ≤ s₂ n := hN₂ n (le_of_max_le_right hn)
+  -- turn the goal into a pointwise statement
+  change k * (t₁ n + t₂ n) ≤ s₁ n + s₂ n
+  -- now distribute and add the two bounds
+  calc
+    k * (t₁ n + t₂ n)
+        = k * t₁ n + k * t₂ n := by
+          simp [Nat.mul_add]
+    _ ≤ s₁ n + s₂ n           := Nat.add_le_add h1 h2
   done
 
+
+
 /- Find a positive function that grows faster than itself when shifted by one. -/
-lemma eventuallyGrowsFaster_shift : ∃ (s : ℕ → ℕ),
+/-!  Find a positive function that grows faster than itself when shifted by one. -/
+lemma eventuallyGrowsFaster_shift :
+  ∃ (s : ℕ → ℕ),
     EventuallyGrowsFaster (fun n ↦ s (n+1)) s ∧ ∀ n, s n ≠ 0 := by
-  sorry
-  done
+  -- choose the sequence: s n = (n+1)!
+  refine ⟨fun n => (n+1)!, ?fast, ?pos⟩
+
+  -- (1) show: (n ↦ (n+2)!) eventually dominates (n ↦ (n+1)!)
+  · -- unfold the definition in the goal shape
+    intro k
+    -- a simple threshold works: N = k
+    refine ⟨k, ?_⟩
+    intro n hn
+    -- goal is: k * (n+1)! ≤ (n+2)!
+    -- rewrite (n+2)! as (n+2) * (n+1)!
+    have fact_succ : (n+2)! = (n+2) * (n+1)! := by
+      simp [Nat.factorial_succ,
+             Nat.add_comm, Nat.add_left_comm]
+    -- from n ≥ k, get k ≤ n+2
+    have hk_le_n2 : k ≤ n + 2 := by
+      have h1 : n ≤ n + 1 := Nat.le_succ n
+      have h2 : n + 1 ≤ n + 2 := Nat.le_succ (n + 1)
+      exact Nat.le_trans hn (Nat.le_trans h1 h2)
+    -- multiply both sides by (n+1)! on the right
+    have : k * (n+1)! ≤ (n+2) * (n+1)! := Nat.mul_le_mul_right ((n+1)!) hk_le_n2
+    -- finish via the factorial rewrite
+    simpa [fact_succ]
+
+  -- (2) positivity: factorials are never zero in ℕ
+  · intro n
+    simpa using Nat.factorial_ne_zero (n+1)
 
 end Growth
diff --git a/LeanCourse25/Assignments/Assignment4.lean b/LeanCourse25/Assignments/Assignment4.lean
index af9bba8..18db239 100644
--- a/LeanCourse25/Assignments/Assignment4.lean
+++ b/LeanCourse25/Assignments/Assignment4.lean
@@ -35,17 +35,26 @@ instance : Add Point := ⟨add⟩
 
 -- Prove that addition of points is associative.
 lemma add_assoc {a b c : Point} : a + (b + c) = a + b + c := by
-  sorry
-  done
+  ext
+  · show a.x + (b.x + c.x) = (a.x + b.x) + c.x
+    exact Eq.symm (_root_.add_assoc a.x b.x c.x)
+  · show a.y + (b.y + c.y) = (a.y + b.y) + c.y
+    exact Eq.symm (_root_.add_assoc a.y b.y c.y)
+  · show a.z + (b.z + c.z) = (a.z + b.z) + c.z
+    exact Eq.symm (_root_.add_assoc a.z b.z c.z)
 
 -- Define scalar multiplication of a point by a real number
 -- in the way you know from Euclidean geometry.
-def smul (r : ℝ) (a : Point) : Point := sorry
+def smul (r : ℝ) (a : Point) : Point :=
+  { x:= r*a.x
+    y:= r*a.y
+    z:= r*a.z
+  }
 
 -- If you made the right definition, proving these lemmas should be easy.
-@[simp] lemma smul_x (r : ℝ) (a : Point) : (Point.smul r a).x = r * a.x := by sorry
-@[simp] lemma smul_y (r : ℝ) (a : Point) : (Point.smul r a).y = r * a.y := by sorry
-@[simp] lemma smul_z (r : ℝ) (a : Point) : (Point.smul r a).z = r * a.z := by sorry
+@[simp] lemma smul_x (r : ℝ) (a : Point) : (Point.smul r a).x = r * a.x := by rfl
+@[simp] lemma smul_y (r : ℝ) (a : Point) : (Point.smul r a).y = r * a.y := by rfl
+@[simp] lemma smul_z (r : ℝ) (a : Point) : (Point.smul r a).z = r * a.z := by rfl
 
 -- This registers the above operation as "scalar multiplication":
 -- you can now write • for scalar multiplication.
@@ -74,13 +83,46 @@ def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le :
   (a b : StandardTwoSimplex) : StandardTwoSimplex
 where
   coords := lambda • a.coords + (1 - lambda) • b.coords
-  x_nonneg := by sorry
-  y_nonneg := by sorry
-  z_nonneg := by sorry
-  sum_eq := by sorry
-
+  x_nonneg := by
+    have hx₁ : 0 ≤ lambda • a.coords.x  :=   mul_nonneg lambda_nonneg  a.x_nonneg
+    have h01 : 0 ≤ 1 - lambda := sub_nonneg.mpr lambda_le
+    have hx₂ : 0 ≤ (1 - lambda) • b.coords.x :=  mul_nonneg h01 b.x_nonneg
+    have hx := add_nonneg hx₁ hx₂
+    change 0 ≤ lambda * a.coords.x + (1 - lambda) * b.coords.x
+    exact hx
+
+
+  y_nonneg := by
+    have hy₁ : 0 ≤ lambda • a.coords.y  :=   mul_nonneg lambda_nonneg  a.y_nonneg
+    have h01 : 0 ≤ 1 - lambda := sub_nonneg.mpr lambda_le
+    have hy₂ : 0 ≤ (1 - lambda) • b.coords.y :=  mul_nonneg h01 b.y_nonneg
+    have hy := add_nonneg hy₁ hy₂
+    change 0 ≤ lambda * a.coords.y + (1 - lambda) * b.coords.y
+    exact hy
+
+  z_nonneg := by
+    have hz₁ : 0 ≤ lambda • a.coords.z  :=   mul_nonneg lambda_nonneg  a.z_nonneg
+    have h01 : 0 ≤ 1 - lambda := sub_nonneg.mpr lambda_le
+    have hz₂ : 0 ≤ (1 - lambda) • b.coords.z :=  mul_nonneg h01 b.z_nonneg
+    have hz := add_nonneg hz₁ hz₂
+    change 0 ≤ lambda * a.coords.z + (1 - lambda) * b.coords.z
+    exact hz
+
+  sum_eq := by
+    have ha := a.sum_eq
+    have hb := b.sum_eq
+    calc
+      (lambda • a.coords + (1 - lambda) • b.coords).x
+        + (lambda • a.coords + (1 - lambda) • b.coords).y
+        + (lambda • a.coords + (1 - lambda) • b.coords).z
+      = lambda • a.coords.x + (1 - lambda) • b.coords.x
+        + (lambda • a.coords.y + (1 - lambda) • b.coords.y)
+        + (lambda • a.coords.z + (1 - lambda) • b.coords.z) := by rfl
+    _ = lambda * (a.coords.x + a.coords.y + a.coords.z)
+          + (1 - lambda) * (b.coords.x + b.coords.y + b.coords.z) := by
+          simp [mul_add, add_assoc, add_comm, add_left_comm]
+    _ = 1 := by simp [ha, hb]
 end
-
 end StandardTwoSimplex
 
 
@@ -140,16 +182,38 @@ def op (a b : Point4) : Point4 where
 
 -- Prove that op is associative.
 lemma op_assoc {a b c : Point4} : op (op a b) c = op a (op b c) := by
-  sorry
-  done
+  ext <;>
+  simp [op, sub_eq_add_neg, mul_add, add_mul]
+  <;> ring
+
+
+
+
 
 -- Investigate whether op is commutative: prove one of the following.
-lemma op_comm : ∀ a b : Point4, op a b = op b a := by sorry
+lemma not_op_comm : ¬ ∀ a b : Point4, op a b = op b a := by
+  by_contra h
+  let i : Point4 := {x := 0, y := 1, z := 0, w := 0}
+  let j : Point4 := {x := 0, y := 0, z := 1, w := 0}
+  have h₁: (op i j).w = 1 := by simp [op, i, j]
+  have h₂: (op j i).w = -1 := by simp [op, i, j]
+  have hw : (op i j).w = (op j i).w := by
+    have := congrArg Point4.w (h i j)
+    assumption
+  rw [h₁, h₂] at hw   -- turns hw into 1 = -1
+  have ha : (1 : ℝ) = -1 := hw
+  have hb : (1 : ℝ) ≠ -1 := by norm_num
+  exact hb ha
+
+
+
 
 -- For the latter, you may the following helpful.
 example : ⟨0, 1, 2, 3⟩ ≠ (⟨0, 3, 2, 3⟩ : Point4) := by
-  sorry
-  done
+  intro h
+  have hy : (1 : ℝ) = 3 := congrArg Point4.y h
+  have hne : (1 : ℝ) ≠ 3 := by norm_num
+  exact hne hy
 
 example {x y : ℝ} (h : x ≠ y) : ⟨0, 1, x, 3⟩ ≠ (⟨0, 1, y, 3⟩ : Point4) := by
   sorry
@@ -169,8 +233,19 @@ lemma not_op_comm : ¬(∀ a b : Point4, op a b = op b a) := by
 def SpecialPoint := { p : Point4 // p.x ^2 + p.y ^2 + p.z ^ 2 + p.w ^ 2 = 1 }
 
 -- We define "the same" operation on special points: complete the proof.
-def op' (a b : SpecialPoint) : SpecialPoint :=
-  ⟨op a.val b.val, sorry⟩
+def op' (a b : SpecialPoint) : SpecialPoint := by
+  refine ⟨op a.val b.val, ?_⟩
+  have hmul :
+      (op a.val b.val).x^2 + (op a.val b.val).y^2
+    + (op a.val b.val).z^2 + (op a.val b.val).w^2
+      =
+      (a.val.x^2 + a.val.y^2 + a.val.z^2 + a.val.w^2) *
+      (b.val.x^2 + b.val.y^2 + b.val.z^2 + b.val.w^2) := by
+    simp [op] ; ring
+
+  rw [a.property, b.property] at hmul
+  simp[hmul]
+
 
 -- Prove that `SpecialPoint` with the operation `op'` is a group.
 -- (If commutativity holds, it's even an abelian group. You don't need to prove this.)
diff --git a/LeanCourse25/Assignments/Assignment5.lean b/LeanCourse25/Assignments/Assignment5.lean
index c8b4300..6cb0455 100644
--- a/LeanCourse25/Assignments/Assignment5.lean
+++ b/LeanCourse25/Assignments/Assignment5.lean
@@ -1,6 +1,10 @@
 import Mathlib.Analysis.Complex.Exponential
 
 import Mathlib
+import Mathlib.Analysis.Calculus.Deriv.Basic
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import Mathlib.FieldTheory.Finite.Basic
+import Mathlib.NumberTheory.LSeries.RiemannZeta
 open Real Function Set
 
 /-
@@ -111,11 +115,40 @@ The following exercise makes this precise: prove it.
 
 Remember that Lean has proof irrelevance: any two proofs of a given proposition are equal.
 -/
+
 example (choiceFunction : ∀ (α : Type) (p : α → Prop) (_h : ∃ x, p x), α)
-    (h : ∀ (α : Type) (p : α → Prop) (x : α) (hx : p x), choiceFunction α p ⟨x, hx⟩ = x) :
+    (h : ∀ (α : Type) (p : α → Prop) (x : α) (hx : p x),
+      choiceFunction α p ⟨x, hx⟩ = x) :
     False := by
-  sorry
-
+  -- Wir nehmen α = Bool und ein triviales Prädikat.
+  let p : Bool → Prop := fun _ => True
+  have ht : p true := trivial
+  have hf : p false := trivial
+
+  -- Nach der gegebenen "Rechenregel":
+  have ht_eq : choiceFunction Bool p ⟨true, ht⟩ = true :=
+    h Bool p true ht
+  have hf_eq : choiceFunction Bool p ⟨false, hf⟩ = false :=
+    h Bool p false hf
+
+  -- In Prop (also auch für ∃ b, p b) gilt Beweis-Irrelevanz:
+  have hexists_eq : (⟨true, ht⟩ : ∃ b, p b) = ⟨false, hf⟩ :=
+    Subsingleton.elim _ _
+
+  -- Also müssen auch die Werte der choiceFunction gleich sein:
+  have hchoice_eq :
+      choiceFunction Bool p ⟨true, ht⟩ =
+        choiceFunction Bool p ⟨false, hf⟩ :=
+    congrArg (choiceFunction Bool p) hexists_eq
+
+  -- Daraus folgt true = false, Widerspruch.
+  have : true = false := by
+    calc
+      true = choiceFunction Bool p ⟨true, ht⟩ := ht_eq.symm
+      _    = choiceFunction Bool p ⟨false, hf⟩ := hchoice_eq
+      _    = false := hf_eq
+
+  exact (Bool.eq_not_self true).mp this
 
 end choice
 
@@ -144,10 +177,132 @@ Hints:
 -/
 attribute [-simp] Finset.card_powerset
 #check Finset.induction
+#check insert
+
+
+example (α : Type*) [DecidableEq α] (s : Finset α) (a : α) : insert a s = {a} ∪ s := by rfl
 
-lemma finset_card_powerset (α : Type*) (s : Finset α) :
+
+lemma finset_card_powerset (α : Type*) [DecidableEq α] (s : Finset α) :
     Finset.card (Finset.powerset s) = 2 ^ Finset.card s := by
-  sorry
-  done
+  induction s using Finset.induction with
+  | empty => simp
+  | @insert a s ha ih =>
+      have hsplit:
+        Finset.powerset (insert a s)
+          =  Finset.powerset s ∪
+            (Finset.powerset s).image (fun t => insert a t ) := by
+        exact Finset.powerset_insert s a
+
+      have hdisj:
+        Disjoint (Finset.powerset s ) ((Finset.powerset s).image (fun t => insert a t )) := by
+
+          -- Use the characterization of disjointness for Finsets:
+          -- A and B are disjoint if for every element t,
+          -- t ∈ A → t ∈ B → False.
+        refine Finset.disjoint_left.mpr ?_
+
+        -- Introduce:
+        -- t  = a candidate subset
+        -- ht  : t ∈ powerset s
+        -- ht' : t ∈ image (insert a) (powerset s)
+        intro t ht ht'
+
+        -- From membership in the image, we obtain:
+        --  t = insert a u for some u ∈ powerset s.
+        rcases Finset.mem_image.mp ht' with ⟨u, hu, rfl⟩
+
+        -- From ht : t ∈ powerset s and t = insert a u,
+        -- we get the subset condition:
+        --   insert a u ⊆ s.
+        have hsubset : insert a u ⊆ s := Finset.mem_powerset.mp ht
+
+        -- But a is always contained in insert a u.
+        have ha_in : a ∈ insert a u :=  Finset.mem_insert_self a u
+
+        -- Therefore a ∈ s.
+        have this: a ∈ s := hsubset ha_in
+
+        -- But this contradicts the induction hypothesis ‘ha : a ∉ s’.
+        exact ha this
+
+      have hinj:
+          ∀ t u: Finset α,
+          t ∈ Finset.powerset s →
+          u ∈ Finset.powerset s →
+          insert a t = insert a u → t = u := by
+            intro t u ht hu h
+            refine Finset.ext_iff.mpr ?_
+
+            -- From t,u ∈ powerset s we know: t ⊆ s and u ⊆ s
+            have ht_ss : t ⊆ s := Finset.mem_powerset.mp ht
+            have hu_ss : u ⊆ s := Finset.mem_powerset.mp hu
+
+            -- Since a ∉ s, a ∉ t and a ∉ u
+            have ha_t : a ∉ t := fun h_mem => ha (ht_ss h_mem)
+            have ha_u : a ∉ u := fun h_mem => ha (hu_ss h_mem)
+
+            -- Remove a from both sides of insert a t = insert a u
+            -- Lean has: Finset.erase_insert ha_t : erase a (insert a t) = t
+            --           Finset.erase_insert ha_u : erase a (insert a u) = u
+            have h₁:= congrArg (Finset.erase · a) h
+          -- erase-insert identities
+            have h₂ : (insert a t).erase a = t :=
+              Finset.erase_insert ha_t
+            have h₃ : (insert a u).erase a = u :=
+              Finset.erase_insert ha_u
+
+            -- chain equalities to get t = u
+            have htu : t = u := by
+              calc
+                t = (insert a t).erase a := h₂.symm
+                _ = (insert a u).erase a := h₁
+                _ = u := h₃
+            simp[htu]
+
+
+      -- Now compute cardinalities:
+      -- |powerset (insert a s)| = |powerset s| + |image|
+      -- and |image| = |powerset s|
+ -- cardinality of the image: same as cardinality of powerset s
+      have hcard_image :
+        Finset.card ((Finset.powerset s).image (fun t => insert a t)) =
+          Finset.card (Finset.powerset s) := by
+        -- card_image_iff lets us use our injectivity lemma
+        apply Finset.card_image_iff.mpr
+        intro t u ht hu h
+        exact hinj t ht u hu h
+
+      -- cardinality of the union from the split decomposition
+      have hcard_union :
+        Finset.card (Finset.powerset (insert a s)) =
+          Finset.card (Finset.powerset s)
+          + Finset.card ((Finset.powerset s).image (fun t => insert a t)) := by
+        simp[hsplit]
+        exact Finset.card_union_of_disjoint hdisj
+
+      -- Now compute cardinalities:
+      -- |powerset (insert a s)| = |powerset s| + |image|
+      -- and |image| = |powerset s|
+      calc
+        Finset.card (Finset.powerset (insert a s))
+            = Finset.card (Finset.powerset s)
+              + Finset.card ((Finset.powerset s).image (fun t => insert a t)) := hcard_union
+        _   = Finset.card (Finset.powerset s)
+              + Finset.card (Finset.powerset s) := by
+                simp [hcard_image]
+        _   = 2 * Finset.card (Finset.powerset s) := by
+                simp [two_mul]
+        _   = 2 * 2 ^ Finset.card s := by
+                simp [ih]
+        _   = 2 ^ Finset.card s * 2 := by
+                ac_rfl
+        _   = 2 ^ (Finset.card s + 1) := by
+                simp [pow_succ, Nat.mul_comm]
+        _   = 2 ^ Finset.card (insert a s) := by
+                -- card (insert a s) = card s + 1 since a ∉ s
+                refine (Nat.pow_right_inj ?_).mpr ?_
+                linarith
+                exact Eq.symm (Finset.card_insert_of_notMem ha)
 
 end cardinality
diff --git a/LeanCourse25/Assignments/Assignment6.lean b/LeanCourse25/Assignments/Assignment6.lean
index 6b5d50c..11314b9 100644
--- a/LeanCourse25/Assignments/Assignment6.lean
+++ b/LeanCourse25/Assignments/Assignment6.lean
@@ -134,26 +134,61 @@ variable {G : AddSubgroup ℚ}
 
 -- In the proof we will consider the following subgroup, consisting of all `n`-fold multiples
 -- of rational numbers.
-def multiple (n : ℕ) : AddSubgroup ℚ := sorry
+
+
+def multiple (n : ℕ) : AddSubgroup ℚ :=
+{ carrier := {x : ℚ | ∃ r,  n * r = x},
+  zero_mem' := by
+    use 0
+    simp,
+  add_mem' := by
+    intro x y hx hy
+    rcases hx with ⟨r₁, hr₁⟩
+    rcases hy with ⟨r₂, hr₂⟩
+    use (r₁ + r₂)
+    simp [hr₁, hr₂, mul_add],
+  neg_mem' :=  by
+    intro x hx
+    rcases hx with ⟨r, hr⟩
+    use -r
+    simp [hr]}
+
+
 
 -- If your definition above is correct, this proof is true by rfl.
-lemma mem_multiple_iff (n : ℕ) (q : ℚ) : q ∈ multiple n ↔ ∃ r, n * r = q := sorry -- by rfl
+lemma mem_multiple_iff (n : ℕ) (q : ℚ) : q ∈ multiple n ↔ ∃ r, n * r = q := by rfl -- by rfl
 
 -- The next lemma is a general fact from group theory: use mathlib to find the right lemma.
 -- Hint: it's similar to `Subgroup.pow_index_mem`.
 
+#loogle "AddGroup.Quotient"
+
+#check AddSubgroup.nsmul_index_mem
+
+#check Subgroup.pow_index_mem
+
+
 lemma step1 {n : ℕ} (hG : G.index = n) (q : ℚ) : n • q ∈ G := by
-  sorry
+  have h : G.index • q ∈ G :=
+    AddSubgroup.nsmul_index_mem (H := G) (g := q)
+  rw [← hG]
+  exact h
 
 lemma step2 {n : ℕ} (hG : G.index = n) : multiple n ≤ G := by
-  sorry
+  subgroup....
+
+  rw[sorry]
 
 lemma step3 {n : ℕ} (hn : n ≠ 0) : multiple n = ⊤ := by
-  sorry
+
+
+  exact mem_multiple_iff
 
 -- The goal of this exercise: (ℚ, +) has no non-trivial subgroups of finite index.
 example (hG : G.index ≠ 0) : G = ⊤ := by
-  sorry
+  1 in G
+
+  exact hG
 
 end
 
@@ -179,8 +214,10 @@ lemma add_pow_eq_pow_add_pow (x y : R) : (x + y) ^ p = x ^ p + y ^ p := by
   have h6 : ∑ i ∈ Ioo 0 p, x ^ i * y ^ (p - i) * Nat.choose p i = 0 :=
     calc
      _ =  ∑ i ∈ Ioo 0 p, x ^ i * y ^ (p - i) * 0 := by
-       sorry
-     _ = 0 := by sorry
+       have ...
+
+       simp
+     _ = 0 := by ring
   sorry
   done
 
diff --git a/LeanCourse25/Assignments/LeanCourse_Exercises b/LeanCourse25/Assignments/LeanCourse_Exercises
new file mode 160000
index 0000000..0249ed9
--- /dev/null
+++ b/LeanCourse25/Assignments/LeanCourse_Exercises
@@ -0,0 +1 @@
+Subproject commit 0249ed929dc9e6c2fe67520ea61d2e55a0bc050a
diff --git a/LeanCourse25/Lectures/Lecture10.lean b/LeanCourse25/Lectures/Lecture10.lean
index b9dfacf..31ef931 100644
--- a/LeanCourse25/Lectures/Lecture10.lean
+++ b/LeanCourse25/Lectures/Lecture10.lean
@@ -219,6 +219,7 @@ whether a number is even or not.
 -- #synth Decidable RiemannHypothesis
 
 
+
 /-
 If you open the `Classical` namespace, then you can treat
 any finite set as a `Finset`.
@@ -337,11 +338,11 @@ example {α : Type*} [DecidableEq α] (f : α → ℕ)
     simp [ha]
     constructor
     · apply h
-      exact?
+      exact mem_insert_self a s
     · apply ih
       intros x hx
       apply h
-      exact?
+      simp [hx]
   done
 
 
diff --git a/LeanCourse25/Lectures/Lecture10Before.lean b/LeanCourse25/Lectures/Lecture10Before.lean
index 5a54493..b6d0cc3 100644
--- a/LeanCourse25/Lectures/Lecture10Before.lean
+++ b/LeanCourse25/Lectures/Lecture10Before.lean
@@ -55,9 +55,11 @@ we're opening the `Real` namespace just for the following command.
 
 open Real in
 #check π
+-- #check π
 
+open Real in
+#check Real.pi
 
--- #check π
 
 
 /- You can declare your own notation with the `notation` keyword. -/
@@ -147,7 +149,7 @@ compute what elements it contains.
 #eval ({j ∈ {1, 2, 3, 4} | Even j} : Finset ℕ)
 
 
--- #check ({j ∈ {1} | RiemannHypothesis } : Finset ℕ)
+--#check ({j ∈ {1} | RiemannHypothesis } : Finset ℕ)
 
 
 
@@ -258,9 +260,52 @@ the following induction principle.
 example {α : Type*} [DecidableEq α] (f : α → ℕ)
     (s : Finset α) (h : ∀ x ∈ s, f x ≠ 0) :
     ∏ x ∈ s, f x ≠ 0 := by
-  sorry
-  done
 
+  -- Induktion über s mit dem Eliminator Finset.induction_on
+  induction s using Finset.induction with
+  |   empty =>
+      -- Fall s = ∅
+      -- Ziel: ∏ x ∈ ∅, f x ≠ 0
+      simp
+  | @insert a s ha ih =>
+      -- Annahmen in diesem Fall:
+      -- a : α
+      -- s : Finset α
+      -- ha : a ∉ s
+      -- ih : (∀ x ∈ s, f x ≠ 0) → ∏ x ∈ s, f x ≠ 0
+      -- h : ∀ x ∈ insert a s, f x ≠ 0
+      -- Ziel: ∏ x ∈ insert a s, f x ≠ 0
+
+      -- 1) f a ≠ 0 aus h
+      have ha0 : f a ≠ 0 := h a (by simp)
+
+      -- 2) Hypothese nur auf s einschränken
+      have h' : ∀ x ∈ s, f x ≠ 0 := by
+        intro x hx
+        exact h x (by simp [hx])
+
+      -- 3) Induktionsvoraussetzung benutzen
+      have hs0 : ∏ x ∈ s, f x ≠ 0 := ih h'
+
+      -- 4) Produkt bleibt ≠ 0
+      have hprod : f a * ∏ x ∈ s, f x ≠ 0 :=
+        Nat.mul_ne_zero ha0 hs0
+      have h: f a ≠ 0 ∧ ∏ x ∈ s, f x ≠ 0 := by
+
+        constructor
+        · -- Ziel: f a ≠ 0
+            intro hfa        -- hfa : f a = 0
+            apply hprod      -- wir wollen zeigen: f a * ∏ x ∈ s, f x = 0
+            simp [hfa]       -- ergibt: 0 * ... = 0
+
+        · -- Ziel: ∏ x ∈ s, f x ≠ 0
+            intro hs         -- hs : ∏ x ∈ s, f x = 0
+            apply hprod
+            simp [hs]        -- f a * 0 = 0
+          -- Replace simpa with basic tactics:
+      simp [ha]
+      push_neg  -- goal becomes: f a * ∏ x ∈ s, f x ≠ 0
+      exact h
 
 
 
@@ -322,7 +367,9 @@ example {α β : Type*} (s : Finset α) (t : Finset β)
     (h_left : ∀ a ∈ s, 3 ≤ #{b ∈ t | r a b})
     (h_right : ∀ b ∈ t, #{a ∈ s | r a b} ≤ 1) :
     3 * #s ≤ #t := by
-  sorry
+  calc
+    3* #s   := by soerry
+
   done
 
 
diff --git a/LeanCourse25/Lectures/Lecture2.lean b/LeanCourse25/Lectures/Lecture2.lean
index a911b45..231e318 100644
--- a/LeanCourse25/Lectures/Lecture2.lean
+++ b/LeanCourse25/Lectures/Lecture2.lean
@@ -294,9 +294,18 @@ Also try it directly with `rw`.
 
 example (a b c : ℝ) (h : a = b - c) (h2 : b * b = 2 * c) :
     a * b = (2 - b) * c := by
-  sorry
-  done
+  calc
+      a * b = (b-c) * b := by rw [h]
+      _     = b*b -c*b  := by ring
+      _     = 2*c - c*b := by rw [h2]
+      _     = (2 - b) * c := by ring
 
+example (a b c : ℝ) (h : a = b - c) (h2 : b * b = 2 * c) :
+  a * b = (2 - b) * c := by
+  rw [h]        -- replace a with (b - c)
+  rw [sub_mul]  -- simplify: (b - c) * b → b*b - c*b
+  rw [h2]       -- replace b*b with 2*c
+  ring_nf       -- simplify: 2*c - c*b → (2 - b)*c
 
 
 /-
@@ -346,7 +355,7 @@ example (p q r : Prop) (hq : p → q) (hr : p → q → r) : p → r := by
 
 /- We can also use `specialize` to apply a hypothesis to arguments. -/
 example (p q : Prop) (a b c : ℝ) (hq : p → q) (hr : p → q → a = b) : p → a + c = b + c := by
-  intro hp
+  intro hp  
   specialize hq hp
   specialize hr hp hq
   rw [hr]
@@ -377,6 +386,10 @@ example (p q r s : Prop) (hq : p → s → q) (hr : q → r) : s → p → r :=
   · assumption
   done
 
+
+
+
+
 example (p q r s : Prop) (hq : (p → s) → q) (hr : q → r) : s → p → r := by
   intro hs hp
   apply hr
@@ -412,7 +425,11 @@ variable (f g : ℝ → ℝ)
 #check (continuous_sin : Continuous (fun x : ℝ ↦ sin x))
 
 example : Continuous (fun x ↦ x + x * Real.sin x) := by
-  sorry
+  apply Continuous.add       -- need both parts continuous
+  ·apply continuous_id        -- part 1: x ↦ x
+  apply Continuous.mul       -- part 2: x ↦ x * sin x
+  ··apply continuous_id        -- factor 1: x ↦ x
+  ··apply continuous_sin       -- factor 2: x ↦ sin x
   done
 
 
@@ -429,6 +446,7 @@ example : Continuous (fun x ↦ x + x * Real.sin x) := by
 -/
 
 
+
 #check exp_le_exp
 #check (exp_le_exp.1 : exp a ≤ exp b → a ≤ b)
 #check (exp_le_exp.2 : a ≤ b → exp a ≤ exp b)
@@ -437,20 +455,24 @@ example : Continuous (fun x ↦ x + x * Real.sin x) := by
 
 
 example (h : a ≤ b) : exp a ≤ exp b := by
-  sorry
+  apply exp_le_exp.2
+  exact h 
   done
 
 
 
 example (h : exp a ≤ exp b) : a ≤ b := by
-  sorry
+  apply exp_le_exp.1
+  assumption 
   done
 
 
 
 
 example {p q : Prop} (h1 : p → q) (h2 : q → p) : p ↔ q := by
-  sorry
+  constructor
+  · apply h1
+  · apply h2
   done
 
 
@@ -468,13 +490,15 @@ def Injective (f : ℝ → ℝ) : Prop := ∀ x y : ℝ, f x = f y → x = y
 
 example (f g : ℝ → ℝ) (hg : Injective g) (hf : Injective f) :
     Injective (g ∘ f) := by
-  sorry
+  intro x y h
+  specialize hg (f x) (f y) h
+  have h1 : f x = f y := hg
+  exact hf x y h1  
   done
 
 
 
 
-
 /- ## Conjunction
 
 In Lean the conjunction of two statements `P` and `Q` is denoted by `P ∧ Q`, read as "P and Q".
diff --git a/LeanCourse25/Lectures/Lecture3Before.lean b/LeanCourse25/Lectures/Lecture3Before.lean
index 44f3e20..36cdf55 100644
--- a/LeanCourse25/Lectures/Lecture3Before.lean
+++ b/LeanCourse25/Lectures/Lecture3Before.lean
@@ -208,7 +208,11 @@ example : a = a * b → a = 0 ∨ b = 1 := by
   intro h
   have hyp : a * (b - 1) = 0 := by linarith
   rw [mul_eq_zero] at hyp
-  sorry
+  obtain ha | hb := hyp
+  · left
+    exact ha
+  · right
+    linarith    
   done
 
 
@@ -218,7 +222,12 @@ example (f : ℝ → ℝ) (hf : StrictMono f) : Injective f := by
   intro x y hxy
   have h : x < y ∨ x = y ∨ x > y := by
     exact lt_trichotomy x y
-  sorry
+  obtain hlt | heq | hgt := h
+  · have : f x < f y := hf hlt
+    linarith  
+  · exact heq
+  · have : f y < f x := hf hgt
+    linarith  
   done
 
 /- ## Negation
@@ -229,12 +238,22 @@ We can use the same tactics as for implication:
 `intro` to prove a negation, and `apply` to use one. -/
 
 example {p : Prop} (h : p) : ¬ ¬ p := by
-  sorry
+  intro hp
+  apply hp 
+  exact h
   done
 
 example {α : Type*} {p : α → Prop} : ¬ (∃ x, p x) ↔ ∀ x, ¬ p x := by
-  sorry
-  done
+constructor
+· -- (→)  If no witness exists, then every point fails p
+    intro h x hx
+    apply h
+    exact ⟨x, hx⟩
+· -- (←)  If every point fails p, then no witness exists
+    intro h hex
+    obtain ⟨x, hx⟩ := hex
+    exact (h x) hx
+done
 
 /- We can use `exfalso` to use the fact that
 everything follows from `False`: ex falso quod libet -/
diff --git a/LeanCourse25/Lectures/Lecture4Before.lean b/LeanCourse25/Lectures/Lecture4Before.lean
index bae032f..04bb74d 100644
--- a/LeanCourse25/Lectures/Lecture4Before.lean
+++ b/LeanCourse25/Lectures/Lecture4Before.lean
@@ -82,16 +82,22 @@ using the following tactics.
 * `push_neg` to push negations inside quantifiers and connectives.
 -/
 example (p q : Prop) (h : ¬q → ¬p) : p → q := by
-  sorry
+  intro hp
+  by_contra hq
+  have:= h hq
+  apply h hq hp 
   done
 
 example (p r : Prop) (h1 : p → r) (h2 : ¬ p → r) : r := by
-  sorry
+  by_cases hp : p
+  · apply h1 hp
+  · apply h2 hp
   done
 
 example {α : Type*} {p : α → α → Prop} :
     ¬ (∃ x y, p x y) ↔ ∀ x y, ¬ p x y := by
-  sorry
+  push_neg
+  rfl
   done
 
 /-
@@ -104,13 +110,16 @@ we need to use `by_contra` to begin a proof by contradiction.
 
 /- The `contrapose` tactic starts a proof by contraposition -/
 example (p q : Prop) (h : ¬q → ¬p) : p → q := by
-  sorry
+  contrapose
+  assumption 
   done
 
 -- Exercise: prove this by contraposition.
 example : 2 ≠ 4 → 1 ≠ 2 := by
-  sorry
-  done
+  contrapose!
+  intro h 
+  linarith
+  done 
 
 -- Final remark: the `use` tactic is compatible with constructive logic.
 
@@ -122,14 +131,69 @@ def SequentialLimit (u : ℕ → ℝ) (l : ℝ) : Prop :=
 
 example (u : ℕ → ℝ) (l : ℝ) : ¬ SequentialLimit u l ↔
     ∃ ε > 0, ∀ N, ∃ n ≥ N, |u n - l| ≥ ε := by
-  sorry
+  unfold SequentialLimit
+  push_neg  
+  rfl
   done
 
 lemma sequentialLimit_unique (u : ℕ → ℝ) (l l' : ℝ) :
     SequentialLimit u l → SequentialLimit u l' → l = l' := by
-  sorry
-  done
-
+  intro hl hl'
+  by_contra H
+  have : 0 < |l - l'| := by 
+    exact abs_pos.mpr (sub_ne_zero.mpr H)
+  specialize hl (|l - l'| / 2) (by linarith)
+  specialize hl' (|l - l'| / 2) (by linarith)
+  obtain ⟨N, hN⟩ := hl
+  obtain ⟨N', hN'⟩ := hl' 
+  let N₀ := max N N'
+  have h1 : N₀ ≥ N := by apply le_max_left
+  have h2 : N₀ ≥ N' := by apply le_max_right
+  specialize hN N₀ h1
+  specialize hN' N₀ h2   
+  have key : |l - l'| < |l - l'| := calc 
+      |l - l'| = |u N₀ - l + (l' - u N₀)| := by sorry
+      _ ≤ |u N₀ - l| + |l' - u N₀| := by sorry
+      _ < |l - l'| / 2 + |l - l'| / 2 := by sorry
+      _ = |l - l'| := by ring
+  linarith    
+  done  
+
+
+lemma sequentialLimit_unique1 (u : ℕ → ℝ) (l l' : ℝ) :
+    SequentialLimit u l → SequentialLimit u l' → l = l' := by
+  intro hl hl'
+  by_contra H
+  have hpos : 0 < |l - l'| := by
+    exact abs_pos.mpr (sub_ne_zero.mpr H)
+  -- take ε = |l - l'|/2 > 0 for both limits
+  specialize hl (|l - l'| / 2) (by have := hpos; linarith)
+  specialize hl' (|l - l'| / 2) (by have := hpos; linarith)
+  obtain ⟨N, hN⟩ := hl
+  obtain ⟨N', hN'⟩ := hl'
+  let N₀ := max N N'
+  have h1 : N ≤ N₀ := le_max_left _ _
+  have h2 : N' ≤ N₀ := le_max_right _ _
+  have hA : |l - u N₀| < |l - l'| / 2 := by
+    -- hN gives |u N₀ - l| < ε; flip with abs_sub_comm
+    have := hN N₀ h1
+    simpa [abs_sub_comm] using this
+  have hB : |l' - u N₀| < |l - l'| / 2 := by
+    -- hN' gives |u N₀ - l'| < ε; flip with abs_sub_comm
+    have := hN' N₀ h2
+    simpa [abs_sub_comm] using this
+  -- Triangle inequality contradiction:
+  have key : |l - l'| < |l - l'| := by
+    calc
+      |l - l'|
+          = |(l - u N₀) + (u N₀ - l')| := by ring
+      _ ≤ |l - u N₀| + |u N₀ - l'| := by
+            simpa using abs_add_le (l - u N₀) (u N₀ - l')
+      _ < |l - l'| / 2 + |l - l'| / 2 := by
+            have : |u N₀ - l'| = |l' - u N₀| := by simpa [abs_sub_comm]
+            exact add_lt_add_of_lt_of_lt hA (by simpa [this] using hB)
+      _ = |l - l'| := by linarith
+  exact (lt_irrefl (|l - l'|)) key
 
 /- ## Proving two functions are equal
 
@@ -139,22 +203,27 @@ point, using the `ext` tactic. `ext x` can prove that `f = g` if `f x = g x` for
 -/
 
 example {α β : Type*} {f g : α → β} (h : ∀ x, f x = g x): f = g := by
-  sorry
+  ext x
+  apply h
+  done
 
 -- `rfl` can prove an equality `f = f`,
 example : (fun n ↦ n + 2 : ℤ → ℤ) = (fun n ↦ n + 2 : ℤ → ℤ) := rfl
 
 -- but once two functions are not "obviously" equal, you need `ext` to prove it.
 example : (fun n ↦ n + 2 : ℤ → ℤ) = (fun n ↦ n + 2 + 0 : ℤ → ℤ) := by
-  sorry
+  ext n
+  ring
   done
 
 example : (fun n ↦ 2 * n : ℤ → ℤ) = (fun n ↦ n + n) := by
-  sorry
+  ext n
+  ring
   done
 
 example : (fun (n : ℤ) ↦ 2 * n + 5) = (fun (n : ℤ) ↦ (n + 2) + (n + 6) - 3) := by
-  sorry
+  ext n
+  ring
   done
 
 
@@ -176,7 +245,11 @@ def g : ZMod 5 → ZMod 5 := fun x ↦ x
 
 -- Are f and g always equal? Yes! Let's prove it.
 example : f = g := by
-  sorry
+  ext x 
+  unfold f g
+  have: x= 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 := by
+    fin_cases x <;> simp
+  obtain (rfl | rfl | rfl | rfl | rfl) := this <;> rfl 
   done
 
 
@@ -210,7 +283,8 @@ We have seen two new tactics:
 -- Lean figures out the co-domain of the left hand side, and the type of the function
 -- on the right hand side automatically.
 example : (fun x ↦ x ^ 7 + 2 * x ^ 13 : ZMod 7 → _) = (fun x ↦ 3 * x) := by
-  sorry
+  ext k
+  fin_cases k <;> rfl
   done
 
 -- Both of these examples hold for a deeper mathematical reason.
@@ -261,7 +335,8 @@ You can often find similar theorems nearby the theorem you searched for.
 -/
 
 example (a b x y : ℝ) (h : a < b) (h2 : x ≤ y) : a + exp x < b + exp y := by
-  sorry
+  refine add_lt_add_of_lt_of_le h ?_
+  exact exp_le_exp.mpr h2 
   done
 
 
@@ -271,7 +346,8 @@ This means that these arguments are *implicit*:
 they don't have to be stated, but will be figured out by Lean automatically. -/
 
 lemma cancel_addition {a b c : ℝ} (h : a + b = a + c) : b = c := by
-  sorry
+  rw [add_left_cancel_iff] at h
+  assumption
   done
 
 example {b c : ℝ} (h : 2 + b = 2 + c) : b = c := by
@@ -292,7 +368,9 @@ example {G : Type*} [Group G] (a : G) : a * a⁻¹ = 1 := by
 example {G : Type*} [Group G] (a : G) : a⁻¹ * a * a * a⁻¹ = 1 := by
   -- Let us try `rw?` first.
   -- Now, we use `rw??`.
-  sorry
+  rw [inv_mul_cancel a]
+  rw [one_mul a]
+  exact mul_inv_cancel a
   done
 
 -- You can also use `rw??` at a hypothesis: simply select a local hypothesis in the infoview.
@@ -334,7 +412,10 @@ example (x : ℝ) : x ≤ x := by apply le_refl
 example (x : ℝ) : x ≤ x := by rfl
 
 example (h₀ : a = b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
-  sorry
+  rw [h₀]         -- replace a with b
+  trans d         -- we want to go from b < d
+  · exact h₁.trans_le h₂   -- use b < c and c ≤ d
+  · exact h₃               -- finally d < e
   done
 
 /- `linarith` can prove inequalities (and equalities)
@@ -363,7 +444,8 @@ example (ha : 0 ≤ a) (hb : 0 ≤ b) (h : 0 ≤ c) : a * (b + 2) ≤ (a + c) *
 /- `gcongr` is very convenient for monotonicity of functions. -/
 
 example (h : a ≤ b) (h2 : b ≤ c) : exp a ≤ exp c := by
-  sorry
+  gcongr
+  trans b <;> assumption
   done
 
 example (h : a ≤ b) : c - exp b ≤ c - exp a := by
diff --git a/LeanCourse25/Lectures/Lecture5Before.lean b/LeanCourse25/Lectures/Lecture5Before.lean
index a5fabd1..5e6d1c4 100644
--- a/LeanCourse25/Lectures/Lecture5Before.lean
+++ b/LeanCourse25/Lectures/Lecture5Before.lean
@@ -39,18 +39,23 @@ Last time we saw:
   - `gcongr` applies monotonicity of functions
 -/
 
+#leansearch "abs_add."
+
+
 example (x : ℝ) : (Real.sin x) ^ 2 ≤ 1 := by
-  sorry
+  exact sin_sq_le_one x
   done
 
+#check Complex.exp_add_pi_mul_I
 example : Complex.exp (Complex.I * π) + 1 = 0 := by
-  sorry
+  rw [mul_comm, Complex.exp_pi_mul_I]
+  ring
   done
 
 
 example {a b c d : ℝ} (h₀ : 0 < b) (h₁ : b < a) (h₂ : c ≤ d) :
     1 / a + Real.exp c ≤ 1 / b + Real.exp d := by
-  sorry
+  gcongr
   done
 
 /-
@@ -61,7 +66,9 @@ example {a b c d : ℝ} (h₀ : 0 < b) (h₁ : b < a) (h₂ : c ≤ d) :
 /- Remark: for equalities, you should use `congr` instead of `gcongr` -/
 
 example (h : a = b) : c - exp b = c - exp a := by
-  sorry
+  congr
+  symm
+  exact h
   done
 
 
@@ -71,7 +78,9 @@ example (h : a = b) : c - exp b = c - exp a := by
 
 example {a b c d : ℝ} (h₀ : 0 < b) (h₁ : b < a) (h₂ : c ≤ d) :
     1 / a + exp c ≤ exp d + 1 / b := by
-  sorry
+  grw [← h₁]
+  grw [← h₂]
+  rw[add_comm]
   done
 
 
@@ -85,27 +94,31 @@ In contrast: `rw` can *only* rewrite with `=` or `↔`.
 #check 8 ≡ 3 [ZMOD 5]
 
 example {a b n : ℤ} (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
+--  gcongr
   grw [h]
 
 
 
 example {a b c d n : ℤ} (h : a ≡ b [ZMOD n]) (h' : c ≡ d [ZMOD n]) :
     a ^ 2 * c ≡ b ^ 2 * d [ZMOD n] := by
-  sorry
+  grw[h,h']
   done
 
 
 
 example {a b c : ℤ} (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) :
     a ∣ b ^ 2 * c := by
-  sorry
+  grw[h₁] at *
+  assumption
   done
 
 
 
 example (f g : ℝ → ℝ) (h : ∀ x : ℝ, f x ≤ g x)
     (h₂ : g a + g b ≤ 5) : f a + f b ≤ 5 := by
-  sorry
+  grw[h]
+  grw[h]
+  assumption
   done
 
 
@@ -203,16 +216,29 @@ There are various ways to prove the following lemmas:
 * give a direct proof: `⟨xs, xt⟩`
 -/
 example (hxs : x ∈ s) (hxt : x ∈ t) : x ∈ s ∩ t := by
-  sorry
-  done
+rw [mem_inter_iff x s t]
+constructor
+· assumption
+· assumption
+done
+
+
 
 example (hxs : x ∈ s) : x ∈ s ∪ t := by
-  sorry
+  simp
+  left
+  assumption
   done
 
 
 example (hx : x ∈ s \ t) : x ∈ (s ∪ t) ∩ (sᶜ ∪ tᶜ) := by
-  sorry
+  simp at *
+  obtain ⟨hsx, htx⟩ := hx
+  constructor
+  left
+  exact hsx
+  right
+  exact htx
   done
 
 
@@ -226,12 +252,18 @@ example (hx : x ∈ s \ t) : x ∈ (s ∪ t) ∩ (sᶜ ∪ tᶜ) := by
 #check (subset_def : (s ⊆ t) = ∀ x ∈ s, x ∈ t)
 
 example : s ∩ t ⊆ s ∩ (t ∪ u) := by
-  sorry
+  rw[subset_def]
+  intro x hx
+  constructor
+  · exact hx.1
+  · left
+    exact hx.2
   done
 
 /- You can also prove it at the level of sets, without talking about elements. -/
 example : s ∩ t ⊆ s ∩ (t ∪ u) := by
-  sorry
+  gcongr
+  exact subset_union_left
   done
 
 
@@ -248,17 +280,20 @@ or using the `ext` tactic.
 #check (subset_antisymm : s ⊆ t → t ⊆ s → s = t)
 
 example : s ∩ t = t ∩ s := by
-  sorry
+  ext x
+  simp
+  exact And.comm
   done
 
 /- We can also use existing lemmas and `calc`. -/
 example : (s ∪ tᶜ) ∩ t = s ∩ t := by
-  sorry
+  calc
+    (s ∪ tᶜ) ∩ t = (s ∩ t )∪(tᶜ ∩ t) :=by rw [@union_inter_distrib_right]
+    _ = (s ∩ t )∪∅ :=by rw [@compl_inter_self]
+    _ = s ∩ t  :=by rw [@union_empty]
   done
 
 
-
-
 /-
 ## Set-builder notation
 We can define the set of elements in `t` satisfying `P` using
@@ -272,7 +307,9 @@ def evens : Set ℕ := {n : ℕ | Even n}
 def odds : Set ℕ := {n | Odd n}
 
 example : evensᶜ = odds := by
-  sorry
+  unfold evens odds
+  ext n
+  simp only [mem_compl_iff, mem_setOf_eq, Nat.not_even_iff_odd]
   done
 
 
@@ -347,7 +384,19 @@ example (𝓒 : Set (Set α)) :
 
 example (C : ι → Set α) (s : Set α) :
     s ∩ (⋃ i, C i) = ⋃ i, (C i ∩ s) := by
-  sorry
+  ext x
+  constructor
+  · intro hx
+    obtain ⟨ hxs, hxC⟩ := hx
+    simp at hxC
+    obtain ⟨i , hi⟩ :=hxC
+    simp only [mem_iUnion, mem_inter_iff]
+    use i
+  · simp only [mem_iUnion, mem_inter_iff]
+    intro hx
+    obtain ⟨ i, hxC, hxs ⟩ := hx
+    refine ⟨ hxs, ?_⟩
+    use i
   done
 
 
diff --git a/LeanCourse25/Lectures/Lecture7.lean b/LeanCourse25/Lectures/Lecture7.lean
index 22774ce..a4c8a79 100644
--- a/LeanCourse25/Lectures/Lecture7.lean
+++ b/LeanCourse25/Lectures/Lecture7.lean
@@ -52,6 +52,7 @@ variable (a b c : ℝ)
 /- # Today: structures and classes -/
 
 
+
 /-
 # Structures and classes
 
diff --git a/LeanCourse25/Lectures/Lecture9Before.lean b/LeanCourse25/Lectures/Lecture9Before.lean
index 79e3e63..c1534ec 100644
--- a/LeanCourse25/Lectures/Lecture9Before.lean
+++ b/LeanCourse25/Lectures/Lecture9Before.lean
@@ -20,11 +20,45 @@ variable (a b c : ℝ)
 
 /-- Let's define the equivalence relation for the even numbers: two numbers are equivalent
 iff their difference is an even number. -/
-def evensEquivalenceRelation : Setoid ℤ := sorry
-
-
-
 
+def evensEquivalenceRelation : Setoid ℤ :=
+{ r := fun a b => Even (a - b),
+  iseqv :=
+  ⟨
+    -- Reflexive
+    by
+      intro a
+      show Even (a - a)
+      rw [sub_self]
+      use 0
+      simp,
+
+    -- Symmetric
+    by
+      intro a b h
+      -- h : Even (a - b)
+      rcases h with ⟨k, hk⟩
+      -- hk : a - b = 2 * k
+      show Even (b - a)
+      -- note: b - a = -(a - b)
+      rw [← neg_sub]
+      rw [hk]
+      -- b - a = -(2 * k) = 2 * (-k)
+      use -k
+      ring,
+
+    -- Transitive
+    by
+      intro a b c hab hbc
+      rcases hab with ⟨k₁, hk₁⟩
+      rcases hbc with ⟨k₂, hk₂⟩
+      show Even (a - c)
+      use k₁ + k₂
+      calc
+        a - c = (a - b) + (b - c) := by ring
+        _     = k₁ + k₁ + (k₂ +k₂)  := by rw [hk₁, hk₂]
+        _     = k₁ + k₂ + (k₁ + k₂)    := by ring
+  ⟩ }
 
 
 
diff --git a/LeanCourse25/formal-conjectures b/LeanCourse25/formal-conjectures
new file mode 160000
index 0000000..f8a0e4b
--- /dev/null
+++ b/LeanCourse25/formal-conjectures
@@ -0,0 +1 @@
+Subproject commit f8a0e4b90da15b27cd9c2c5c029b09f54244b467
diff --git a/LeanCourse_Exercises b/LeanCourse_Exercises
new file mode 160000
index 0000000..3ed9aa2
--- /dev/null
+++ b/LeanCourse_Exercises
@@ -0,0 +1 @@
+Subproject commit 3ed9aa28ed3f6a5eea96e039301d29f008b30c46
diff --git a/mathematics_in_lean b/mathematics_in_lean
new file mode 160000
index 0000000..2bf0e10
--- /dev/null
+++ b/mathematics_in_lean
@@ -0,0 +1 @@
+Subproject commit 2bf0e10dd0c02438b65110f85cd9b68a9dbe6e39