diff --git a/Examples/Command/Attribute/AppUnexpander.lean b/Examples/Command/Attribute/AppUnexpander.lean
index d265eb87..001865ab 100644
--- a/Examples/Command/Attribute/AppUnexpander.lean
+++ b/Examples/Command/Attribute/AppUnexpander.lean
@@ -1,5 +1,5 @@
 /- # app_unexpander
-`app_unexpander` 属性を付与すると、関数適用 `f a₁ a₂ ... aₙ` の `#check` コマンドおよび infoview での表示のされ方を変更することができます。
+`[app_unexpander]` 属性を付与すると、関数適用 `f a₁ a₂ ... aₙ` の `#check` コマンドおよび infoview での表示のされ方を変更することができます。
 -/
 namespace AppUnexpander --#
 
diff --git a/Examples/Command/Attribute/CasesEliminator.lean b/Examples/Command/Attribute/CasesEliminator.lean
index c746941c..7f01653a 100644
--- a/Examples/Command/Attribute/CasesEliminator.lean
+++ b/Examples/Command/Attribute/CasesEliminator.lean
@@ -1,8 +1,8 @@
 /- # cases_eliminator
 
-`cases_eliminator` 属性は、[`cases`](../../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
+`[cases_eliminator]` 属性は、[`cases`](../../Tactic/Cases.md) タクティクで場合分けをした際の枝を変更します。
 
-より詳しくいうと、[`cases`](../../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`cases_eliminator` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`cases`](../../Tactic/Cases.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.casesOn` という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[cases_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace CasesEliminator --#
 
@@ -35,7 +35,7 @@ info: CasesEliminator.Many.casesOn.{u} {α : Type} {motive : Many α → Sort u}
 #guard_msgs (whitespace := lax) in #check Many.casesOn
 
 /-- Many.casesOn の more を cons に置き換えたバージョン。
-この定理に `cases_eliminator` 属性を与えることで、
+この定理に `[cases_eliminator]` 属性を与えることで、
 `casesOn` の代わりにこれがデフォルトで使われるようになる。 -/
 @[cases_eliminator]
 protected def Many.cons_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
diff --git a/Examples/Command/Attribute/Csimp.lean b/Examples/Command/Attribute/Csimp.lean
index 8b1613f7..698425bc 100644
--- a/Examples/Command/Attribute/Csimp.lean
+++ b/Examples/Command/Attribute/Csimp.lean
@@ -1,5 +1,5 @@
 /- # csimp
-`csimp` は、コンパイラに単純化を指示する属性です。
+`[csimp]` 属性は、コンパイラに単純化を指示します。
 
 `A = B` という形の定理に付与することでコンパイラに `A` の計算を `B` の計算に置き換えさせることができます。非効率な関数を効率的な実装に置き換えるために使用されます。
 -/
@@ -44,7 +44,7 @@ where
 theorem fib_add (n : Nat) : fib (n + 2) = fib n + fib (n + 1) := by rfl
 
 /-- `fibonacci` と `fib` は同じ結果を返す。
-`csimp` 属性を与えることで、`fibonacci` の計算を `fib` の計算に置き換えることができる。-/
+`[csimp]` 属性を与えることで、`fibonacci` の計算を `fib` の計算に置き換えることができる。-/
 @[csimp]
 theorem fib_eq_fibonacci : fibonacci = fib := by
   ext n
diff --git a/Examples/Command/Attribute/InductionEliminator.lean b/Examples/Command/Attribute/InductionEliminator.lean
index 1b9b5db4..f7587de3 100644
--- a/Examples/Command/Attribute/InductionEliminator.lean
+++ b/Examples/Command/Attribute/InductionEliminator.lean
@@ -1,8 +1,8 @@
 /- # induction_eliminator
 
-`induction_eliminator` 属性は、帰納法の枝を変更することを可能にします。
+`[induction_eliminator]` 属性は、帰納法の枝を変更することを可能にします。
 
-より詳しくいうと、[`induction`](../../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`induction_eliminator` 属性で別な定理を指定すると、それが使われるようになります。
+より詳しくいうと、[`induction`](../../Tactic/Induction.md) タクティクの `using` キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 `T` に対して `T.rec` (および `T.recOn` )という定理が自動生成されてそれが暗黙の裡に `using` キーワードの引数として使われますが、`[induction_eliminator]` 属性で別な定理を指定すると、それが使われるようになります。
 -/
 namespace InductionEliminator --#
 
@@ -42,7 +42,7 @@ info: InductionEliminator.Many.rec.{u} {α : Type} {motive : Many α → Sort u}
 #guard_msgs (whitespace := lax) in #check Many.rec
 
 -- Many.rec の `Many.more` の部分を `Many.cons` に置き換えた定理を作る。
--- これに `induction_eliminator` 属性を与えることで、
+-- これに `[induction_eliminator]` 属性を与えることで、
 -- コンストラクタ `Many.more` の代わりに `Many.cons` が使えるようになる
 @[induction_eliminator]
 protected def Many.cons_rec.{u} {α : Type} {motive : Many α → Sort u}
diff --git a/Examples/Command/Attribute/InheritDoc.lean b/Examples/Command/Attribute/InheritDoc.lean
index e5530566..6b37892b 100644
--- a/Examples/Command/Attribute/InheritDoc.lean
+++ b/Examples/Command/Attribute/InheritDoc.lean
@@ -1,5 +1,5 @@
 /- # inherit_doc
-`inherit_doc` 属性を指定すると、既存の定数などのドキュメントコメントを使いまわすことができます。
+`[inherit_doc]` 属性を指定すると、既存の定数などのドキュメントコメントを使いまわすことができます。
 -/
 import Lean
 
diff --git a/Examples/Command/Attribute/MatchPattern.lean b/Examples/Command/Attribute/MatchPattern.lean
index 8e7aeb49..39891aff 100644
--- a/Examples/Command/Attribute/MatchPattern.lean
+++ b/Examples/Command/Attribute/MatchPattern.lean
@@ -1,6 +1,6 @@
 /- # match_pattern
 
-`match_pattern` 属性を付与すると、元々コンストラクタしか使用できない `match` 式でのパターンマッチの枝に、指定した関数を使うことができるようになります。
+`[match_pattern]` 属性を付与すると、元々コンストラクタしか使用できない `match` 式でのパターンマッチの枝に、指定した関数を使うことができるようになります。
 -/
 
 /-- 自前で定義したリスト -/
@@ -21,7 +21,7 @@ def MyList.myCons (a : α) (as : MyList α) : MyList α :=
     | MyList.nil => 0
     | MyList.myCons _ as => 1 + badLength as
 
--- `match_pattern` 属性を付与する
+-- `[match_pattern]` 属性を付与する
 attribute [match_pattern] MyList.myCons
 
 -- これで `match` の中で `MyList.myCons` を使うことができる
diff --git a/Examples/Command/Attribute/Simps.lean b/Examples/Command/Attribute/Simps.lean
index 6a981880..a0bca93e 100644
--- a/Examples/Command/Attribute/Simps.lean
+++ b/Examples/Command/Attribute/Simps.lean
@@ -1,8 +1,8 @@
 /- # simps
 
-補題を [`simp`](../../Tactic/Simp.md) で使えるようにするのは `@[simp]` タグを付けることで可能ですが、`simps` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
+補題を [`simp`](../../Tactic/Simp.md) で使えるようにするのは `[simp]` 属性を付与することで可能ですが、`[simps]` 属性(または `@[simps]` タグ)を利用すると `simp` で使用するための補題を自動的に生成してくれます。
 
-例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`simps` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
+例えば、ユーザが `Point` という構造体を定義し、`Point` 上の足し算を定義したところを考えましょう。このとき、足し算はフィールドの値の足し算で定義されているため、「`Point` の和の `x` 座標」は `x` 座標の和ですが、これはそのままでは `simp` で示すことができません。`[simps]` 属性を `Point.add` 関数に付与することで、`simp` で示せるようになります。
 -/
 import Mathlib.Tactic.Simps.Basic -- simps 属性を使うため
 
@@ -22,7 +22,7 @@ example (a b : Point) : (Point.add a b).x = a.x + b.x := by
 
   rfl
 
--- `Point.add` に `simps` 属性を付与する
+-- `Point.add` に `[simps]` 属性を付与する
 attribute [simps] Point.add
 
 example (a b : Point) : (Point.add a b).x = a.x + b.x := by
diff --git a/Examples/Command/Declarative/Abbrev.lean b/Examples/Command/Declarative/Abbrev.lean
index 3a37e077..ddd18c33 100644
--- a/Examples/Command/Declarative/Abbrev.lean
+++ b/Examples/Command/Declarative/Abbrev.lean
@@ -30,7 +30,7 @@ abbrev NaturalNumber : Type := Nat
 
 end Abbrev1 --#
 /- ## 舞台裏
-`abbrev` は `@[reducible]` 属性のついた `def` と同じであり、定義に `reducible` という属性を与えても同様のことができます。-/
+`abbrev` は `[reducible]` 属性のついた `def` と同じであり、定義に `[reducible]` 属性を与えても同様のことができます。-/
 namespace Abbrev2 --#
 
 @[reducible] def NaturalNumber : Type := Nat
diff --git a/Examples/Command/Declarative/Attribute.lean b/Examples/Command/Declarative/Attribute.lean
index 9658ee26..b1ef0576 100644
--- a/Examples/Command/Declarative/Attribute.lean
+++ b/Examples/Command/Declarative/Attribute.lean
@@ -3,7 +3,7 @@
 
 `attribute` は、属性(attribute)を付与するためのコマンドです。
 
-次の例では、命題に `simp` 属性を付与しています。これは `simp` タクティクで利用される命題を増やすことを意味します。
+次の例では、命題に `[simp]` 属性を付与しています。これは `simp` タクティクで利用される命題を増やすことを意味します。
 -/
 namespace Attribute --#
 
@@ -34,7 +34,7 @@ example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
 /- ## 属性の削除
 与えた属性を削除することができることもあります。削除するには `-` を属性の頭に付けます。-/
 section
-  -- `simp` 属性を削除
+  -- `[simp]` 属性を削除
   attribute [-simp] foo
 
   -- 再び示せなくなった
diff --git a/Examples/Command/Declarative/Instance.lean b/Examples/Command/Declarative/Instance.lean
index 1910a54a..d87a21da 100644
--- a/Examples/Command/Declarative/Instance.lean
+++ b/Examples/Command/Declarative/Instance.lean
@@ -69,7 +69,7 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 
 /-
 ## 舞台裏
-`instance` は `@[instance]` 属性を付与された [`def`](./Def.md) と同じようにはたらきます。ただし `instance` はインスタンス名を省略することができるという違いがあります。
+`instance` は `[instance]` 属性を付与された [`def`](./Def.md) と同じようにはたらきます。ただし `instance` はインスタンス名を省略することができるという違いがあります。
 -/
 
 -- `List` 同士を足すことはできない
diff --git a/Examples/Tactic/Ext.lean b/Examples/Tactic/Ext.lean
index 8cafe5cb..bdcd4152 100644
--- a/Examples/Tactic/Ext.lean
+++ b/Examples/Tactic/Ext.lean
@@ -27,7 +27,7 @@ example : s ∩ t = t ∩ s := by
   aesop
 
 /- ## ext 属性
-`ext` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`ext` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
+`[ext]` 属性を命題に与えると、上記のようにその命題は `ext` タクティクで利用できるようになります。さらに、`[ext]` 属性は構造体に対しても与えることができます。このとき、その構造体に対して自動的に `.ext` と `.ext_iff` の２つの定理が生成されます。
 -/
 
 variable {α : Type}
@@ -40,7 +40,7 @@ structure Point (α : Type) where
 #check_failure Point.ext
 #check_failure Point.ext_iff
 
--- `Point` に `ext` 属性を与える
+-- `Point` に `[ext]` 属性を与える
 attribute [ext] Point
 
 -- 自動生成された定理
diff --git a/Examples/Tactic/Gcongr.lean b/Examples/Tactic/Gcongr.lean
index e8a49958..9d8de996 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]` という属性(attribute)を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
+さらに `[gcongr]` 属性を付与することにより、 `gcongr` で呼び出して使える補題を増やすことができます。-/
 
 variable {U : Type*}
 variable (A B C : Set U)