diff --git a/Examples/Declarative/Section.lean b/Examples/Declarative/Section.lean
index d0fe4154..3872919e 100644
--- a/Examples/Declarative/Section.lean
+++ b/Examples/Declarative/Section.lean
@@ -75,7 +75,7 @@ section hoge
   #check a
 end hoge
 
-/-! セクションは入れ子にすることもできます。-/
+/- セクションは入れ子にすることもできます。-/
 
 section parent
   variable (a : Type)
diff --git a/Examples/Diagnostic/Check.lean b/Examples/Diagnostic/Check.lean
index 0e0d53e6..11cdf66b 100644
--- a/Examples/Diagnostic/Check.lean
+++ b/Examples/Diagnostic/Check.lean
@@ -37,7 +37,7 @@
 -- 命題
 #check True
 
-/-! ## 型の型
+/- ## 型の型
 「すべての」項には型があるので、型も型を持ちます。
 -/
 -- 宇宙変数を宣言する
@@ -59,7 +59,7 @@ universe u
 -- この調子で限りなく続く
 #check (Type u : Type (u + 1))
 
-/-! ## 命題と証明
+/- ## 命題と証明
 Lean では命題やその証明にも型があります。命題の型は `Prop` で、命題の項が証明になっています。逆に言えば、Lean ではある命題 `P : Prop` を証明するということは、`P` という型を持つ項 `proof : P` を構成することと同じです。
 -/
 
@@ -71,7 +71,7 @@ theorem two_eq_add_one : 2 = 1 + 1 := by rfl
 -- 証明の型が命題になっている
 #check (two_eq_add_one : 2 = 1 + 1)
 
-/-! ## 型としての True/False
+/- ## 型としての True/False
 `True` は型としては一点集合であり、
 `False` は型としては空集合です。
 -/
@@ -79,7 +79,7 @@ theorem two_eq_add_one : 2 = 1 + 1 := by rfl
 -- `trivial : True` は `True` 型を持つ項
 #check trivial
 
-/-! ## 関数としての証明
+/- ## 関数としての証明
 命題 `P → Q` の証明は、`P → Q` という型を持つ項です。
 つまり、`P` の証明 `h : P` に対して `Q` の証明を返す関数です。
 -/
diff --git a/Examples/Diagnostic/Eval.lean b/Examples/Diagnostic/Eval.lean
index 11b8f67e..e7ac0c1d 100644
--- a/Examples/Diagnostic/Eval.lean
+++ b/Examples/Diagnostic/Eval.lean
@@ -51,7 +51,7 @@ failed to be synthesized, this instance instructs Lean on how to display the res
 
 /- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 
-/-! ## 例外処理の慣例
+/- ## 例外処理の慣例
 Lean および Mathlib では、「関数ではなく定理に制約を付ける」ことが慣例です。
 関数の定義域を制限するアプローチだと、
 関数を呼び出すたびに、引数が定義域に含まれているか確認する必要が生じて、
diff --git a/Examples/Diagnostic/Find.lean b/Examples/Diagnostic/Find.lean
index ead85870..9f56bf79 100644
--- a/Examples/Diagnostic/Find.lean
+++ b/Examples/Diagnostic/Find.lean
@@ -1,4 +1,4 @@
-/-! # \#find
+/- # \#find
 
 `#find` はライブラリ検索を行うコマンドです。
 
diff --git a/Examples/Diagnostic/Guard.lean b/Examples/Diagnostic/Guard.lean
index dcc71dba..efeaa111 100644
--- a/Examples/Diagnostic/Guard.lean
+++ b/Examples/Diagnostic/Guard.lean
@@ -34,7 +34,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 #guard_msgs (whitespace := lax) in
 #guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
 
-/-! しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
+/- しかし、 `1 + 1 = 2` 等も `#check` で確かめてみると型は `Prop` です。にも関わらず `#guard` に渡してもエラーになりません。これは不思議に思えますが、理由は `1 + 1 = 2` が [`Decidable`](../TypeClass/Decidable.md) 型クラスのインスタンスであり、決定可能だからです。-/
 
 -- 型は Prop
 /-- info: 1 + 1 = 2 : Prop -/
@@ -45,7 +45,7 @@ error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains error
 -- 1 + 1 = 2 は決定可能
 #synth Decidable (1 + 1 = 2)
 
-/-!
+/-
 `Prop` 型であっても、`Decidable` クラスのインスタンスであれば `Bool` に変換できます。それを自動で行っているので、`Prop` 型の項でも `#guard` に通せるというわけです。
 -/
 
diff --git a/Examples/Diagnostic/Synth.lean b/Examples/Diagnostic/Synth.lean
index 7a86b583..21b15513 100644
--- a/Examples/Diagnostic/Synth.lean
+++ b/Examples/Diagnostic/Synth.lean
@@ -13,7 +13,7 @@ import Mathlib.Data.Real.Basic -- 実数 --#
 -- 実数として見ても同じ
 #check (1 : ℝ)⁻¹
 
-/-! 逆数をとる関数 `fun x => x⁻¹` の定義域はどうなっているのでしょうか？定義域を一般の型 `α` に拡張してみて、どうなるか見てみましょう。-/
+/- 逆数をとる関数 `fun x => x⁻¹` の定義域はどうなっているのでしょうか？定義域を一般の型 `α` に拡張してみて、どうなるか見てみましょう。-/
 
 variable (α : Type)
 
@@ -24,16 +24,16 @@ Additional diagnostic information may be available using the `set_option diagnos
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
-/-! 一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで `α` は `Inv` のインスタンスではないと言われています。この `Inv` が型クラスです。`Inv` のインスタンスであるような型 `T` に対しては、逆数関数 `(·)⁻¹ : T → T` が定義できるというわけです。-/
+/- 一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで `α` は `Inv` のインスタンスではないと言われています。この `Inv` が型クラスです。`Inv` のインスタンスであるような型 `T` に対しては、逆数関数 `(·)⁻¹ : T → T` が定義できるというわけです。-/
 
-/-! ## インスタンスとは
+/- ## インスタンスとは
 例えば実数 `ℝ` に対して逆数は定義できるだろうと予想されますが、実際 `ℝ` は `Inv` のインスタンスであることが確認できます。
 -/
 
 /-- info: Real.instInv -/
 #guard_msgs in #synth Inv Real
 
-/-! 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
+/- 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
 
 -- エラーになってしまう
 /--
@@ -47,7 +47,7 @@ Additional diagnostic information may be available using the `set_option diagnos
 #guard_msgs (drop warning) in --#
 #check_failure (inferInstance : Inv Nat)
 
-/-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
+/- 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
 
 instance : Inv Nat := ⟨fun _ => 1⟩
 
diff --git a/Examples/Tactic/AllGoals.lean b/Examples/Tactic/AllGoals.lean
index 00870634..90154e5b 100644
--- a/Examples/Tactic/AllGoals.lean
+++ b/Examples/Tactic/AllGoals.lean
@@ -12,7 +12,7 @@ example (hP : P) (hQ : Q) : P ∧ Q := by
   -- 両方に `assumption` を適用する
   all_goals assumption
 
-/-! `all_goals` には、タクティクブロックを渡すこともできます。-/
+/- `all_goals` には、タクティクブロックを渡すこともできます。-/
 
 example {R : Prop} (hnP : ¬ P) : (P → R) ∧ (P → Q) := by
   constructor
diff --git a/Examples/Tactic/Apply.lean b/Examples/Tactic/Apply.lean
index aed334f2..4a673880 100644
--- a/Examples/Tactic/Apply.lean
+++ b/Examples/Tactic/Apply.lean
@@ -15,7 +15,7 @@ example (h : P → Q) (hP : P) : Q := by
 
   exact hP
 
-/-! 注意点として、`h : P → Q` は `P` の証明を受け取って `Q` の証明を返す関数でもあるので、上記の例は `apply` を使わずに `exact h hP` で閉じることもできます。-/
+/- 注意点として、`h : P → Q` は `P` の証明を受け取って `Q` の証明を返す関数でもあるので、上記の例は `apply` を使わずに `exact h hP` で閉じることもできます。-/
 
 example (h : P → Q) (hP : P) : Q := by
   exact h hP
diff --git a/Examples/Tactic/ApplyAssumption.lean b/Examples/Tactic/ApplyAssumption.lean
index 4a78ba30..8f64f545 100644
--- a/Examples/Tactic/ApplyAssumption.lean
+++ b/Examples/Tactic/ApplyAssumption.lean
@@ -23,7 +23,7 @@ example (hPQ : P → Q) : ¬ Q → ¬ P := by
   -- 証明終わり
   done
 
-/-! タクティクを繰り返すことを指示するタクティク [`repeat`](./Repeat.md) と組み合わせると、「ローカルコンテキストにある仮定を適切に選んで `apply`, `exact` することを繰り返し、ゴールを閉じる」ことができます。
+/- タクティクを繰り返すことを指示するタクティク [`repeat`](./Repeat.md) と組み合わせると、「ローカルコンテキストにある仮定を適切に選んで `apply`, `exact` することを繰り返し、ゴールを閉じる」ことができます。
 -/
 
 example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
diff --git a/Examples/Tactic/ApplyAt.lean b/Examples/Tactic/ApplyAt.lean
index 5bb3a41f..abea5e04 100644
--- a/Examples/Tactic/ApplyAt.lean
+++ b/Examples/Tactic/ApplyAt.lean
@@ -17,7 +17,7 @@ example (h : P → Q) (hP : P) : Q := by
 
   assumption
 
-/-! 便利な記法以上のものではなく、他のタクティクを利用しても同じことができます。-/
+/- 便利な記法以上のものではなく、他のタクティクを利用しても同じことができます。-/
 
 example (h : P → Q) (hP : P) : Q := by
   -- `apply at` は `replace` と同じように動作する
diff --git a/Examples/Tactic/ApplyQuestion.lean b/Examples/Tactic/ApplyQuestion.lean
index 06af5f9d..ef449aa6 100644
--- a/Examples/Tactic/ApplyQuestion.lean
+++ b/Examples/Tactic/ApplyQuestion.lean
@@ -15,7 +15,7 @@ example [Group G] [Group H] (f : G →* H) (a b : G) :
   -- `exact MonoidHom.map_mul f a b` を提案してくれる
   apply? says exact MonoidHom.map_mul f a b
 
-/-!
+/-
 ## 補足
 
 `apply?` はあくまで証明を書くときに補助として使うものです。
diff --git a/Examples/Tactic/Assumption.lean b/Examples/Tactic/Assumption.lean
index af55979d..32d8034e 100644
--- a/Examples/Tactic/Assumption.lean
+++ b/Examples/Tactic/Assumption.lean
@@ -1,4 +1,4 @@
-/-! # assumption
+/- # assumption
 
 `assumption` は、現在のゴール `⊢ P` がローカルコンテキストにあるとき、ゴールを閉じます。-/
 
diff --git a/Examples/Tactic/By.lean b/Examples/Tactic/By.lean
index ba39300e..4904efa6 100644
--- a/Examples/Tactic/By.lean
+++ b/Examples/Tactic/By.lean
@@ -2,7 +2,7 @@
 
 Lean においては、命題は型で、証明はその項です。命題 `P` の証明を構成するとは項 `h : P` を構成するということです。`by` は、証明の構成をタクティクで行いたいときに使います。-/
 
-/-! 証明項による証明とは、たとえば次のようなものです。 -/
+/- 証明項による証明とは、たとえば次のようなものです。 -/
 
 variable (P Q R : Prop)
 
@@ -11,14 +11,14 @@ variable (P Q R : Prop)
 example (hPQ : P → Q) (hQR : Q → R) : P → R :=
   fun hP ↦ hQR (hPQ hP)
 
-/-! 同じ命題をタクティクを使って示すと、例えば次のようになります。 -/
+/- 同じ命題をタクティクを使って示すと、例えば次のようになります。 -/
 
 -- 同じ命題をタクティクで示した例
 example (hPQ : P → Q) (hQR : Q → R) : P → R := by
   intro hP
   exact hQR (hPQ hP)
 
-/-! ## by?
+/- ## by?
 
 `by` の代わりに `by?` を使うとタクティクモードで構成した証明を直接構成した証明に変換してくれます。`show_term by` としてもほぼ同じ結果が得られます。
 -/
diff --git a/Examples/Tactic/Cases.lean b/Examples/Tactic/Cases.lean
index fb4fdc82..bbff3f1e 100644
--- a/Examples/Tactic/Cases.lean
+++ b/Examples/Tactic/Cases.lean
@@ -25,7 +25,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
   case inr hQ =>
     exact hQR hQ
 
-/-! ## with を使う書き方
+/- ## with を使う書き方
 
 `case` を使わずに、`with` を使って次のように書くこともできます
 -/
diff --git a/Examples/Tactic/Congr.lean b/Examples/Tactic/Congr.lean
index 007ab7ee..96974be7 100644
--- a/Examples/Tactic/Congr.lean
+++ b/Examples/Tactic/Congr.lean
@@ -30,7 +30,7 @@ example (h : a < b) : a + 1 < b + 1 := by
 
   exact Int.add_lt_add_right h 1
 
-/-! ## 再帰の深さの調節
+/- ## 再帰の深さの調節
 
 `congr` が適用される再帰の深さを引数として渡すことができます。これは、主に単に `congr` とするだけだと「行き過ぎ」になるときに調整する目的で使用されます。-/
 set_option linter.unusedTactic false in --#
diff --git a/Examples/Tactic/Exact.lean b/Examples/Tactic/Exact.lean
index 536e34e2..dab330fe 100644
--- a/Examples/Tactic/Exact.lean
+++ b/Examples/Tactic/Exact.lean
@@ -9,7 +9,7 @@ example (hP : P) (hQ : Q) : P := by
 
   exact hP
 
-/-! `exact` は与えられた証明項をそのまま証明として使うタクティクなので、`by exact` だけで証明が終わるときには、`by exact` を消しても証明が通ります。-/
+/- `exact` は与えられた証明項をそのまま証明として使うタクティクなので、`by exact` だけで証明が終わるときには、`by exact` を消しても証明が通ります。-/
 
 example (hP : P) (hQ : Q) : P ∧ Q := by
   exact And.intro hP hQ
diff --git a/Examples/Tactic/ExactQuestion.lean b/Examples/Tactic/ExactQuestion.lean
index e27102d2..a8b91277 100644
--- a/Examples/Tactic/ExactQuestion.lean
+++ b/Examples/Tactic/ExactQuestion.lean
@@ -32,7 +32,7 @@ example (_h1 : P) (h2 : P) : P := by
   exact? using h2 says
     exact h2
 
-/-!
+/-
 ## exact? を使用する際のコツ
 
 これは `exact?` に限らず、Lean でライブラリ検索を行うとき常に意識した方が良いことですが、
diff --git a/Examples/Tactic/FieldSimp.lean b/Examples/Tactic/FieldSimp.lean
index e48fcd15..9d609d10 100644
--- a/Examples/Tactic/FieldSimp.lean
+++ b/Examples/Tactic/FieldSimp.lean
@@ -13,7 +13,7 @@ example (n m : Rat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
   -- Rat は可換環なので、 示すべきことが言える
   ring
 
-/-! 分母がゼロでないことが判らない場合は動作しません。分母がゼロでないことを証明してローカルコンテキストに加えると動作することがあります。-/
+/- 分母がゼロでないことが判らない場合は動作しません。分母がゼロでないことを証明してローカルコンテキストに加えると動作することがあります。-/
 
 example {x y z : Rat} (hy : y = z ^ 2 + 1) : (x + 2 * y) / y = x / y + 2 := by
   -- 最初 `field_simp` は動作しない
@@ -27,7 +27,7 @@ example {x y z : Rat} (hy : y = z ^ 2 + 1) : (x + 2 * y) / y = x / y + 2 := by
   -- 動作するようになった
   field_simp
 
-/-! ## 制約
+/- ## 制約
 `field_simp` という名前の通り、割り算が体の割り算でなければ動作しません。たとえば 自然数 `Nat` における割り算は `field_simp` では扱うことができず、次のコード例のように工夫する必要があります。-/
 
 example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
diff --git a/Examples/Tactic/Gcongr.lean b/Examples/Tactic/Gcongr.lean
index 2cea95ae..fd2f4f51 100644
--- a/Examples/Tactic/Gcongr.lean
+++ b/Examples/Tactic/Gcongr.lean
@@ -43,7 +43,7 @@ example {c d : ℝ} (h : a + c + 1 ≤ b + d + 1) :
 
   linarith
 
-/-! ## 補題の登録
+/- ## 補題の登録
 さらに `[gcongr]` 属性を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
 
 variable {U : Type*}
diff --git a/Examples/Tactic/Have.lean b/Examples/Tactic/Have.lean
index 34221e54..fef4d1d6 100644
--- a/Examples/Tactic/Have.lean
+++ b/Examples/Tactic/Have.lean
@@ -17,7 +17,7 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
   -- 仮定 `hQR : Q → R` と `hQ : Q` から `R` が導かれる
   exact hQR hQ
 
-/-! `have` で示した補題には必ず名前がつきます。名前を省略して `have : P := ...` とすると、自動的に `this` という名前になります。無名の補題が欲しい場合、代わりに `show` を検討してみてください。
+/- `have` で示した補題には必ず名前がつきます。名前を省略して `have : P := ...` とすると、自動的に `this` という名前になります。無名の補題が欲しい場合、代わりに `show` を検討してみてください。
 
 また `have` で同じ名前を2回宣言すると、古い方はアクセス不能になってしまいます。ローカルコンテキストの補題の置き換えを行いたいときは、代わりに `replace` を使用してください。 -/
 
@@ -44,7 +44,7 @@ example (hPQ : P ∧ Q) : P := by
 
   assumption
 
-/-! ### 存在 ∃
+/- ### 存在 ∃
 
 次のように、`∃ x: X, P x` という命題から、条件を満たす `x` を取り出すことができます。`x : X` と `hx : P x` がローカルコンテキストに追加されます。 -/
 
diff --git a/Examples/Tactic/Hint.lean b/Examples/Tactic/Hint.lean
index 1b3a4b20..c4e67c0e 100644
--- a/Examples/Tactic/Hint.lean
+++ b/Examples/Tactic/Hint.lean
@@ -66,7 +66,7 @@ info: Try these:
 example : Nat.Prime 37 := by
   hint
 
-/-!
+/-
 ## タクティクの新規登録
 
 登録されているタクティクに `tac` を追加するには、`register_hint tac` を実行します。
diff --git a/Examples/Tactic/Induction.lean b/Examples/Tactic/Induction.lean
index 33279425..03683201 100644
--- a/Examples/Tactic/Induction.lean
+++ b/Examples/Tactic/Induction.lean
@@ -35,7 +35,7 @@ example (n : Nat) : sum n = n * (n + 1) / 2 := by
     -- 後は可換環の性質から示せる
     ring
 
-/-! ## 再帰定理
+/- ## 再帰定理
 Lean では、実は帰納法を使用するのに必ずしも `induction` は必要ありません。場合分けの中で示されたケースを帰納法の仮定として使うことができます。これは recursive theorem(再帰定理) と呼ばれることがあります。[^recursive]
 -/
 
@@ -70,7 +70,7 @@ theorem sample : True := by
       sorry
   trivial
 
-/-!
+/-
 ## 完全帰納法
 
 時には、 より強い帰納法が必要なこともあります。 強い帰納法とは、 たとえば
@@ -129,7 +129,7 @@ example (n : Nat) : fibonacci n = fib n := by
       -- 帰納法の仮定を適用して示す
       simp [ih_n, ih_succ]
 
-/-! なお、完全帰納法も `induction` タクティクを使わずに行うことができます。-/
+/- なお、完全帰納法も `induction` タクティクを使わずに行うことができます。-/
 
 /-- `fibonacci` と `fib` は同じ結果を返す -/
 theorem fib_eq (n : Nat) : fibonacci n = fib n := by
diff --git a/Examples/Tactic/InductionAp.lean b/Examples/Tactic/InductionAp.lean
index c9fe2900..14340a3b 100644
--- a/Examples/Tactic/InductionAp.lean
+++ b/Examples/Tactic/InductionAp.lean
@@ -30,7 +30,7 @@ example (n : Nat) : sum n = n * (n + 1) / 2 := by
     -- 後は可換環の性質から示せる
     ring
 
-/-!
+/-
 ## 完全帰納法
 
 時には、 より強い帰納法が必要なこともあります。 強い帰納法とは、 たとえば
diff --git a/Examples/Tactic/Intro.lean b/Examples/Tactic/Intro.lean
index b6826341..a8be1eec 100644
--- a/Examples/Tactic/Intro.lean
+++ b/Examples/Tactic/Intro.lean
@@ -97,7 +97,7 @@ example (P Q : Nat → Prop) (h : ∀ n, P n ↔ Q n) : ∀ y, P (y + 1) → Q (
   -- 仮定 `P (y + 1)` より従う
   assumption
 
-/-! ## 否定 ¬ について
+/- ## 否定 ¬ について
 
 Lean では否定 `¬ P` は `P → False` として定義されているので、ゴールが `¬ P` のときに `intro` すると `P` が仮定に追加されて、ゴールが `False` に変わります。
 
@@ -118,7 +118,7 @@ example (h: P → Q) : ¬Q → ¬P := by
   -- `hQ : Q` と `hnQ : ¬Q` から矛盾が導かれる
   contradiction
 
-/-!
+/-
 ## 関数の構成
 
 より一般的には、`intro` は関数の構成に使うことができます。
diff --git a/Examples/Tactic/Left.lean b/Examples/Tactic/Left.lean
index 6f591deb..236adc82 100644
--- a/Examples/Tactic/Left.lean
+++ b/Examples/Tactic/Left.lean
@@ -11,7 +11,7 @@ example (hP : P) : P ∨ Q := by
 
   assumption
 
-/-! ## left, right を使わない方法
+/- ## left, right を使わない方法
 
 以下に示すように、`Or.inl` は `a` から `a ∨ b` を得る関数です。また `Or.inr` は `b` から `a ∨ b` を得る関数です。これを使うことで `left` や `right` を使わずに証明できます。
 -/
diff --git a/Examples/Tactic/Linarith.lean b/Examples/Tactic/Linarith.lean
index 2f8a78d8..771e6975 100644
--- a/Examples/Tactic/Linarith.lean
+++ b/Examples/Tactic/Linarith.lean
@@ -13,7 +13,7 @@ example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
     12 * y - 4 * z ≥ 0 := by
   linarith
 
-/-! `linarith` はローカルコンテキストにある命題を読むので、`linarith` が通らないとき、追加で補題を示すことで解決することがあります。-/
+/- `linarith` はローカルコンテキストにある命題を読むので、`linarith` が通らないとき、追加で補題を示すことで解決することがあります。-/
 
 example : id x ≤ x := by
   -- `linarith` で示すことはできない
@@ -47,7 +47,7 @@ example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
   linarith
 
 end --#
-/-! ## linarith と他のタクティクの使い分け
+/- ## linarith と他のタクティクの使い分け
 `1 < 2` のような簡単な数値のみの不等式の場合、`norm_num` や `simp_arith` でも証明ができます。
 同じ命題を示すのに複数のコマンドがあるわけですが、コマンド実行にかかる時間に違いがあります。
 
diff --git a/Examples/Tactic/Omega.lean b/Examples/Tactic/Omega.lean
index 4f9f9c14..a18d6532 100644
--- a/Examples/Tactic/Omega.lean
+++ b/Examples/Tactic/Omega.lean
@@ -23,7 +23,7 @@ example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
   -- `omega` では示せる
   omega
 
-/-! Lean では自然数同士の引き算は整数同士の引き算とは異なる結果になって厄介なのですが、`omega` はこの問題を上手く処理します。 たとえば、以下は `linarith` では示すことができない線形な命題です。-/
+/- Lean では自然数同士の引き算は整数同士の引き算とは異なる結果になって厄介なのですが、`omega` はこの問題を上手く処理します。 たとえば、以下は `linarith` では示すことができない線形な命題です。-/
 
 variable (a b : Nat)
 
@@ -46,7 +46,7 @@ example : (a - b) - b = a - 2 * b := by
   fail_if_success linarith
   omega
 
-/-! `omega` は整数や自然数の整除関係を扱うこともできます。-/
+/- `omega` は整数や自然数の整除関係を扱うこともできます。-/
 
 example {a b c : ℤ} : 3 ∣ (100 * c + 10 * b + a) ↔ 3 ∣ (c + b + a) := by omega
 
diff --git a/Examples/Tactic/PushNeg.lean b/Examples/Tactic/PushNeg.lean
index 54aed914..c13d8c05 100644
--- a/Examples/Tactic/PushNeg.lean
+++ b/Examples/Tactic/PushNeg.lean
@@ -20,7 +20,7 @@ example (h: P → Q) : ¬ (P ∧ ¬ Q) := by
 
   exact h
 
-/-! 以下の例は、「酔っぱらいのパラドクス」として有名な命題です。 -/
+/- 以下の例は、「酔っぱらいのパラドクス」として有名な命題です。 -/
 
 -- `People` という空ではない集合がある
 variable {People : Type} [Inhabited People]
@@ -51,7 +51,7 @@ example : ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := b
     exists x
     simp_all
 
-/-!
+/-
 ## use_distrib
 
 option で `push_neg.use_distrib` を `true` にすると、`¬ (p ∧ q)` を `¬ p ∨ ¬ q` に変形します。
diff --git a/Examples/Tactic/Refine.lean b/Examples/Tactic/Refine.lean
index a8d357a4..f9900b02 100644
--- a/Examples/Tactic/Refine.lean
+++ b/Examples/Tactic/Refine.lean
@@ -12,7 +12,7 @@ example (hP: P) (hQ: Q) : P ∧ Q := by
 
   exact hP
 
-/-! ## constructor との関連
+/- ## constructor との関連
 
 `refine` は [`constructor`](./Constructor.md) の代わりに使うこともできます。実際 `refine` は `constructor` よりも柔軟で、`⊢ P ∧ Q ∧ R` のような形のゴールは `constructor` よりも簡潔に分割できます。-/
 
@@ -27,7 +27,7 @@ example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
   · show R
     exact hR
 
-/-! `constructor` を使った場合、一度に２つのゴールに分割することしかできません。 -/
+/- `constructor` を使った場合、一度に２つのゴールに分割することしかできません。 -/
 
 example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
   constructor
@@ -40,7 +40,7 @@ example (hP: P) (hQ: Q) (hR : R) : P ∧ Q ∧ R := by
     · show R
       exact hR
 
-/-! ## apply との関連
+/- ## apply との関連
 
 `h : P → Q` という命題があって、ゴールが `⊢ Q` であるとき `refine h ?_` は `apply h` と同様に機能するので、`refine` で [`apply`](./Apply.md) を代用することができます。 -/
 
diff --git a/Examples/Tactic/Rel.lean b/Examples/Tactic/Rel.lean
index 571d68a7..3cdbe9c7 100644
--- a/Examples/Tactic/Rel.lean
+++ b/Examples/Tactic/Rel.lean
@@ -10,13 +10,13 @@ variable (a b c d: Nat)
 example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
   rel [h1, h2]
 
-/-! 下記で示すように、ゴールが関係式でないときにはエラーになります。-/
+/- 下記で示すように、ゴールが関係式でないときにはエラーになります。-/
 
 /-- error: rel failed, goal not a relation -/
 #guard_msgs in
 example (x : Nat) : Nat := by rel [x]
 
-/-! なお、基本的に `rel` よりも [`gcongr`](./Gcongr.md) の方が強いタクティクです。`gcongr` は `rel` とは異なり、ローカルコンテキストから必要な命題を自動的に読み込むことができます。
+/- なお、基本的に `rel` よりも [`gcongr`](./Gcongr.md) の方が強いタクティクです。`gcongr` は `rel` とは異なり、ローカルコンテキストから必要な命題を自動的に読み込むことができます。
 -/
 
 example (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by
diff --git a/Examples/Tactic/Rfl.lean b/Examples/Tactic/Rfl.lean
index a0db36eb..3d7283c0 100644
--- a/Examples/Tactic/Rfl.lean
+++ b/Examples/Tactic/Rfl.lean
@@ -23,7 +23,7 @@ attribute [refl] MyEq.refl
 -- `rfl` で示せるようになる
 example (n : ℕ) : MyEq n n := by rfl
 
-/-! 適宜ライブラリが必要ですが、不等式 `≤` の反射性も登録されているので `rfl` で示すことができます。-/
+/- 適宜ライブラリが必要ですが、不等式 `≤` の反射性も登録されているので `rfl` で示すことができます。-/
 
 example (n : ℕ) : n ≤ n := by rfl
 
diff --git a/Examples/Tactic/Right.lean b/Examples/Tactic/Right.lean
index eb6e5212..ea562138 100644
--- a/Examples/Tactic/Right.lean
+++ b/Examples/Tactic/Right.lean
@@ -10,7 +10,7 @@ example (hQ : Q) : P ∨ Q := by
 
   assumption
 
-/-! ## left, right を使わない方法
+/- ## left, right を使わない方法
 
 以下に示すように、`Or.inl` は `a` から `a ∨ b` を得る関数です。また `Or.inr` は `b` から `a ∨ b` を得る関数です。これを使うことで `left` や `right` を使わずに証明できます。
 -/
diff --git a/Examples/Tactic/Ring.lean b/Examples/Tactic/Ring.lean
index 13f3c61a..a956a1af 100644
--- a/Examples/Tactic/Ring.lean
+++ b/Examples/Tactic/Ring.lean
@@ -17,7 +17,7 @@ example (hz : z = x + y) : x * z = x ^ 2 + x * y := by
   rw [hz]
   ring
 
-/-! ## ring_nf
+/- ## ring_nf
 `ring` は等式を示そうとするタクティクですが、`ring_nf` は式を整理して標準形と呼ばれる形にします。
 -/
 example {x y z : Rat} (h : z = (x + y) ^ 2) : z = x ^ 2 + 2 * x * y + y ^ 2 := by
@@ -30,7 +30,7 @@ example {x y z : Rat} (h : z = (x + y) ^ 2) : z = x ^ 2 + 2 * x * y + y ^ 2 := b
   -- 後は可換環の公理から示せる
   ring
 
-/-! ## 環でないものに ring を使ったら
+/- ## 環でないものに ring を使ったら
 
 たとえば自然数 `ℕ` は環ではありません。そのため、自然数の引き算などを含む式は多くの場合 `ring` では示せません。代わりに `ring_nf` を使うように促されますが、`ring_nf` でも示せるとは限りません。
 -/
@@ -57,7 +57,7 @@ example {n : Nat} : n - n + n = n := by
 
   simp
 
-/-! ## ring の中身を見る方法
+/- ## ring の中身を見る方法
 
 `simp` 等と異なり、`ring?` タクティクは用意されていませんが、`show_term` で具体的にどんなルールが適用されたのかを知ることができます。
 ただし、その出力結果は非常に長く読みづらいものであることがしばしばです。
diff --git a/Examples/Tactic/RwSearch.lean b/Examples/Tactic/RwSearch.lean
index c99d04cc..2e42b6e4 100644
--- a/Examples/Tactic/RwSearch.lean
+++ b/Examples/Tactic/RwSearch.lean
@@ -33,7 +33,7 @@ example (h : n + m = 0) : n = 0 ↔ m = 0 := by
   rw_search says
     rw [propext (eq_zero_iff_eq_zero_of_add_eq_zero h)]
 
-/-! ## rw?
+/- ## rw?
 `rw?` は `apply?` のように、ゴールを `rw` できる補題をライブラリから検索します。`rw?` は等式以外も扱うことができますが、`rw_search` と同様に同値関係の扱いは苦手です。-/
 set_option linter.unusedTactic false in --#
 
diff --git a/Examples/Tactic/Says.lean b/Examples/Tactic/Says.lean
index f5b1478d..3f846279 100644
--- a/Examples/Tactic/Says.lean
+++ b/Examples/Tactic/Says.lean
@@ -22,7 +22,7 @@ example (hPQ : P → Q) (hQR : Q → R) (hRS : R → S) (hP : P) : S := by
   exact? says
     exact hRS (hQR (hPQ hP))
 
-/-! [`simp`](./Simp.md) や [`aesop`](./Aesop.md) のような証明自動化系のタクティクに対して、動作を軽量化しながらも証明の読みやすさを保つという目的でも使用できます。たとえば `aesop? says ...` と書かれていたら、その後のブロックでどんな複雑なことが書かれていようと、単に `aesop` の発見した証明内容を丁寧に書いているだけだとわかるわけです。-/
+/- [`simp`](./Simp.md) や [`aesop`](./Aesop.md) のような証明自動化系のタクティクに対して、動作を軽量化しながらも証明の読みやすさを保つという目的でも使用できます。たとえば `aesop? says ...` と書かれていたら、その後のブロックでどんな複雑なことが書かれていようと、単に `aesop` の発見した証明内容を丁寧に書いているだけだとわかるわけです。-/
 
 -- 以下 `X` `Y` `Z`を集合とする
 variable {X Y Z : Type}
@@ -37,7 +37,7 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
     apply hgfinj
     simp_all only [comp_apply]
 
-/-! ## オプション
+/- ## オプション
 
 `says.no_verify_in_CI : Bool` : `true` にすると、CI 環境で `X says Y` の `Y` の部分が実際に提案されている内容と一致するかのチェックが走らなくなります。-/
 
diff --git a/Examples/Tactic/Show.lean b/Examples/Tactic/Show.lean
index 665d9ec7..f1cae647 100644
--- a/Examples/Tactic/Show.lean
+++ b/Examples/Tactic/Show.lean
@@ -20,7 +20,7 @@ example (f : ℚ → ℕ) : f ((a + b) ^ 2) = f (a ^ 2 + 2 * a * b + b ^ 2) := b
   -- `show ... from` で無名の証明を構成してそれを `rw` に渡すことができる
   rw [show (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 from by ring]
 
-/-! この話は `show` と直接関係はありませんが、証明項のところに、頭に `?` をつけた変数(メタ変数)を配置すると、証明を後回しにすることができます。 -/
+/- この話は `show` と直接関係はありませんが、証明項のところに、頭に `?` をつけた変数(メタ変数)を配置すると、証明を後回しにすることができます。 -/
 
 example (h : a * x < b) (ha : a > 0) : x < b / a := by
   -- `b / a` を `r` とおく
@@ -39,7 +39,7 @@ example (h : a * x < b) (ha : a > 0) : x < b / a := by
     -- 分母を払う
     field_simp
 
-/-!
+/-
 ## ゴールの状態を確認する
 
 `show` 単独で使った場合、ゴールが特定の命題に等しいかどうかチェックします。`show P` は、ゴールの中に `⊢ P` (に定義上等しい命題)が存在しないときにエラーになり、存在すればそれをメインのゴールにします。たとえば、証明中にこれから示すべきことを明示し、コードを読みやすくする目的で使うことができます。
diff --git a/Examples/Tactic/Simp.lean b/Examples/Tactic/Simp.lean
index d740707c..9e1bfe84 100644
--- a/Examples/Tactic/Simp.lean
+++ b/Examples/Tactic/Simp.lean
@@ -64,7 +64,7 @@ use `set_option diagnostics true` to get diagnostic information
 example (n m : Nat) : (n + 0) * m = n * m := by simp
 
 end
-/-! ## simp で使用できる構文
+/- ## simp で使用できる構文
 
 既知の `h : P` という命題を使って単純化させたいときは、明示的に `simp [h]` と指定することで可能です。複数個指定することもできます。また `simp only [h₁, ... , hₖ]` とすると `h₁, ... , hₖ` だけを使用して単純化を行います。-/
 
@@ -72,7 +72,7 @@ example (h : R) : (P ∨ Q ∨ R) ∧ R := by
   simp only [or_and]
   assumption
 
-/-! 単に名前を定義に展開したい場合は [`dsimp`](./Dsimp.md) を使用します。
+/- 単に名前を定義に展開したい場合は [`dsimp`](./Dsimp.md) を使用します。
 `simp` は何も指定しなければゴールを単純化しますが、ローカルコンテキストにある `h : P` を単純化させたければ `simp at h` と指定することで可能です。ゴールと `h` の両方を単純化したいときは `simp at h ⊢` とします。-/
 
 variable {n m : Nat}
@@ -83,7 +83,7 @@ example (h : n + 0 + 0 = m) : n = m + (0 * n) := by
 
 /- ローカルコンテキストとゴールをまとめて全部単純化したい場合は `simp at *` とします。 -/
 
-/-! ## simpa
+/- ## simpa
 `simpa` は、`simp` を実行した後 `assumption` を実行するという一連の流れを一つのタクティクにしたものです。`simpa at h` 構文は存在せず、`simpa using h` と書くことに注意してください。-/
 
 example (h : R) : (P ∨ Q ∨ R) ∧ R := by
@@ -92,7 +92,7 @@ example (h : R) : (P ∨ Q ∨ R) ∧ R := by
 example (h : n + 0 + 0 = m) : n = m := by
   simpa using h
 
-/-! ## simp?
+/- ## simp?
 
 `simp` は自動的に証明を行ってくれますが、何が使われたのか知りたいときもあります。`simp?` は単純化に何が使われたのかを示してくれるので、`simp only` などを用いて明示的に書き直すことができます。-/
 
@@ -100,7 +100,7 @@ example : (P ∨ Q ∨ R) ∧ R ↔ R := by
   simp? says
     simp only [or_and]
 
-/-! ## simp_arith
+/- ## simp_arith
 `simp` の設定で `arith` を有効にすると、算術的な単純化もできるようになります。
 これはよく使用されるので、`simp_arith` という省略形が用意されています。
 -/
diff --git a/Examples/Tactic/SlimCheck.lean b/Examples/Tactic/SlimCheck.lean
index 905a5861..df98e24f 100644
--- a/Examples/Tactic/SlimCheck.lean
+++ b/Examples/Tactic/SlimCheck.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.SlimCheck
 variable (a b : ℕ)
 
 #guard_msgs (drop warning) in --#
-example (h : 2 ≤ a + b) : 1 ≤ a := by
+example (h : 0 ≤ a + b) : 1 ≤ a := by
   /-
   Found problems! というエラーが表示される
   -/
@@ -14,7 +14,7 @@ example (h : 2 ≤ a + b) : 1 ≤ a := by
 
   sorry
 
-/-!
+/-
 ## 反例が見つからない時
 
 100 個のテストケースでテストしてOKならエラーにならないのですが、途中でギブアップした場合はエラーになります。-/
diff --git a/Examples/Tactic/Split.lean b/Examples/Tactic/Split.lean
index 0b5dc388..09290f46 100644
--- a/Examples/Tactic/Split.lean
+++ b/Examples/Tactic/Split.lean
@@ -54,7 +54,7 @@ example (x : Int) : myabs (2 * x) = 2 * myabs x := by
     -- `simp` で単純化
     simp [h, hx]
 
-/-! ## match 式と split
+/- ## match 式と split
 `if` 式だけでなく `match` 式に対しても使うことができます。
 -/
 
diff --git a/Examples/Tactic/Tauto.lean b/Examples/Tactic/Tauto.lean
index 9995e33e..4049089c 100644
--- a/Examples/Tactic/Tauto.lean
+++ b/Examples/Tactic/Tauto.lean
@@ -20,7 +20,7 @@ example : (P → (Q → R)) → ((P → Q) → (P → R)) := by
 example : (P ↔ ¬ P) → false := by
   tauto
 
-/-! `tauto` はすべてのトートロジーを示せるわけではありません。ごく簡単なトートロジーの中にも `tauto` で示せないものがあります。-/
+/- `tauto` はすべてのトートロジーを示せるわけではありません。ごく簡単なトートロジーの中にも `tauto` で示せないものがあります。-/
 
 variable (α : Type) (S : α → Prop)