diff --git a/LeanByExample/Declarative/Infix.lean b/LeanByExample/Declarative/Infix.lean
index 86334137..835dcdcc 100644
--- a/LeanByExample/Declarative/Infix.lean
+++ b/LeanByExample/Declarative/Infix.lean
@@ -57,9 +57,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
diff --git a/LeanByExample/Declarative/Postfix.lean b/LeanByExample/Declarative/Postfix.lean
index 304c9910..934ec844 100644
--- a/LeanByExample/Declarative/Postfix.lean
+++ b/LeanByExample/Declarative/Postfix.lean
@@ -28,9 +28,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
diff --git a/LeanByExample/Declarative/Prefix.lean b/LeanByExample/Declarative/Prefix.lean
index f652e38d..717cecf3 100644
--- a/LeanByExample/Declarative/Prefix.lean
+++ b/LeanByExample/Declarative/Prefix.lean
@@ -24,9 +24,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean
index b49aa854..a1e44c6b 100644
--- a/LeanByExample/Tactic/Exists.lean
+++ b/LeanByExample/Tactic/Exists.lean
@@ -8,7 +8,7 @@ import Lean --#
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
-/- ## 内部処理についての補足
+/- ## 舞台裏
 なお Lean での存在量化の定義は次のようになっています。-/
 --#--
 -- Exists の定義が変わっていないことを確認する
@@ -41,9 +41,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
diff --git a/LeanByExample/Tactic/ShowTerm.lean b/LeanByExample/Tactic/ShowTerm.lean
index 404f70b7..689675fc 100644
--- a/LeanByExample/Tactic/ShowTerm.lean
+++ b/LeanByExample/Tactic/ShowTerm.lean
@@ -32,9 +32,10 @@ open Lean in
 
 /-- マクロを展開するコマンド -/
 elab "#expand " t:macro_stx : command => do
-  let t : Syntax := match t.raw with
-  | .node _ _ #[t] => t
-  | _ => t.raw
+  let t : Syntax :=
+    match t.raw with
+    | .node _ _ #[t] => t
+    | _ => t.raw
   match ← Elab.liftMacroM <| Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"