leanprover-community · grunweg · May 12, 2026
diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean
@@ -238,8 +238,10 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) :
 
 It looks like this as a `2l x 2l` matrix of `l x l` blocks:
 
-   [ 0 1 ]
-   [ 1 0 ]
+```
+[ 0 1 ]
+[ 1 0 ]
+```
 -/
 def JD : Matrix (l ⊕ l) (l ⊕ l) R :=
   Matrix.fromBlocks 0 1 1 0
@@ -254,9 +256,10 @@ diagonal matrix.
 
 It looks like this as a `2l x 2l` matrix of `l x l` blocks:
 
-   [ 1 -1 ]
-   [ 1  1 ]
--/
+```
+[ 1 -1 ]
+[ 1  1 ]
+``` -/
 def PD : Matrix (l ⊕ l) (l ⊕ l) R :=
   Matrix.fromBlocks 1 (-1) 1 1
 
@@ -295,15 +298,19 @@ noncomputable def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃
 
 It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
 
-   [ 2 0 0 ]
-   [ 0 0 1 ]
-   [ 0 1 0 ]
+```
+[ 2 0 0 ]
+[ 0 0 1 ]
+[ 0 1 0 ]
+```
 
 where sizes of the blocks are:
 
-   [`1 x 1` `1 x l` `1 x l`]
-   [`l x 1` `l x l` `l x l`]
-   [`l x 1` `l x l` `l x l`]
+```
+[`1 x 1` `1 x l` `1 x l`]
+[`l x 1` `l x l` `l x l`]
+[`l x 1` `l x l` `l x l`]
+```
 -/
 def JB :=
   Matrix.fromBlocks ((2 : R) • (1 : Matrix Unit Unit R)) 0 0 (JD l R)
@@ -318,16 +325,19 @@ almost-split-signature diagonal matrix.
 
 It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
 
-   [ 1 0  0 ]
-   [ 0 1 -1 ]
-   [ 0 1  1 ]
+```
+[ 1 0  0 ]
+[ 0 1 -1 ]
+[ 0 1  1 ]
+```
 
 where sizes of the blocks are:
 
-   [`1 x 1` `1 x l` `1 x l`]
-   [`l x 1` `l x l` `l x l`]
-   [`l x 1` `l x l` `l x l`]
--/
+```
+[`1 x 1` `1 x l` `1 x l`]
+[`l x 1` `l x l` `l x l`]
+[`l x 1` `l x l` `l x l`]
+``` -/
 def PB :=
   Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (PD l R)
 

diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
@@ -240,9 +240,11 @@ instance instSProd : SProd (List α) (List β) (List (α × β)) where
   sprod := List.product
 
 /-- `dedup l` removes duplicates from `l` (taking only the last occurrence).
-  Defined as `pwFilter (≠)`.
+Defined as `pwFilter (≠)`.
 
-     dedup [1, 0, 2, 2, 1] = [0, 2, 1] -/
+```
+dedup [1, 0, 2, 2, 1] = [0, 2, 1]
+``` -/
 def dedup [DecidableEq α] : List α → List α :=
   pwFilter (· ≠ ·)
 

diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean
@@ -23,7 +23,9 @@ collection of theorems is to show the equivalence of the different approaches.
 
 /-- The type of positive binary numbers.
 
-     13 = 1101(base 2) = bit1 (bit0 (bit1 one)) -/
+```
+13 = 1101(base 2) = bit1 (bit0 (bit1 one))
+``` -/
 inductive PosNum : Type
   | one : PosNum
   | bit1 : PosNum → PosNum
@@ -38,7 +40,9 @@ instance : Inhabited PosNum :=
 
 /-- The type of nonnegative binary numbers, using `PosNum`.
 
-     13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one))) -/
+```
+13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
+``` -/
 inductive Num : Type
   | zero : Num
   | pos : PosNum → Num
@@ -55,8 +59,10 @@ instance : Inhabited Num :=
 
 /-- Representation of integers using trichotomy around zero.
 
-     13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
-     -13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one))) -/
+```
+13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
+-13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one)))
+``` -/
 inductive ZNum : Type
   | zero : ZNum
   | pos : PosNum → ZNum

diff --git a/Mathlib/Data/Num/Bitwise.lean b/Mathlib/Data/Num/Bitwise.lean
@@ -216,20 +216,25 @@ inductive NzsNum : Type
   | bit : Bool → NzsNum → NzsNum
   deriving DecidableEq
 
-/-- Alternative representation of integers using a sign bit at the end.
-  The convention on sign here is to have the argument to `msb` denote
-  the sign of the MSB itself, with all higher bits set to the negation
-  of this sign. The result is interpreted in two's complement.
+/--
+Alternative representation of integers using a sign bit at the end.
+The convention on sign here is to have the argument to `msb` denote
+the sign of the MSB itself, with all higher bits set to the negation
+of this sign. The result is interpreted in two's complement.
 
-     13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true))))
-     -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))
+```
+13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true))))
+-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))
+```
 
   As with `Num`, a special case must be added for zero, which has no msb,
-  but by two's complement symmetry there is a second special case for -1.
-  Here the `Bool` field indicates the sign of the number.
+but by two's complement symmetry there is a second special case for -1.
+Here the `Bool` field indicates the sign of the number.
 
-     0  = ..0000000(base 2) = zero false
-     -1 = ..1111111(base 2) = zero true -/
+```
+0  = ..0000000(base 2) = zero false
+-1 = ..1111111(base 2) = zero true
+``` -/
 inductive SNum : Type
   | zero : Bool → SNum
   | nz : NzsNum → SNum

diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -489,10 +489,12 @@ instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) where
 set_option backward.isDefEq.respectTransparency false in
 /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
 
+```
 Vᵢⱼ ⟶ Uᵢ
  |      |
  ↓      ↓
  Uⱼ ⟶ X
+```
 -/
 def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
   PullbackCone.isLimitAux' _ fun s => by
@@ -589,10 +591,12 @@ theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (
 
 /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
 
+```
 Vᵢⱼ ⟶ Uᵢ
  |      |
  ↓      ↓
  Uⱼ ⟶ X
+```
 -/
 def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
   𝖣.vPullbackConeIsLimitOfMap forgetToPresheafedSpace i j