diff --git a/tactics.lean b/tactics.lean
index b40a5f3..b1e5e29 100644
--- a/tactics.lean
+++ b/tactics.lean
@@ -2,8 +2,74 @@
 -- 5. Tactics
 --
 
---
+-- Entering Tactic Mode
+
 theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
   apply And.intro
   exact hp
   exact { left := hq, right := hp }
+
+#print test
+
+example (hp : p) (hq : q) : p ∧ q ∧ p := by
+  apply And.intro hp
+  exact And.intro hq hp
+
+example (hp : p) (hq : q) : p ∧ q ∧ p := by
+  apply And.intro
+  case left => exact hp
+  case right =>
+    apply And.intro
+    case left => exact hq
+    case right => exact hp
+
+example (hp : p) (hq : q) : p ∧ q ∧ p := by
+  apply And.intro
+  . exact hp
+  . apply And.intro
+    . exact hq
+    . exact hp
+
+-- Basic Tactics
+
+example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
+  apply Iff.intro
+  . intro h
+    apply Or.elim (And.right h)
+    . intro hq
+      apply Or.inl
+      apply And.intro
+      . exact And.left h
+      . exact hq
+    . intro hr
+      apply Or.inr
+      apply And.intro
+      . exact And.left h
+      . exact hr
+  . intro h
+    apply Or.elim h
+    . intro hpq
+      apply And.intro
+      . exact And.left hpq
+      . apply Or.inl
+        exact And.right hpq
+    . intro hpr
+      apply And.intro
+      . exact And.left hpr
+      . apply Or.inr
+        exact And.right hpr
+
+example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro ⟨w, hpq⟩
+  exact ⟨w, hpq.symm⟩
+
+example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro ⟨w, hp, hq⟩
+  exact ⟨w, hq, hp⟩
+
+example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro ⟨w, hp, hq⟩
+  apply Exists.intro
+  case w => exact w
+  case h =>
+    exact ⟨hq, hp⟩