fix: malformed/misaligned markdown code fences

src/Lean/Elab/Term.lean

@@ -850,13 +850,13 @@ Otherwise, we just use the basic `tryCoe`.
 
 Extensions for monads.
 
-1- Try to unify `n` and `m`. If it succeeds, then we use
-   ```
-   coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
-   ```
-   `n` must be a `Monad` to use this one.
+1. Try to unify `n` and `m`. If it succeeds, then we use
+  ```
+  coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
+  ```
+  `n` must be a `Monad` to use this one.
 
-2- If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
+2. If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
   ```
   liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
   ```
@@ -871,7 +871,7 @@ Extensions for monads.
 
   ```
 
-3- If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use
+3. If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use
   ```
   liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β
   ```

src/Lean/Meta/Match/Match.lean

@@ -188,18 +188,18 @@ private def processAsPattern (p : Problem) : MetaM Problem :=
       match alt.patterns with
       | Pattern.as fvarId p h :: ps =>
         /- We used to use `checkAndReplaceFVarId` here, but `x` and `fvarId` may have different types
-           when dependent types are beind used. Let's consider the repro for issue #471
-           ```
-            inductive vec : Nat → Type
-            | nil : vec 0
-            | cons : Int → vec n → vec n.succ
+          when dependent types are beind used. Let's consider the repro for issue #471
+          ```
+          inductive vec : Nat → Type
+          | nil : vec 0
+          | cons : Int → vec n → vec n.succ
 
-            def vec_len : vec n → Nat
-            | vec.nil => 0
-            | x@(vec.cons h t) => vec_len t + 1
+          def vec_len : vec n → Nat
+          | vec.nil => 0
+          | x@(vec.cons h t) => vec_len t + 1
 
-           ```
-           we reach the state
+          ```
+          we reach the state
           ```
             [Meta.Match.match] remaining variables: [x✝:(vec n✝)]
             alternatives:
@@ -297,7 +297,7 @@ def assign (fvarId : FVarId) (v : Expr) : M Bool := do
         The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives.
         The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable.
         After applying the variable-transition step twice, we reach the following state
-        ``lean
+        ```lean
         [Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
         alternatives:
           [g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g

tests/elabissues/issues8.lean

@@ -7,6 +7,7 @@ The following example works, but it adds a coercion at `forceInt i`.
 The elaborated term is
 ```
 fun (n i : Nat) => if n == i then forceNat n else forceInt (coe i)
+```
 -/
 fun n i => if n == i then forceNat n else forceInt i -- works