Convert refine' to refine (#229)

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -139,7 +139,7 @@ SOLUTIONS: -/
     exact Nat.succ_le_of_lt (Nat.factorial_pos _)
 -- BOTH:
   rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
-  refine' ⟨p, _, pp⟩
+  refine ⟨p, ?_, pp⟩
   show p > n
   by_contra ple
   push_neg  at ple

MIL/C09_Topology/S02_Metric_Spaces.lean

@@ -233,7 +233,7 @@ example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n,
   rw [Metric.mem_closure_iff]
   intro ε ε_pos
   rcases hu ε ε_pos with ⟨N, hN⟩
-  refine' ⟨u N, hs _, _⟩
+  refine ⟨u N, hs _, ?_⟩
   rw [dist_comm]
   exact hN N le_rfl
 
@@ -539,7 +539,7 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
     rw [dist_comm] at xy
     obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedBall y r ⊆ f n :=
       nhds_basis_closedBall.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
-    refine' ⟨y, min (min (δ / 2) r) (B (n + 1)), _, _, fun z hz ↦ ⟨_, _⟩⟩
+    refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz ↦ ⟨?_, ?_⟩⟩
     show 0 < min (min (δ / 2) r) (B (n + 1))
     exact lt_min (lt_min (half_pos δpos) rpos) (Bpos (n + 1))
     show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
@@ -560,7 +560,7 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
           _ ≤ r := (min_le_left _ _).trans (min_le_right _ _)
           )
   choose! center radius Hpos HB Hball using this
-  refine' fun x ↦ (mem_closure_iff_nhds_basis nhds_basis_closedBall).2 fun ε εpos ↦ _
+  refine fun x ↦ (mem_closure_iff_nhds_basis nhds_basis_closedBall).2 fun ε εpos ↦ ?_
   /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all
     `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball
     `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that
@@ -602,13 +602,13 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : 
   use y
   have I : ∀ n, ∀ m ≥ n, closedBall (c m) (r m) ⊆ closedBall (c n) (r n) := by
     intro n
-    refine' Nat.le_induction _ fun m hnm h ↦ _
+    refine Nat.le_induction ?_ fun m hnm h ↦ ?_
     · exact Subset.rfl
     · exact (incl m).trans (Set.inter_subset_left.trans h)
   have yball : ∀ n, y ∈ closedBall (c n) (r n) := by
     intro n
-    refine' isClosed_ball.mem_of_tendsto ylim _
-    refine' (Filter.eventually_ge_atTop n).mono fun m hm ↦ _
+    refine isClosed_ball.mem_of_tendsto ylim ?_
+    refine (Filter.eventually_ge_atTop n).mono fun m hm ↦ ?_
     exact I n m hm (mem_closedBall_self (rpos _).le)
   constructor
   · suffices ∀ n, y ∈ f n by rwa [Set.mem_iInter]

MIL/C09_Topology/S03_Topological_Spaces.lean

@@ -151,7 +151,7 @@ example {α : Type*} (n : α → Filter α) (H₀ : ∀ a, pure a ≤ n a)
     (H : ∀ a : α, ∀ p : α → Prop, (∀ᶠ x in n a, p x) → ∀ᶠ y in n a, ∀ᶠ x in n y, p x) :
     ∀ a, ∀ s ∈ n a, ∃ t ∈ n a, t ⊆ s ∧ ∀ a' ∈ t, s ∈ n a' := by
   intro a s s_in
-  refine' ⟨{ y | s ∈ n y }, H a (fun x ↦ x ∈ s) s_in, _, by tauto⟩
+  refine ⟨{ y | s ∈ n y }, H a (fun x ↦ x ∈ s) s_in, ?_, by tauto⟩
   rintro y (hy : s ∈ n y)
   exact H₀ y hy
 
@@ -509,7 +509,7 @@ example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs :
     rwa [map_eq, inf_of_le_right F_le]
   have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left
   rcases hs Hle with ⟨x, x_in, hx⟩
-  refine' ⟨f x, mem_image_of_mem f x_in, _⟩
+  refine ⟨f x, mem_image_of_mem f x_in, ?_⟩
   apply hx.map hf.continuousAt
   rw [Tendsto, map_eq]
   exact inf_le_right

MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean

@@ -200,7 +200,7 @@ example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, 
   have real_norm_le : ∀ z ∈ ball x ε, ∀ (i : ι), ‖g i z‖ ≤ m
   sorry
   have εk_pos : 0 < ε / ‖k‖ := sorry
-  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos _ hk _⟩
+  refine ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos ?_ hk ?_⟩
   sorry
   sorry
 -- QUOTE.
@@ -215,7 +215,7 @@ example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, 
     isClosed_iInter fun i ↦ isClosed_le (g i).cont.norm continuous_const
   -- the union is the entire space; this is where we use `h`
   have hU : (⋃ n : ℕ, e n) = univ := by
-    refine' eq_univ_of_forall fun x ↦ _
+    refine eq_univ_of_forall fun x ↦ ?_
     rcases h x with ⟨C, hC⟩
     obtain ⟨m, hm⟩ := exists_nat_ge C
     exact ⟨e m, mem_range_self m, mem_iInter.mpr fun i ↦ le_trans (hC i) hm⟩
@@ -230,7 +230,7 @@ example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, 
     replace hz := mem_iInter.mp (interior_iInter_subset _ (hε hz)) i
     apply interior_subset hz
   have εk_pos : 0 < ε / ‖k‖ := div_pos ε_pos (zero_lt_one.trans hk)
-  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos _ hk _⟩
+  refine ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos ?_ hk ?_⟩
   · exact div_nonneg (Nat.cast_nonneg _) εk_pos.le
   intro y le_y y_lt
   calc