Fix dots (#228)

MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean

@@ -68,7 +68,7 @@ TEXT. -/
 example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
   apply le_trans
   · apply h₀
-  . apply h₁
+  · apply h₁
 
 example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
   apply le_trans h₀

MIL/C03_Logic/S05_Disjunction.lean

@@ -75,7 +75,7 @@ example : x < |y| → x < y ∨ x < -y := by
   rcases le_or_gt 0 y with h | h
   · rw [abs_of_nonneg h]
     intro h; left; exact h
-  . rw [abs_of_neg h]
+  · rw [abs_of_neg h]
     intro h; right; exact h
 -- QUOTE.
 
@@ -168,20 +168,20 @@ theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
 theorem le_abs_selfαα (x : ℝ) : x ≤ |x| := by
   rcases le_or_gt 0 x with h | h
   · rw [abs_of_nonneg h]
-  . rw [abs_of_neg h]
+  · rw [abs_of_neg h]
     linarith
 
 theorem neg_le_abs_selfαα (x : ℝ) : -x ≤ |x| := by
   rcases le_or_gt 0 x with h | h
   · rw [abs_of_nonneg h]
     linarith
-  . rw [abs_of_neg h]
+  · rw [abs_of_neg h]
 
 theorem abs_addαα (x y : ℝ) : |x + y| ≤ |x| + |y| := by
   rcases le_or_gt 0 (x + y) with h | h
   · rw [abs_of_nonneg h]
     linarith [le_abs_self x, le_abs_self y]
-  . rw [abs_of_neg h]
+  · rw [abs_of_neg h]
     linarith [neg_le_abs_self x, neg_le_abs_self y]
 
 /- TEXT:
@@ -205,19 +205,19 @@ theorem lt_absαα : x < |y| ↔ x < y ∨ x < -y := by
     · intro h'
       left
       exact h'
-    . intro h'
+    · intro h'
       rcases h' with h' | h'
       · exact h'
-      . linarith
+      · linarith
   rw [abs_of_neg h]
   constructor
   · intro h'
     right
     exact h'
-  . intro h'
+  · intro h'
     rcases h' with h' | h'
     · linarith
-    . exact h'
+    · exact h'
 
 theorem abs_ltαα : |x| < y ↔ -y < x ∧ x < y := by
   rcases le_or_gt 0 x with h | h
@@ -227,16 +227,16 @@ theorem abs_ltαα : |x| < y ↔ -y < x ∧ x < y := by
       constructor
       · linarith
       exact h'
-    . intro h'
+    · intro h'
       rcases h' with ⟨h1, h2⟩
       exact h2
-  . rw [abs_of_neg h]
+  · rw [abs_of_neg h]
     constructor
     · intro h'
       constructor
       · linarith
-      . linarith
-    . intro h'
+      · linarith
+    · intro h'
       linarith
 
 -- BOTH:
@@ -255,7 +255,7 @@ example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
   · left
     exact xlt
   · contradiction
-  . right; exact xgt
+  · right; exact xgt
 -- QUOTE.
 
 /- TEXT:
@@ -267,7 +267,7 @@ example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
   rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
   · rw [mul_assoc]
     apply dvd_mul_right
-  . rw [mul_comm, mul_assoc]
+  · rw [mul_comm, mul_assoc]
     apply dvd_mul_right
 -- QUOTE.
 
@@ -309,7 +309,7 @@ example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
   rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
   · right
     exact eq_neg_iff_add_eq_zero.mpr h1
-  . left
+  · left
     exact eq_of_sub_eq_zero h1
 
 example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
@@ -320,7 +320,7 @@ example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
   rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
   · right
     exact eq_neg_iff_add_eq_zero.mpr h1
-  . left
+  · left
     exact eq_of_sub_eq_zero h1
 
 /- TEXT:
@@ -364,7 +364,7 @@ example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
   rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
   · right
     exact eq_neg_iff_add_eq_zero.mpr h1
-  . left
+  · left
     exact eq_of_sub_eq_zero h1
 
 example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
@@ -375,7 +375,7 @@ example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
   rcases eq_zero_or_eq_zero_of_mul_eq_zero h'' with h1 | h1
   · right
     exact eq_neg_iff_add_eq_zero.mpr h1
-  . left
+  · left
     exact eq_of_sub_eq_zero h1
 
 -- BOTH:
@@ -400,7 +400,7 @@ example (P : Prop) : ¬¬P → P := by
   intro h
   cases em P
   · assumption
-  . contradiction
+  · contradiction
 -- QUOTE.
 
 /- TEXT:
@@ -441,10 +441,10 @@ example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
     by_cases h' : P
     · right
       exact h h'
-    . left
+    · left
       exact h'
   rintro (h | h)
   · intro h'
     exact absurd h' h
-  . intro
+  · intro
     exact h

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -101,7 +101,7 @@ example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   · left
     show x ∈ s ∩ t
     exact ⟨xs, xt⟩
-  . right
+  · right
     show x ∈ s ∩ u
     exact ⟨xs, xu⟩
 -- QUOTE.
@@ -116,7 +116,7 @@ TEXT. -/
 example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rintro x ⟨xs, xt | xu⟩
   · left; exact ⟨xs, xt⟩
-  . right; exact ⟨xs, xu⟩
+  · right; exact ⟨xs, xu⟩
 -- QUOTE.
 
 /- TEXT:
@@ -129,7 +129,7 @@ example : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
 SOLUTIONS: -/
   rintro x (⟨xs, xt⟩ | ⟨xs, xu⟩)
   · use xs; left; exact xt
-  . use xs; right; exact xu
+  · use xs; right; exact xu
 -- QUOTE.
 
 -- BOTH:
@@ -160,7 +160,7 @@ example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   -- x ∈ t ∨ x ∈ u
   rcases xtu with xt | xu
   · show False; exact xnt xt
-  . show False; exact xnu xu
+  · show False; exact xnu xu
 
 example : (s \ t) \ u ⊆ s \ (t ∪ u) := by
   rintro x ⟨⟨xs, xnt⟩, xnu⟩
@@ -200,7 +200,7 @@ example : s ∩ t = t ∩ s := by
   simp only [mem_inter_iff]
   constructor
   · rintro ⟨xs, xt⟩; exact ⟨xt, xs⟩
-  . rintro ⟨xt, xs⟩; exact ⟨xs, xt⟩
+  · rintro ⟨xt, xs⟩; exact ⟨xs, xt⟩
 -- QUOTE.
 
 /- TEXT:
@@ -232,7 +232,7 @@ TEXT. -/
 example : s ∩ t = t ∩ s := by
   apply Subset.antisymm
   · rintro x ⟨xs, xt⟩; exact ⟨xt, xs⟩
-  . rintro x ⟨xt, xs⟩; exact ⟨xs, xt⟩
+  · rintro x ⟨xt, xs⟩; exact ⟨xs, xt⟩
 -- QUOTE.
 
 /- TEXT:
@@ -274,20 +274,20 @@ example : s ∩ (s ∪ t) = s := by
   ext x; constructor
   · rintro ⟨xs, _⟩
     exact xs
-  . intro xs
+  · intro xs
     use xs; left; exact xs
 
 example : s ∪ s ∩ t = s := by
   ext x; constructor
   · rintro (xs | ⟨xs, xt⟩) <;> exact xs
-  . intro xs; left; exact xs
+  · intro xs; left; exact xs
 
 example : s \ t ∪ t = s ∪ t := by
   ext x; constructor
   · rintro (⟨xs, nxt⟩ | xt)
     · left
       exact xs
-    . right
+    · right
       exact xt
   by_cases h : x ∈ t
   · intro
@@ -306,7 +306,7 @@ example : s \ t ∪ t \ s = (s ∪ t) \ (s ∩ t) := by
       exact xs
       rintro ⟨_, xt⟩
       contradiction
-    . constructor
+    · constructor
       right
       exact xt
       rintro ⟨xs, _⟩
@@ -317,7 +317,7 @@ example : s \ t ∪ t \ s = (s ∪ t) \ (s ∩ t) := by
     intro xt
     apply nxst
     constructor <;> assumption
-  . right; use xt; intro xs
+  · right; use xt; intro xs
     apply nxst
     constructor <;> assumption
 

MIL/C04_Sets_and_Functions/S02_Functions.lean

@@ -193,28 +193,28 @@ example : f ⁻¹' (u ∪ v) = f ⁻¹' u ∪ f ⁻¹' v := by
 example : f '' (s ∩ t) ⊆ f '' s ∩ f '' t := by
   rintro y ⟨x, ⟨xs, xt⟩, rfl⟩
   constructor
-  . use x, xs
-  . use x, xt
+  · use x, xs
+  · use x, xt
 
 example (h : Injective f) : f '' s ∩ f '' t ⊆ f '' (s ∩ t) := by
   rintro y ⟨⟨x₁, x₁s, rfl⟩, ⟨x₂, x₂t, fx₂eq⟩⟩
   use x₁
   constructor
-  . use x₁s
+  · use x₁s
     rw [← h fx₂eq]
     exact x₂t
-  . rfl
+  · rfl
 
 example : f '' s \ f '' t ⊆ f '' (s \ t) := by
   rintro y ⟨⟨x₁, x₁s, rfl⟩, h⟩
   use x₁
   constructor
-  . constructor
-    . exact x₁s
-    . intro h'
+  · constructor
+    · exact x₁s
+    · intro h'
       apply h
       use x₁, h'
-  . rfl
+  · rfl
 
 example : f ⁻¹' u \ f ⁻¹' v ⊆ f ⁻¹' (u \ v) :=
   fun x ↦ id

README.md

@@ -145,7 +145,7 @@ TEXT. -/
 example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rintro x ⟨xs, xt | xu⟩
   · left; exact ⟨xs, xt⟩
-  . right; exact ⟨xs, xu⟩
+  · right; exact ⟨xs, xu⟩
 -- QUOTE.
 
 /- TEXT:
@@ -158,7 +158,7 @@ theorem foo : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
 SOLUTIONS: -/
   rintro x (⟨xs, xt⟩ | ⟨xs, xu⟩)
   · use xs; left; exact xt
-  . use xs; right; exact xu
+  · use xs; right; exact xu
 -- QUOTE.
 
 ```
@@ -190,7 +190,7 @@ variable (s t u : Set α)
 example : s ∩ (t ∪ u) ⊆ s ∩ t ∪ s ∩ u := by
   rintro x ⟨xs, xt | xu⟩
   · left; exact ⟨xs, xt⟩
-  . right; exact ⟨xs, xu⟩
+  · right; exact ⟨xs, xu⟩
 -- QUOTE.
 
 ```
@@ -215,7 +215,7 @@ theorem foo : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
 theorem fooαα : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
   rintro x (⟨xs, xt⟩ | ⟨xs, xu⟩)
   · use xs; left; exact xt
-  . use xs; right; exact xu
+  · use xs; right; exact xu
 
 ```
 The theorem is named `foo` in both the examples and the solutions, but Lean doesn't
@@ -230,7 +230,7 @@ theorem foo : s ∩ t ∪ s ∩ u ⊆ s ∩ (t ∪ u) := by
 -- TAG: my_tag
   rintro x (⟨xs, xt⟩ | ⟨xs, xu⟩)
   · use xs; left; exact xt
-  . use xs; right; exact xu
+  · use xs; right; exact xu
 -- TAG: end
 ```
 The first tag can have any label you want in place of `my_tag`, whereas the second should