diff --git a/README.md b/README.md
index 8b01007..2efb94c 100644
--- a/README.md
+++ b/README.md
@@ -15,18 +15,19 @@ A PDF is [available here for download](../../releases/download/latest/Metaprogra
     8. [DSLs](md/main/08_dsls.md)
     9. [Tactics](md/main/09_tactics.md)
     10. [Cheat sheet](md/main/10_cheat-sheet.md)
-* Extra
     1. [Options](md/extra/01_options.md)
     2. [Attributes](md/extra/02_attributes.md)
-    1. [Pretty Printing](md/extra/03_pretty-printing.md)
+    3. [Pretty Printing](md/extra/03_pretty-printing.md)
 * Solutions to exercises
-    1. ...
-    2. ...
+    1. Introduction
+    2. Overview
     3. [Expressions](md/solutions/03_expressions.md)
     4. [`MetaM`](md/solutions/04_metam.md)
     5. [`Syntax`](md/solutions/05_syntax.md)
-    6. ...
+    6. Macros
     7. [Elaboration](md/solutions/07_elaboration.md)
+    8. DSLs
+    9. [Tactics](md/solutions/09_tactics.md)
 
 Sources to extract material from:
 * [Material written by Ed](https://github.com/leanprover-community/mathlib4/blob/tutorial/docs/metaprogramming/02_metavariables.md)
diff --git a/lean/main/04_metam.lean b/lean/main/04_metam.lean
index 5ec64b1..4ff970d 100644
--- a/lean/main/04_metam.lean
+++ b/lean/main/04_metam.lean
@@ -1214,47 +1214,47 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
 3. [**Metavariables**] Fill in the missing lines in the following code.
 
-  ```
-  #eval show MetaM Unit from do
-    let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
-    let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
-
-    -- Create `mvar1` with type `Nat`
-    -- let mvar1 ← ...
-    -- Create `mvar2` with type `Nat`
-    -- let mvar2 ← ...
-    -- Create `mvar3` with type `Nat`
-    -- let mvar3 ← ...
-
-    -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
-    -- ...
-
-    -- Assign `mvar3` to `1`
-    -- ...
-
-    -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
-    ...
-  ```
+    ```lean
+    #eval show MetaM Unit from do
+      let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
+      let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
+
+      -- Create `mvar1` with type `Nat`
+      -- let mvar1 ← ...
+      -- Create `mvar2` with type `Nat`
+      -- let mvar2 ← ...
+      -- Create `mvar3` with type `Nat`
+      -- let mvar3 ← ...
+
+      -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
+      -- ...
+
+      -- Assign `mvar3` to `1`
+      -- ...
+
+      -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
+      ...
+    ```
 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-  a) What would be the `type` and `userName` of metavariable `mvarId`?  
-  b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
+  **a)** What would be the `type` and `userName` of metavariable `mvarId`?  
+  **b)** What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
   Print them all out.
 
-  ```
-  elab "explore" : tactic => do
-    let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
-    let metavarDecl : MetavarDecl ← mvarId.getDecl
+    ```lean
+    elab "explore" : tactic => do
+      let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
+      let metavarDecl : MetavarDecl ← mvarId.getDecl
 
-    IO.println "Our metavariable"
-    -- ...
+      IO.println "Our metavariable"
+      -- ...
 
-    IO.println "All of its local declarations"
-    -- ...
+      IO.println "All of its local declarations"
+      -- ...
 
-  theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
-    explore
-    sorry
-  ```
+    theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
+      explore
+      sorry
+    ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
 6. [**Computation**] What is the normal form of the following expressions:  
   **a)** `fun x => x` of type `Bool → Bool`  
@@ -1270,36 +1270,36 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
   **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
-```
-@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
-@[instance] def instanceDef       : Nat := 2 -- same as `instance`
-def defaultDef                    : Nat := 3
-@[irreducible] def irreducibleDef : Nat := 4
+    ```lean
+    @[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
+    @[instance] def instanceDef       : Nat := 2 -- same as `instance`
+    def defaultDef                    : Nat := 3
+    @[irreducible] def irreducibleDef : Nat := 4
 
-@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
+    @[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
 
-#eval show MetaM Unit from do
-  let constantExpr := Expr.const `sum []
+    #eval show MetaM Unit from do
+      let constantExpr := Expr.const `sum []
 
-  Meta.withTransparency Meta.TransparencyMode.reducible do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.reducible do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.instances do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.instances do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.default do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.default do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.all do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.all do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  let reducedExpr ← Meta.reduce constantExpr
-  dbg_trace (← ppExpr reducedExpr) -- ...
-```
+      let reducedExpr ← Meta.reduce constantExpr
+      dbg_trace (← ppExpr reducedExpr) -- ...
+    ```
 10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
   **a)** not idiomatically, with loose bound variables  
   **b)** idiomatically.  
@@ -1312,20 +1312,20 @@ def defaultDef                    : Nat := 3
 13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?
 
-```
-#eval show Lean.Elab.Term.TermElabM _ from do
-  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
-  let expr ← Elab.Term.elabTermAndSynthesize stx none
+    ```lean
+    #eval show Lean.Elab.Term.TermElabM _ from do
+      let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
+      let expr ← Elab.Term.elabTermAndSynthesize stx none
 
-  let (_, _, conclusion) ← forallMetaTelescope expr
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaTelescope expr
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← lambdaMetaTelescope expr
-  dbg_trace conclusion -- ...
-```
+      let (_, _, conclusion) ← lambdaMetaTelescope expr
+      dbg_trace conclusion -- ...
+    ```
 15. [**Backtracking**] Check that the expressions `?a + Int` and `"hi" + ?b` are definitionally equal with `isDefEq` (make sure to use the proper types or `Option.none` for the types of your metavariables!).
 Use `saveState` and `restoreState` to revert metavariable assignments.
 -/
diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean
index 410c3ca..0543da0 100644
--- a/lean/main/05_syntax.lean
+++ b/lean/main/05_syntax.lean
@@ -559,68 +559,68 @@ the bound variables, we refer the reader to the macro chapter.
 
 1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
 
-**a)** Using `notation` command.  
-**b)** Using `infix` command.  
-**c)** Using `syntax` command.  
+    **a)** Using `notation` command.  
+    **b)** Using `infix` command.  
+    **c)** Using `syntax` command.  
 
-Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
+    Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
 
 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
 
-```
-  syntax "good morning" : term
-  syntax "hello" : command
-  syntax "yellow" : tactic
-```
+    ```
+      syntax "good morning" : term
+      syntax "hello" : command
+      syntax "yellow" : tactic
+    ```
 
 3. Create a `syntax` rule that would accept the following commands:
 
-- `red red red 4`
-- `blue 7`
-- `blue blue blue blue blue 18`
+    - `red red red 4`
+    - `blue 7`
+    - `blue blue blue blue blue 18`
 
-(So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
+    (So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
 
-Use the following code template:
+    Use the following code template:
 
-```
-syntax (name := colors) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := colors) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 4. Mathlib has a `#help option` command that displays all options available in the current environment, and their descriptions. `#help option pp.r` will display all options starting with a "pp.r" substring.
 
-Create a `syntax` rule that would accept the following commands:
+    Create a `syntax` rule that would accept the following commands:
 
-- `#better_help option`
-- `#better_help option pp.r`
-- `#better_help option some.other.name`
+    - `#better_help option`
+    - `#better_help option pp.r`
+    - `#better_help option some.other.name`
 
-Use the following template:
+    Use the following template:
 
-```
-syntax (name := help) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := help) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 5. Mathlib has a ∑ operator. Create a `syntax` rule that would accept the following terms:
 
-- `∑ x in { 1, 2, 3 }, x^2`
-- `∑ x in { "apple", "banana", "cherry" }, x.length`
+    - `∑ x in { 1, 2, 3 }, x^2`
+    - `∑ x in { "apple", "banana", "cherry" }, x.length`
 
-Use the following template:
+    Use the following template:
 
-```
-import Std.Classes.SetNotation
-import Std.Util.ExtendedBinder
-syntax (name := bigsumin) ...
--- our "elaboration function" that infuses syntax with semantics
-@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
-```
+    ```lean
+    import Std.Classes.SetNotation
+    import Std.Util.ExtendedBinder
+    syntax (name := bigsumin) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
+    ```
 
-Hint: use the `Std.ExtendedBinder.extBinder` parser.
-Hint: you need Std4 installed in your Lean project for these imports to work.
+    Hint: use the `Std.ExtendedBinder.extBinder` parser.
+    Hint: you need Std4 installed in your Lean project for these imports to work.
 
 -/
diff --git a/lean/main/07_elaboration.lean b/lean/main/07_elaboration.lean
index f39bc98..c8d8328 100644
--- a/lean/main/07_elaboration.lean
+++ b/lean/main/07_elaboration.lean
@@ -348,52 +348,52 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
 1. Consider the following code. Rewrite `syntax` + `@[term_elab hi]... : TermElab` combination using just `elab`.
 
-```
-syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
-
-@[term_elab hi]
-def heartElab : TermElab := fun stx tp =>
-  match stx with
-    | `($l:term ♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
-    | `($l:term ♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
-    | `($l:term ♥♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
-    | _ =>
-      throwUnsupportedSyntax
-```
+    ```lean
+    syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
+
+    @[term_elab hi]
+    def heartElab : TermElab := fun stx tp =>
+      match stx with
+        | `($l:term ♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+        | `($l:term ♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+        | `($l:term ♥♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+        | _ =>
+          throwUnsupportedSyntax
+    ```
 
 2. Here is some syntax taken from a real mathlib command `alias`.
 
-```
-syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
-```
+    ```
+    syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
+    ```
 
-We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
+    We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
 
 3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
 
-```
-open Parser.Tactic
-syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
-```
+    ```lean
+    open Parser.Tactic
+    syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
+    ```
 
-We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
+    We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
 
 -/
diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index 86c4f05..208c009 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -587,4 +587,135 @@ A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to
 implement basic features such as rewriting. `Lean.Elab.Tactic.*` contains
 high-level code that connects the low level development in `Lean.Meta` to the
 tactic infrastructure and the parsing front-end.
+
+## Exercises
+
+1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics.
+    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.  
+
+    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.  
+    The tactic `step_1` is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as `mkFreshExprMVar`, `mvarId.assign` and `modify fun _ => { goals := ~)`.
+
+    ```lean
+    -- [this is the initial goal]
+    example : p ∧ q ↔ q ∧ p :=
+      _
+
+    -- step_1
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro _ _
+
+    -- step_2
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          _
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+
+    -- step_3
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          (And.intro _ _)
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+
+    -- step_4
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          (And.intro hA.right hA.left)
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+    ```
+
+    ```lean
+    elab "step_1" : tactic => do
+      let mvarId ← getMainGoal
+      let goalType ← getMainTarget
+
+      let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"
+
+      -- 1. Create new `_`s with appropriate types.
+      let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
+      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+
+      -- 2. Assign the main goal to the expression `Iff.intro _ _`.
+      mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
+
+      -- 3. Report the new `_`s to Lean as the new goals.
+      modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+    ```
+
+    ```lean
+    theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
+      step_1
+      step_2
+      step_3
+      step_4
+    ```
+
+2. In the first exercise, we used lower-level `modify` api to update our goals.  
+    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.  
+    Please rewrite the `forker` tactic with:  
+
+    **a)** `liftMetaTactic`  
+    **b)** `setGoals`  
+    **c)** `replaceMainGoal`  
+
+    ```lean
+    elab "forker" : tactic => do
+      let mvarId ← getMainGoal
+      let goalType ← getMainTarget
+
+      let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId (m!"Goal is not of the form P ∧ Q")
+
+      mvarId.withContext do
+        let mvarIdP ← mkFreshExprMVar p (userName := "red")
+        let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+        let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+        mvarId.assign proofTerm
+
+        modify fun state => { goals := [mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ state.goals.drop 1 }
+    ```
+
+    ```lean
+    example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
+      intro hA hB hC
+      forker
+      forker
+      assumption
+      assumption
+      assumption
+    ```
+
+3. In the first exercise, you created your own `intro` in `step_2` (with a hardcoded hypothesis name, but the basics are the same). When writing tactics, we usually want to use functions such as `intro`, `intro1`, `intro1P`, `introN` or `introNP`.
+
+    For each of the points below, create a tactic `introductor` (one per each point), that turns the goal `(ab: a = b) → (bc: b = c) → (a = c)`:
+
+    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.  
+    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.  
+    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.  
+
+    ```lean
+    example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
+      introductor
+      sorry
+    ```
+
+    Hint: **"P"** in `intro1P` and `introNP` stands for **"Preserve"**.
 -/
diff --git a/lean/solutions/09_tactics.lean b/lean/solutions/09_tactics.lean
new file mode 100644
index 0000000..145080e
--- /dev/null
+++ b/lean/solutions/09_tactics.lean
@@ -0,0 +1,189 @@
+import Lean.Elab.Tactic
+open Lean Elab Tactic Meta
+
+/- ### 1. -/
+
+elab "step_1" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"
+
+  -- 1. Create new `_`s with appropriate types.
+  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
+  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+
+  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
+  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
+
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+
+elab "step_2" : tactic => do
+  let some redMvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red
+  ) | throwError "No mvar with username `red`"
+  let some blueMvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `blue
+  ) | throwError "No mvar with username `blue`"
+
+  ---- HANDLE `red` goal
+  let Expr.forallE _ redFrom redTo _ := (← redMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
+  let handyRedMvarId ← withLocalDecl `hA BinderInfo.default redFrom (fun fvar => do
+    -- 1. Create new `_`s with appropriate types.
+    let mvarId1 ← mkFreshExprMVar redTo MetavarKind.syntheticOpaque `red
+    -- 2. Assign the main goal to the expression `fun hA => _`.
+    redMvarId.assign (← mkLambdaFVars #[fvar] mvarId1)
+    -- just a handy way to return a handyRedMvarId for the next code
+    return mvarId1.mvarId!
+  )
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [handyRedMvarId, blueMvarId] }
+
+  ---- HANDLE `blue` goal
+  let Expr.forallE _ blueFrom _ _ := (← blueMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `fun hB : q ∧ p => (And.intro hB.right hB.left)`.
+  Lean.Meta.withLocalDecl `hB .default blueFrom (fun hB => do
+    let body ← Lean.Meta.mkAppM `And.intro #[← Lean.Meta.mkAppM `And.right #[hB], ← Lean.Meta.mkAppM `And.left #[hB]]
+    blueMvarId.assign (← Lean.Meta.mkLambdaFVars #[hB] body)
+  )
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [handyRedMvarId] }
+
+elab "step_3" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+  let mainDecl ← mvarId.getDecl
+
+  let Expr.app (Expr.app (Expr.const `And _) q) p := goalType | throwError "Goal type is not of the form `And q p`"
+
+  -- 1. Create new `_`s with appropriate types.
+  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := "red1")
+  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := "red2")
+
+  -- 2. Assign the main goal to the expression `And.intro _ _`.
+  mvarId.assign (← mkAppM `And.intro #[mvarId1, mvarId2])
+
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+
+elab "step_4" : tactic => do
+  let some red1MvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red1
+  ) | throwError "No mvar with username `red1`"
+  let some red2MvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red2
+  ) | throwError "No mvar with username `red2`"
+
+  ---- HANDLE `red1` goal
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `hA.right`.
+  let some hA := (← red1MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red1`)"
+  red1MvarId.withContext do
+    red1MvarId.assign (← mkAppM `And.right #[hA.toExpr])
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [red2MvarId] }
+
+  ---- HANDLE `red2` goal
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `hA.left`.
+  let some hA := (← red2MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red2`)"
+  red2MvarId.withContext do
+    red2MvarId.assign (← mkAppM `And.left #[hA.toExpr])
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [] }
+
+theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  step_1
+  step_2
+  step_3
+  step_4
+
+/- ### 2. -/
+
+elab "forker_a" : tactic => do
+  liftMetaTactic fun mvarId => do
+    let (Expr.app (Expr.app (Expr.const `And _) p) q) ← mvarId.getType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    return [mvarIdP.mvarId!, mvarIdQ.mvarId!]
+
+elab "forker_b" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+  mvarId.withContext do
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    setGoals ([mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ (← getGoals).drop 1)
+
+elab "forker_c" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+  mvarId.withContext do
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    replaceMainGoal [mvarIdP.mvarId!, mvarIdQ.mvarId!]
+
+example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
+  intro hA hB hC
+  forker_a
+  forker_a
+  assumption
+  assumption
+  assumption
+
+/- ### 3. -/
+
+elab "introductor_a" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.introN 2
+      return [mvarIdNew]
+
+elab "introductor_b" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.intro1P
+      return [mvarIdNew]
+
+elab "introductor_c" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.intro `wow
+      return [mvarIdNew]
+
+-- So:
+-- `intro`   - **intro**, specify the name manually
+-- `intro1`  - **intro**, make the name inacessible
+-- `intro1P` - **intro**, preserve the original name
+-- `introN`  - **intro many**, specify the names manually
+-- `introNP` - **intro many**, preserve the original names
+
+example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
+  introductor_a
+  -- introductor_b
+  -- introductor_c
+  sorry
diff --git a/md/main/01_intro.md b/md/main/01_intro.md
index d6bd53c..a49c3ef 100644
--- a/md/main/01_intro.md
+++ b/md/main/01_intro.md
@@ -39,7 +39,7 @@ offering some small examples to serve as appetizers for what the book shall
 cover.
 
 Note: the code snippets aren't self-contained. They are supposed to be run/read
-incrementally,starting from the beginning of each chapter.
+incrementally, starting from the beginning of each chapter.
 
 ## What does it mean to be in meta?
 
diff --git a/md/main/04_metam.md b/md/main/04_metam.md
index b3245e1..5ba10bd 100644
--- a/md/main/04_metam.md
+++ b/md/main/04_metam.md
@@ -1212,47 +1212,47 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
 2. [**Metavariables**] What would `instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2])` output?
 3. [**Metavariables**] Fill in the missing lines in the following code.
 
-  ```
-  #eval show MetaM Unit from do
-    let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
-    let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
-
-    -- Create `mvar1` with type `Nat`
-    -- let mvar1 ← ...
-    -- Create `mvar2` with type `Nat`
-    -- let mvar2 ← ...
-    -- Create `mvar3` with type `Nat`
-    -- let mvar3 ← ...
-
-    -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
-    -- ...
-
-    -- Assign `mvar3` to `1`
-    -- ...
-
-    -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
-    ...
-  ```
+    ```lean
+    #eval show MetaM Unit from do
+      let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
+      let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr
+
+      -- Create `mvar1` with type `Nat`
+      -- let mvar1 ← ...
+      -- Create `mvar2` with type `Nat`
+      -- let mvar2 ← ...
+      -- Create `mvar3` with type `Nat`
+      -- let mvar3 ← ...
+
+      -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
+      -- ...
+
+      -- Assign `mvar3` to `1`
+      -- ...
+
+      -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
+      ...
+    ```
 4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-  a) What would be the `type` and `userName` of metavariable `mvarId`?  
-  b) What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
+  **a)** What would be the `type` and `userName` of metavariable `mvarId`?  
+  **b)** What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
   Print them all out.
 
-  ```
-  elab "explore" : tactic => do
-    let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
-    let metavarDecl : MetavarDecl ← mvarId.getDecl
+    ```lean
+    elab "explore" : tactic => do
+      let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
+      let metavarDecl : MetavarDecl ← mvarId.getDecl
 
-    IO.println "Our metavariable"
-    -- ...
+      IO.println "Our metavariable"
+      -- ...
 
-    IO.println "All of its local declarations"
-    -- ...
+      IO.println "All of its local declarations"
+      -- ...
 
-  theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
-    explore
-    sorry
-  ```
+    theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
+      explore
+      sorry
+    ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
 6. [**Computation**] What is the normal form of the following expressions:  
   **a)** `fun x => x` of type `Bool → Bool`  
@@ -1268,36 +1268,36 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
   **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
-```
-@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
-@[instance] def instanceDef       : Nat := 2 -- same as `instance`
-def defaultDef                    : Nat := 3
-@[irreducible] def irreducibleDef : Nat := 4
+    ```lean
+    @[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
+    @[instance] def instanceDef       : Nat := 2 -- same as `instance`
+    def defaultDef                    : Nat := 3
+    @[irreducible] def irreducibleDef : Nat := 4
 
-@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
+    @[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]
 
-#eval show MetaM Unit from do
-  let constantExpr := Expr.const `sum []
+    #eval show MetaM Unit from do
+      let constantExpr := Expr.const `sum []
 
-  Meta.withTransparency Meta.TransparencyMode.reducible do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.reducible do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.instances do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.instances do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.default do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.default do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  Meta.withTransparency Meta.TransparencyMode.all do
-    let reducedExpr ← Meta.reduce constantExpr
-    dbg_trace (← ppExpr reducedExpr) -- ...
+      Meta.withTransparency Meta.TransparencyMode.all do
+        let reducedExpr ← Meta.reduce constantExpr
+        dbg_trace (← ppExpr reducedExpr) -- ...
 
-  let reducedExpr ← Meta.reduce constantExpr
-  dbg_trace (← ppExpr reducedExpr) -- ...
-```
+      let reducedExpr ← Meta.reduce constantExpr
+      dbg_trace (← ppExpr reducedExpr) -- ...
+    ```
 10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
   **a)** not idiomatically, with loose bound variables  
   **b)** idiomatically.  
@@ -1310,19 +1310,19 @@ def defaultDef                    : Nat := 3
 13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?
 
-```
-#eval show Lean.Elab.Term.TermElabM _ from do
-  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
-  let expr ← Elab.Term.elabTermAndSynthesize stx none
+    ```lean
+    #eval show Lean.Elab.Term.TermElabM _ from do
+      let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
+      let expr ← Elab.Term.elabTermAndSynthesize stx none
 
-  let (_, _, conclusion) ← forallMetaTelescope expr
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaTelescope expr
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
-  dbg_trace conclusion -- ...
+      let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
+      dbg_trace conclusion -- ...
 
-  let (_, _, conclusion) ← lambdaMetaTelescope expr
-  dbg_trace conclusion -- ...
-```
+      let (_, _, conclusion) ← lambdaMetaTelescope expr
+      dbg_trace conclusion -- ...
+    ```
 15. [**Backtracking**] Check that the expressions `?a + Int` and `"hi" + ?b` are definitionally equal with `isDefEq` (make sure to use the proper types or `Option.none` for the types of your metavariables!).
 Use `saveState` and `restoreState` to revert metavariable assignments.
diff --git a/md/main/05_syntax.md b/md/main/05_syntax.md
index 0ae7ab5..968c014 100644
--- a/md/main/05_syntax.md
+++ b/md/main/05_syntax.md
@@ -557,66 +557,66 @@ the bound variables, we refer the reader to the macro chapter.
 
 1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
 
-**a)** Using `notation` command.  
-**b)** Using `infix` command.  
-**c)** Using `syntax` command.  
+    **a)** Using `notation` command.  
+    **b)** Using `infix` command.  
+    **c)** Using `syntax` command.  
 
-Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
+    Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
 
 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
 
-```
-  syntax "good morning" : term
-  syntax "hello" : command
-  syntax "yellow" : tactic
-```
+    ```
+      syntax "good morning" : term
+      syntax "hello" : command
+      syntax "yellow" : tactic
+    ```
 
 3. Create a `syntax` rule that would accept the following commands:
 
-- `red red red 4`
-- `blue 7`
-- `blue blue blue blue blue 18`
+    - `red red red 4`
+    - `blue 7`
+    - `blue blue blue blue blue 18`
 
-(So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
+    (So, either all `red`s followed by a number; or all `blue`s followed by a number; `red blue blue 5` - shouldn't work.)
 
-Use the following code template:
+    Use the following code template:
 
-```
-syntax (name := colors) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := colors) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 4. Mathlib has a `#help option` command that displays all options available in the current environment, and their descriptions. `#help option pp.r` will display all options starting with a "pp.r" substring.
 
-Create a `syntax` rule that would accept the following commands:
+    Create a `syntax` rule that would accept the following commands:
 
-- `#better_help option`
-- `#better_help option pp.r`
-- `#better_help option some.other.name`
+    - `#better_help option`
+    - `#better_help option pp.r`
+    - `#better_help option some.other.name`
 
-Use the following template:
+    Use the following template:
 
-```
-syntax (name := help) ...
--- our "elaboration function" that infuses syntax with semantics
-@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
-```
+    ```lean
+    syntax (name := help) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
+    ```
 
 5. Mathlib has a ∑ operator. Create a `syntax` rule that would accept the following terms:
 
-- `∑ x in { 1, 2, 3 }, x^2`
-- `∑ x in { "apple", "banana", "cherry" }, x.length`
+    - `∑ x in { 1, 2, 3 }, x^2`
+    - `∑ x in { "apple", "banana", "cherry" }, x.length`
 
-Use the following template:
+    Use the following template:
 
-```
-import Std.Classes.SetNotation
-import Std.Util.ExtendedBinder
-syntax (name := bigsumin) ...
--- our "elaboration function" that infuses syntax with semantics
-@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
-```
+    ```lean
+    import Std.Classes.SetNotation
+    import Std.Util.ExtendedBinder
+    syntax (name := bigsumin) ...
+    -- our "elaboration function" that infuses syntax with semantics
+    @[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
+    ```
 
-Hint: use the `Std.ExtendedBinder.extBinder` parser.
-Hint: you need Std4 installed in your Lean project for these imports to work.
+    Hint: use the `Std.ExtendedBinder.extBinder` parser.
+    Hint: you need Std4 installed in your Lean project for these imports to work.
diff --git a/md/main/07_elaboration.md b/md/main/07_elaboration.md
index ebb55d9..92c94dd 100644
--- a/md/main/07_elaboration.md
+++ b/md/main/07_elaboration.md
@@ -347,50 +347,50 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
 1. Consider the following code. Rewrite `syntax` + `@[term_elab hi]... : TermElab` combination using just `elab`.
 
-```
-syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
-
-@[term_elab hi]
-def heartElab : TermElab := fun stx tp =>
-  match stx with
-    | `($l:term ♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
-    | `($l:term ♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
-    | `($l:term ♥♥♥) => do
-      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
-      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
-    | _ =>
-      throwUnsupportedSyntax
-```
+    ```lean
+    syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term
+
+    @[term_elab hi]
+    def heartElab : TermElab := fun stx tp =>
+      match stx with
+        | `($l:term ♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
+        | `($l:term ♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
+        | `($l:term ♥♥♥) => do
+          let nExpr ← elabTermEnsuringType l (mkConst `Nat)
+          return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
+        | _ =>
+          throwUnsupportedSyntax
+    ```
 
 2. Here is some syntax taken from a real mathlib command `alias`.
 
-```
-syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
-```
+    ```
+    syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
+    ```
 
-We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
+    We want `alias hi ← hello yes` to print out the identifiers after `←` - that is, "hello" and "yes".
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
 
 3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
 
-```
-open Parser.Tactic
-syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
-```
+    ```lean
+    open Parser.Tactic
+    syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
+    ```
 
-We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
+    We want `nth_rewrite 5 [←add_zero a] at h` to print out `"rewrite location!"` if the user provided location, and `"rewrite target!"` if the user didn't provide location.
 
-Please add these semantics:
+    Please add these semantics:
 
-**a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-**b)** using `syntax` + `elab_rules`.  
-**c)** using `elab`.
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
+    **b)** using `syntax` + `elab_rules`.  
+    **c)** using `elab`.
diff --git a/md/main/09_tactics.md b/md/main/09_tactics.md
index e2f7ff1..5c0960a 100644
--- a/md/main/09_tactics.md
+++ b/md/main/09_tactics.md
@@ -586,3 +586,134 @@ A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to
 implement basic features such as rewriting. `Lean.Elab.Tactic.*` contains
 high-level code that connects the low level development in `Lean.Meta` to the
 tactic infrastructure and the parsing front-end.
+
+## Exercises
+
+1. Consider the theorem `p ∧ q ↔ q ∧ p`. We could either write its proof as a proof term, or construct it using the tactics.
+    When we are writing the proof of this theorem *as a proof term*, we're gradually filling up `_`s with certain expressions, step by step. Each such step corresponds to a tactic.  
+
+    There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic.  
+    The tactic `step_1` is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as `mkFreshExprMVar`, `mvarId.assign` and `modify fun _ => { goals := ~)`.
+
+    ```lean
+    -- [this is the initial goal]
+    example : p ∧ q ↔ q ∧ p :=
+      _
+
+    -- step_1
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro _ _
+
+    -- step_2
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          _
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+
+    -- step_3
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          (And.intro _ _)
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+
+    -- step_4
+    example : p ∧ q ↔ q ∧ p :=
+      Iff.intro
+        (
+          fun hA =>
+          (And.intro hA.right hA.left)
+        )
+        (
+          fun hB =>
+          (And.intro hB.right hB.left)
+        )
+    ```
+
+    ```lean
+    elab "step_1" : tactic => do
+      let mvarId ← getMainGoal
+      let goalType ← getMainTarget
+
+      let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"
+
+      -- 1. Create new `_`s with appropriate types.
+      let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
+      let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+
+      -- 2. Assign the main goal to the expression `Iff.intro _ _`.
+      mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
+
+      -- 3. Report the new `_`s to Lean as the new goals.
+      modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+    ```
+
+    ```lean
+    theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
+      step_1
+      step_2
+      step_3
+      step_4
+    ```
+
+2. In the first exercise, we used lower-level `modify` api to update our goals.  
+    `liftMetaTactic`, `setGoals`, `appendGoals`, `replaceMainGoal`, `closeMainGoal`, etc. are all syntax sugars on top of `modify fun s : State => { s with goals := myMvarIds }`.  
+    Please rewrite the `forker` tactic with:  
+
+    **a)** `liftMetaTactic`  
+    **b)** `setGoals`  
+    **c)** `replaceMainGoal`  
+
+    ```lean
+    elab "forker" : tactic => do
+      let mvarId ← getMainGoal
+      let goalType ← getMainTarget
+
+      let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId (m!"Goal is not of the form P ∧ Q")
+
+      mvarId.withContext do
+        let mvarIdP ← mkFreshExprMVar p (userName := "red")
+        let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+        let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+        mvarId.assign proofTerm
+
+        modify fun state => { goals := [mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ state.goals.drop 1 }
+    ```
+
+    ```lean
+    example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
+      intro hA hB hC
+      forker
+      forker
+      assumption
+      assumption
+      assumption
+    ```
+
+3. In the first exercise, you created your own `intro` in `step_2` (with a hardcoded hypothesis name, but the basics are the same). When writing tactics, we usually want to use functions such as `intro`, `intro1`, `intro1P`, `introN` or `introNP`.
+
+    For each of the points below, create a tactic `introductor` (one per each point), that turns the goal `(ab: a = b) → (bc: b = c) → (a = c)`:
+
+    **a)** into the goal `(a = c)` with hypotheses `(ab✝: a = b)` and `(bc✝: b = c)`.  
+    **b)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(ab: a = b)`.  
+    **c)** into the goal `(bc: b = c) → (a = c)` with hypothesis `(hello: a = b)`.  
+
+    ```lean
+    example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
+      introductor
+      sorry
+    ```
+
+    Hint: **"P"** in `intro1P` and `introNP` stands for **"Preserve"**.
diff --git a/md/solutions/09_tactics.md b/md/solutions/09_tactics.md
new file mode 100644
index 0000000..17af738
--- /dev/null
+++ b/md/solutions/09_tactics.md
@@ -0,0 +1,197 @@
+```lean
+import Lean.Elab.Tactic
+open Lean Elab Tactic Meta
+```
+
+### 1.
+
+```lean
+elab "step_1" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"
+
+  -- 1. Create new `_`s with appropriate types.
+  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
+  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 
+
+  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
+  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
+
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+
+elab "step_2" : tactic => do
+  let some redMvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red
+  ) | throwError "No mvar with username `red`"
+  let some blueMvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `blue
+  ) | throwError "No mvar with username `blue`"
+
+  ---- HANDLE `red` goal
+  let Expr.forallE _ redFrom redTo _ := (← redMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
+  let handyRedMvarId ← withLocalDecl `hA BinderInfo.default redFrom (fun fvar => do
+    -- 1. Create new `_`s with appropriate types.
+    let mvarId1 ← mkFreshExprMVar redTo MetavarKind.syntheticOpaque `red
+    -- 2. Assign the main goal to the expression `fun hA => _`.
+    redMvarId.assign (← mkLambdaFVars #[fvar] mvarId1)
+    -- just a handy way to return a handyRedMvarId for the next code
+    return mvarId1.mvarId!
+  )
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [handyRedMvarId, blueMvarId] }
+
+  ---- HANDLE `blue` goal
+  let Expr.forallE _ blueFrom _ _ := (← blueMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `fun hB : q ∧ p => (And.intro hB.right hB.left)`.
+  Lean.Meta.withLocalDecl `hB .default blueFrom (fun hB => do
+    let body ← Lean.Meta.mkAppM `And.intro #[← Lean.Meta.mkAppM `And.right #[hB], ← Lean.Meta.mkAppM `And.left #[hB]]
+    blueMvarId.assign (← Lean.Meta.mkLambdaFVars #[hB] body)
+  )
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [handyRedMvarId] }
+
+elab "step_3" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+  let mainDecl ← mvarId.getDecl
+
+  let Expr.app (Expr.app (Expr.const `And _) q) p := goalType | throwError "Goal type is not of the form `And q p`"
+
+  -- 1. Create new `_`s with appropriate types.
+  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := "red1")
+  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := "red2")
+
+  -- 2. Assign the main goal to the expression `And.intro _ _`.
+  mvarId.assign (← mkAppM `And.intro #[mvarId1, mvarId2])
+
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+
+elab "step_4" : tactic => do
+  let some red1MvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red1
+  ) | throwError "No mvar with username `red1`"
+  let some red2MvarId ← (← get).goals.findM? (fun mvarId => do
+    return (← mvarId.getDecl).userName == `red2
+  ) | throwError "No mvar with username `red2`"
+
+  ---- HANDLE `red1` goal
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `hA.right`.
+  let some hA := (← red1MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red1`)"
+  red1MvarId.withContext do
+    red1MvarId.assign (← mkAppM `And.right #[hA.toExpr])
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [red2MvarId] }
+
+  ---- HANDLE `red2` goal
+  -- 1. Create new `_`s with appropriate types.
+  -- None needed!
+  -- 2. Assign the main goal to the expression `hA.left`.
+  let some hA := (← red2MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red2`)"
+  red2MvarId.withContext do
+    red2MvarId.assign (← mkAppM `And.left #[hA.toExpr])
+  -- 3. Report the new `_`s to Lean as the new goals.
+  modify fun _ => { goals := [] }
+
+theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  step_1
+  step_2
+  step_3
+  step_4
+```
+
+### 2.
+
+```lean
+elab "forker_a" : tactic => do
+  liftMetaTactic fun mvarId => do
+    let (Expr.app (Expr.app (Expr.const `And _) p) q) ← mvarId.getType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    return [mvarIdP.mvarId!, mvarIdQ.mvarId!]
+
+elab "forker_b" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+  mvarId.withContext do
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    setGoals ([mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ (← getGoals).drop 1)
+
+elab "forker_c" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")
+
+  mvarId.withContext do
+    let mvarIdP ← mkFreshExprMVar p (userName := "red")
+    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
+
+    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
+    mvarId.assign proofTerm
+
+    replaceMainGoal [mvarIdP.mvarId!, mvarIdQ.mvarId!]
+
+example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
+  intro hA hB hC
+  forker_a
+  forker_a
+  assumption
+  assumption
+  assumption
+```
+
+### 3.
+
+```lean
+elab "introductor_a" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.introN 2
+      return [mvarIdNew]
+
+elab "introductor_b" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.intro1P
+      return [mvarIdNew]
+
+elab "introductor_c" : tactic => do
+  withMainContext do
+    liftMetaTactic fun mvarId => do
+      let (_, mvarIdNew) ← mvarId.intro `wow
+      return [mvarIdNew]
+
+-- So:
+-- `intro`   - **intro**, specify the name manually
+-- `intro1`  - **intro**, make the name inacessible
+-- `intro1P` - **intro**, preserve the original name
+-- `introN`  - **intro many**, specify the names manually
+-- `introNP` - **intro many**, preserve the original names
+
+example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
+  introductor_a
+  -- introductor_b
+  -- introductor_c
+  sorry
+```