diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
new file mode 100644
index 0000000..6bc5f02
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
@@ -0,0 +1,158 @@
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+namespace C03S01
+
+def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, f x ≤ a
+
+def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, a ≤ f x
+
+section
+variable (f g : ℝ → ℝ) (a b : ℝ)
+
+example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
+  duper [add_le_add, *, FnUb]
+
+example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) := by
+  duper [add_le_add, *, FnLb]
+
+example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 := by
+  duper [mul_nonneg, *, FnLb]
+
+example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
+    FnUb (fun x ↦ f x * g x) (a * b) := by
+  duper [mul_le_mul, *, FnUb, FnLb]
+
+end
+
+section
+variable {α : Type*} {R : Type*} [OrderedCancelAddCommMonoid R]
+
+#check add_le_add
+
+def FnUb' (f : α → R) (a : R) : Prop :=
+  ∀ x, f x ≤ a
+
+theorem fnUb_add {f g : α → R} {a b : R} (hfa : FnUb' f a) (hgb : FnUb' g b) :
+    FnUb' (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)
+
+end
+
+example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
+  @h
+
+section
+variable (f g : ℝ → ℝ)
+
+example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
+  -- interesting: duper doesn't work unless you intro first
+  --intro a b aleb
+  rw [Monotone]
+  duper [Monotone, add_le_add, *]
+
+example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x := by
+  intro a b aleb
+  apply mul_le_mul_of_nonneg_left _ nnc
+  apply mf aleb
+
+example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x := by
+  duper [*, Monotone, mul_le_mul_of_nonneg_left]
+
+example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) := by
+  intro a b aleb
+  apply mf
+  apply mg
+  apply aleb
+
+example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) := by
+  duper [Monotone, *]
+
+def FnEven (f : ℝ → ℝ) : Prop :=
+  ∀ x, f x = f (-x)
+
+def FnOdd (f : ℝ → ℝ) : Prop :=
+  ∀ x, f x = -f (-x)
+
+example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
+  intro x
+  calc
+    (fun x ↦ f x + g x) x = f x + g x := rfl
+    _ = f (-x) + g (-x) := by rw [ef, eg]
+
+example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
+  duper [*, FnEven]
+
+example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
+  duper [*, FnOdd, FnEven, neg_mul_neg]
+
+example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
+  intro x
+  dsimp
+  rw [ef, og, neg_mul_eq_mul_neg]
+
+example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
+  intro x
+  dsimp
+  rw [og, ← ef]
+
+example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
+  duper [*, FnEven, FnOdd, neg_mul_eq_mul_neg]
+
+example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
+  duper [*, FnEven, FnOdd]
+
+end
+
+section
+
+variable {α : Type*} (r s t : Set α)
+
+example : s ⊆ s := by
+  intro x xs
+  exact xs
+
+example : s ⊆ s := by
+  duper [Set.subset_def]
+
+theorem Subset.refl : s ⊆ s := fun x xs ↦ xs
+
+theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
+  duper [Set.subset_def]
+
+end
+
+section
+variable {α : Type*} [PartialOrder α]
+variable (s : Set α) (a b : α)
+
+def SetUb (s : Set α) (a : α) :=
+  ∀ x, x ∈ s → x ≤ a
+
+example (h : SetUb s a) (h' : a ≤ b) : SetUb s b := by
+  duper [*, SetUb, le_trans]
+
+end
+
+section
+
+open Function
+
+example (c : ℝ) : Injective fun x ↦ x + c := by
+  intro x₁ x₂ h'
+  exact (add_left_inj c).mp h'
+
+example (c : ℝ) : Injective fun x ↦ x + c := by
+  duper [*, Injective, add_left_inj]
+
+example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
+  duper [*, Injective, mul_right_inj']
+
+variable {α : Type*} {β : Type*} {γ : Type*}
+variable {g : β → γ} {f : α → β}
+
+example (injg : Injective g) (injf : Injective f) : Injective fun x ↦ g (f x) := by
+  duper [*, Injective]
+
+end
diff --git a/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S02_The_Existential_Quantifier.lean b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S02_The_Existential_Quantifier.lean
new file mode 100644
index 0000000..8300d8b
--- /dev/null
+++ b/DuperOnMathlib/DuperOnMathlib/MIL/C03_Logic/S02_The_Existential_Quantifier.lean
@@ -0,0 +1,156 @@
+
+import Mathlib.Data.Real.Basic
+import Duper.Tactic
+
+set_option autoImplicit true
+
+namespace C03S02
+
+example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
+  use 5 / 2
+  norm_num
+
+
+def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, f x ≤ a
+
+def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
+  ∀ x, a ≤ f x
+
+def FnHasUb (f : ℝ → ℝ) :=
+  ∃ a, FnUb f a
+
+def FnHasLb (f : ℝ → ℝ) :=
+  ∃ a, FnLb f a
+
+theorem fnUb_add {f g : ℝ → ℝ} {a b : ℝ} (hfa : FnUb f a) (hgb : FnUb g b) :
+    FnUb (fun x ↦ f x + g x) (a + b) := by
+  simp only [FnUb] at *
+  duper [FnUb, add_le_add, *]
+
+section
+
+variable {f g : ℝ → ℝ}
+
+example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
+  rcases ubf with ⟨a, ubfa⟩
+  rcases ubg with ⟨b, ubgb⟩
+  use a + b
+  apply fnUb_add ubfa ubgb
+
+example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
+  duper [*, FnHasUb, FnUb, add_le_add]
+
+
+example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
+  duper [*, FnHasLb, FnLb, add_le_add]
+
+example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
+  rcases ubf with ⟨a, lbfa⟩
+  use c * a
+  intro x
+  exact mul_le_mul_of_nonneg_left (lbfa x) h
+
+example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
+  duper [*, FnHasUb, FnUb, mul_le_mul_of_nonneg_left]
+
+example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
+  rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩
+  exact ⟨a + b, fnUb_add ubfa ubgb⟩
+
+example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
+  duper [*, FnHasUb, fnUb_add]
+
+example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
+  fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩
+
+example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
+  duper [*, FnHasUb, fnUb_add]
+
+end
+
+example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
+  duper [*, FnHasUb, fnUb_add]
+
+
+section
+
+variable {α : Type*} [CommRing α]
+
+def SumOfSquares (x : α) :=
+  ∃ a b, x = a ^ 2 + b ^ 2
+
+theorem sumOfSquares_mul {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
+    SumOfSquares (x * y) := by
+  rcases sosx with ⟨a, b, xeq⟩
+  rcases sosy with ⟨c, d, yeq⟩
+  rw [xeq, yeq]
+  use a * c - b * d, a * d + b * c
+  ring
+
+theorem sumOfSquares_mul' {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
+    SumOfSquares (x * y) := by
+  rcases sosx with ⟨a, b, rfl⟩
+  rcases sosy with ⟨c, d, rfl⟩
+  use a * c - b * d, a * d + b * c
+  ring
+
+end
+
+section
+variable {a b c : ℕ}
+
+example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
+  rcases divab with ⟨d, beq⟩
+  rcases divbc with ⟨e, ceq⟩
+  rw [ceq, beq]
+  use d * e; ring
+
+example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
+  duper [dvd_def, mul_assoc, *]
+
+example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
+  duper [dvd_def, mul_add, *]
+
+end
+
+section
+
+open Function
+
+example {c : ℝ} : Surjective fun x ↦ x + c := by
+  intro x
+  use x - c
+  dsimp; ring
+
+example {c : ℝ} : Surjective fun x ↦ x + c := by
+  duper [Surjective, sub_add_cancel]
+
+example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
+  duper [Surjective, div_mul_cancel, mul_comm, *]
+
+example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
+  field_simp [h]
+  ring
+
+example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
+  rcases h 2 with ⟨x, hx⟩
+  use x
+  rw [hx]
+  norm_num
+
+example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
+  have : (2 : ℝ)^2 = 4 := by norm_num
+  duper [*, Surjective]
+
+end
+
+section
+open Function
+variable {α : Type*} {β : Type*} {γ : Type*}
+variable {g : β → γ} {f : α → β}
+
+example (surjg : Surjective g) (surjf : Surjective f) : Surjective fun x ↦ g (f x) := by
+  duper [Surjective, *]
+
+end