chore: more refine' to refine (#13287)

A PR analogous to #13166.  The reason some of these `refine'` are now caught is that my previous script missed all instances.  I am not sure why it is still missing other `refine'`.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -107,7 +107,7 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
 set_option tactic.skipAssignedInstances false in
 theorem real_roots_Phi_le : Fintype.card ((Φ ℚ a b).rootSet ℝ) ≤ 3 := by
   rw [← map_Phi a b (algebraMap ℤ ℚ), Φ, ← one_mul (X ^ 5), ← C_1]
-  refine' (card_rootSet_le_derivative _).trans
+  apply (card_rootSet_le_derivative _).trans
     (Nat.succ_le_succ ((card_rootSet_le_derivative _).trans (Nat.succ_le_succ _)))
   suffices (Polynomial.rootSet (C (20 : ℚ) * X ^ 3) ℝ).Subsingleton by
     norm_num [Fintype.card_le_one_iff_subsingleton, ← mul_assoc] at *
@@ -129,7 +129,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
   · have hf1 : f 1 < 0 := by simp [hf, hb]
     have hfa : 0 ≤ f a := by
       simp_rw [hf, ← sq]
-      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha _)) _ <;> norm_num
+      refine add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha ?_)) ?_ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
@@ -140,7 +140,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
           norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
-          refine' add_le_add (sub_le_sub_left (pow_le_pow_right ha _) _) _ <;> linarith
+          refine add_le_add (sub_le_sub_left (pow_le_pow_right ha ?_) _) ?_ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -80,7 +80,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       intro hi
       rw [mem_image] at this
       obtain ⟨t, ht₁, ht₂⟩ := this
-      refine' ⟨t, by rwa [ht₂], _⟩
+      refine ⟨t, by rwa [ht₂], ?_⟩
       rw [mem_filter] at ht₁
       apply ht₁.2.2
   -- Show first that the pair of labels is unique.
@@ -106,7 +106,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       -- Ensure `t` ends at `i`.
       have : t.max = i := by simp only [ht₁.2.1]
       -- Now our new subsequence is given by adding `j` at the end of `t`.
-      refine' ⟨insert j t, _, _⟩
+      refine ⟨insert j t, ?_, ?_⟩
       -- First make sure it's valid, i.e., that this subsequence ends at `j` and is increasing
       · rw [mem_filter]
         refine ⟨?_, ?_, ?_⟩
@@ -155,7 +155,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       constructor <;>
         · apply le_max'
           rw [mem_image]
-          refine' ⟨{i}, by solve_by_elim, card_singleton i⟩
+          refine ⟨{i}, by solve_by_elim, card_singleton i⟩
     refine ⟨?_, ?_⟩
     -- Need to get `a_i ≤ r`, here phrased as: there is some `a < r` with `a+1 = a_i`.
     · refine ⟨(ab i).1 - 1, ?_, Nat.succ_pred_eq_of_pos z.1⟩

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -374,7 +374,7 @@ theorem ballot_problem' :
       field_simp [h₄, h₅, h₆] at *
       ring
     all_goals
-      refine' (ENNReal.mul_lt_top _ _).ne
+      refine (ENNReal.mul_lt_top ?_ ?_).ne
       · exact (measure_lt_top _ _).ne
       · simp [Ne, ENNReal.div_eq_top]
 #align ballot.ballot_problem' Ballot.ballot_problem'

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -138,7 +138,7 @@ lemma measurable_needleCrossesIndicator : Measurable (needleCrossesIndicator l)
   case' l => refine isClosed_le continuous_fst ?_
   case' r => refine isClosed_le (Continuous.neg continuous_fst) ?_
   all_goals
-    refine' Continuous.mul (Continuous.mul _ continuous_const) continuous_const
+    refine Continuous.mul (Continuous.mul ?_ continuous_const) continuous_const
     simp_rw [← Function.comp_apply (f := Real.sin) (g := Prod.snd),
       Continuous.comp Real.continuous_sin continuous_snd]
 

Counterexamples/DirectSumIsInternal.lean

@@ -65,7 +65,7 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
 #align counterexample.with_sign.is_compl Counterexample.withSign.isCompl
 
 def withSign.independent : CompleteLattice.Independent withSign := by
-  refine'
+  apply
     (CompleteLattice.independent_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i
   fin_cases i <;> simp

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -104,8 +104,8 @@ def grading.decompose : R × R →+ DirectSum Two fun i => grading R i where
     of (grading R ·) 0 ⟨(zz.1, zz.1), rfl⟩ +
     of (grading R ·) 1 ⟨(0, zz.2 - zz.1), rfl⟩
   map_zero' := by
-    refine' DFinsupp.ext (fun (i : Two) =>
-        Option.casesOn i _ (fun (i_1 : Unit) => PUnit.casesOn i_1 _)) <;> rfl
+    refine DFinsupp.ext (fun (i : Two) =>
+        Option.casesOn i ?_ (fun (i_1 : Unit) => PUnit.casesOn i_1 ?_)) <;> rfl
   map_add' := by
     rintro ⟨a1, b1⟩ ⟨a2, b2⟩
     rw [add_add_add_comm, ← map_add, ← map_add]

Counterexamples/MapFloor.lean

@@ -66,7 +66,7 @@ instance linearOrder : LinearOrder ℤ[ε] :=
   LinearOrder.lift' (toLex ∘ coeff) coeff_injective
 
 instance orderedAddCommGroup : OrderedAddCommGroup ℤ[ε] := by
-  refine' (toLex.injective.comp coeff_injective).orderedAddCommGroup _ _ _ _ _ _ _ <;>
+  refine (toLex.injective.comp coeff_injective).orderedAddCommGroup _ ?_ ?_ ?_ ?_ ?_ ?_ <;>
   (first | rfl | intros) <;> funext <;>
   (simp only [comp_apply, Pi.toLex_apply, coeff_add, coeff_neg, coeff_sub,
     ← nsmul_eq_mul, ← zsmul_eq_mul]; rfl)
@@ -95,7 +95,7 @@ instance : FloorRing ℤ[ε] :=
     constructor
     · split_ifs with h
       · rintro ⟨_ | n, hn⟩
-        · refine' (sub_one_lt _).trans _
+        · apply (sub_one_lt _).trans _
           simp at hn
           rwa [intCast_coeff_zero] at hn
         · dsimp at hn

Counterexamples/SorgenfreyLine.lean

@@ -162,7 +162,7 @@ instance : OrderClosedTopology ℝₗ :=
   ⟨isClosed_le_prod.preimage (continuous_toReal.prod_map continuous_toReal)⟩
 
 instance : ContinuousAdd ℝₗ := by
-  refine' ⟨continuous_iff_continuousAt.2 _⟩
+  refine ⟨continuous_iff_continuousAt.2 ?_⟩
   rintro ⟨x, y⟩
   rw [ContinuousAt, nhds_prod_eq, nhds_eq_comap (x + y), tendsto_comap_iff,
     nhds_eq_map, nhds_eq_map, prod_map_map_eq, ← nhdsWithin_prod_eq, Ici_prod_Ici]
@@ -198,12 +198,12 @@ instance : CompletelyNormalSpace ℝₗ := by
   Then `⋃ x ∈ s, Ico x (X x)` and `⋃ y ∈ t, Ico y (Y y)` are
   disjoint open sets that include `s` and `t`.
   -/
-  refine' ⟨fun s t hd₁ hd₂ => _⟩
+  refine ⟨fun s t hd₁ hd₂ => ?_⟩
   choose! X hX hXd using fun x (hx : x ∈ s) =>
     exists_Ico_disjoint_closed isClosed_closure (disjoint_left.1 hd₂ hx)
   choose! Y hY hYd using fun y (hy : y ∈ t) =>
     exists_Ico_disjoint_closed isClosed_closure (disjoint_right.1 hd₁ hy)
-  refine' disjoint_of_disjoint_of_mem _
+  refine disjoint_of_disjoint_of_mem ?_
     (bUnion_mem_nhdsSet fun x hx => (isOpen_Ico x (X x)).mem_nhds <| left_mem_Ico.2 (hX x hx))
     (bUnion_mem_nhdsSet fun y hy => (isOpen_Ico y (Y y)).mem_nhds <| left_mem_Ico.2 (hY y hy))
   simp only [disjoint_iUnion_left, disjoint_iUnion_right, Ico_disjoint_Ico]

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -515,8 +515,8 @@ def adjoin (s : Set A) : NonUnitalSubalgebra R A :=
       @fun a b (ha : a ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A))
         (hb : b ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A)) =>
       show a * b ∈ Submodule.span R (NonUnitalSubsemiring.closure s : Set A) by
-        refine' Submodule.span_induction ha _ _ _ _
-        · refine' Submodule.span_induction hb _ _ _ _
+        refine Submodule.span_induction ha ?_ ?_ ?_ ?_
+        · refine Submodule.span_induction hb ?_ ?_ ?_ ?_
           · exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
               (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)
           · exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _

Mathlib/Algebra/BigOperators/Fin.lean

@@ -330,7 +330,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       cases m
       · exact isEmptyElim (f <| Fin.last _)
       simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
-      refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
+      refine (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq ?_
       rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']⟩)
     (fun a b => ⟨a / m ^ (b : ℕ) % m, by
       cases' n with n
@@ -385,7 +385,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
       intro n nn f fn
       cases nn
       · exact isEmptyElim fn
-      refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
+      refine (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq ?_
       rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]⟩)
     (fun a b => ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b, by
       cases m

Mathlib/Algebra/BigOperators/Group/Multiset.lean

@@ -232,7 +232,7 @@ theorem prod_induction (p : α → Prop) (s : Multiset α) (p_mul : ∀ a b, p a
 @[to_additive]
 theorem prod_induction_nonempty (p : α → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅)
     (p_s : ∀ a ∈ s, p a) : p s.prod := by
-  -- Porting note: used `refine' Multiset.induction _ _`
+  -- Porting note: used to be `refine' Multiset.induction _ _`
   induction' s using Multiset.induction_on with a s hsa
   · simp at hs
   rw [prod_cons]

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -193,7 +193,7 @@ theorem sum_Ico_Ico_comm {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ →
     (fun _ _ ↦ rfl) <;>
   simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
   rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
-  refine' ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>
+  refine ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>
   omega
 #align finset.sum_Ico_Ico_comm Finset.sum_Ico_Ico_comm
 
@@ -206,7 +206,7 @@ theorem sum_Ico_Ico_comm' {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ →
     (fun _ _ ↦ rfl) <;>
   simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
   rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
-  refine' ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>
+  refine ⟨⟨_, _⟩, ⟨_, _⟩⟩ <;>
   omega
 
 @[to_additive]

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -193,7 +193,7 @@ instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom
   (associativity := associativity R)
 
 instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
-  refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
+  refine ⟨⟨Finsupp.lapply PUnit.unit, ⟨?_, ?_⟩⟩⟩
   · -- Porting note (#11041): broken ext
     apply LinearMap.ext_ring
     -- Porting note (#10959): simp used to be able to close this goal

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -136,7 +136,7 @@ instance colimitModule : Module R (M F) :=
 { colimitMulAction F,
   colimitSMulWithZero F with
   smul_add := fun r x y => by
-    refine' Quot.induction_on₂ x y _; clear x y; intro x y; cases' x with i x; cases' y with j y
+    refine Quot.induction_on₂ x y ?_; clear x y; intro x y; cases' x with i x; cases' y with j y
     erw [colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
       (IsFiltered.rightToMax i j), colimit_smul_mk_eq, smul_add, colimit_smul_mk_eq,
       colimit_smul_mk_eq, colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -282,7 +282,7 @@ open Opposite
 
 -- Porting note: simp wasn't firing but rw was, annoying
 instance : MonoidalPreadditive (ModuleCat.{u} R) := by
-  refine' ⟨_, _, _, _⟩
+  refine ⟨?_, ?_, ?_, ?_⟩
   · dsimp only [autoParam]; intros
     refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
@@ -316,7 +316,7 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by
 
 -- Porting note: simp wasn't firing but rw was, annoying
 instance : MonoidalLinear R (ModuleCat.{u} R) := by
-  refine' ⟨_, _⟩
+  refine ⟨?_, ?_⟩
   · dsimp only [autoParam]; intros
     refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -67,7 +67,7 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
           rw [this, comp_def, LinearEquiv.range_comp]
         · exact (Submodule.range_subtype _).symm
       map_rel_iff' := fun {S T} => by
-        refine' ⟨fun h => _, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
+        refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
         convert LinearMap.range_comp_le_range (ofMkLEMk _ _ h) (↾T.subtype)
         · simpa only [← comp_def, ofMkLEMk_comp] using (Submodule.range_subtype _).symm
         · exact (Submodule.range_subtype _).symm }

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -167,7 +167,7 @@ theorem colimitMulAux_eq_of_rel_right {x y y' : Σ j, F.obj j}
 @[to_additive "Addition in the colimit. See also `colimitAddAux`."]
 noncomputable instance colimitMul : Mul (M.{v, u} F) :=
 { mul := fun x y => by
-    refine' Quot.lift₂ (colimitMulAux F) _ _ x y
+    refine Quot.lift₂ (colimitMulAux F) ?_ ?_ x y
     · intro x y y' h
       apply colimitMulAux_eq_of_rel_right
       apply Types.FilteredColimit.rel_of_quot_rel

Mathlib/Algebra/DirectLimit.lean

@@ -702,7 +702,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
   refine span_induction (Ideal.Quotient.eq_zero_iff_mem.1 H) ?_ ?_ ?_ ?_
   · rintro x (⟨i, j, hij, x, rfl⟩ | ⟨i, rfl⟩ | ⟨i, x, y, rfl⟩ | ⟨i, x, y, rfl⟩)
     · refine'
-        ⟨j, {⟨i, x⟩, ⟨j, f' i j hij x⟩}, _,
+        ⟨j, {⟨i, x⟩, ⟨j, f' i j hij x⟩}, ?_,
           isSupported_sub (isSupported_of.2 <| Or.inr rfl) (isSupported_of.2 <| Or.inl rfl),
             fun [_] => _⟩
       · rintro k (rfl | ⟨rfl | _⟩)
@@ -724,7 +724,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
       · rw [RingHom.map_sub, RingHom.map_sub]
         erw [lift_of, dif_pos rfl, RingHom.map_one, lift_of, RingHom.map_one, sub_self]
     · refine'
-        ⟨i, {⟨i, x + y⟩, ⟨i, x⟩, ⟨i, y⟩}, _,
+        ⟨i, {⟨i, x + y⟩, ⟨i, x⟩, ⟨i, y⟩}, ?_,
           isSupported_sub (isSupported_of.2 <| Or.inl rfl)
             (isSupported_add (isSupported_of.2 <| Or.inr <| Or.inl rfl)
               (isSupported_of.2 <| Or.inr <| Or.inr rfl)),

Mathlib/Algebra/Free.lean

@@ -375,7 +375,7 @@ theorem quot_mk_assoc_left (x y z w : α) :
 @[to_additive]
 instance : Semigroup (AssocQuotient α) where
   mul x y := by
-    refine' Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) _ _
+    refine Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) ?_ ?_
     · rintro a b₁ b₂ (⟨c, d, e⟩ | ⟨c, d, e, f⟩) <;> simp only
       · exact quot_mk_assoc_left _ _ _ _
       · rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -947,14 +947,14 @@ instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
   ⟨fun g₁ g₂ => by
     have hgcd : g₁.gcd = g₂.gcd := by
       ext a b
-      refine' associated_iff_eq.mp (associated_of_dvd_dvd _ _)
+      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
       -- Porting note: Lean4 seems to need help specifying `g₁` and `g₂`
       · exact dvd_gcd (@gcd_dvd_left _ _ g₁ _ _) (@gcd_dvd_right _ _ g₁ _ _)
       · exact @dvd_gcd _ _ g₁ _ _ _ (@gcd_dvd_left _ _ g₂ _ _) (@gcd_dvd_right _ _ g₂ _ _)
     have hlcm : g₁.lcm = g₂.lcm := by
       ext a b
       -- Porting note: Lean4 seems to need help specifying `g₁` and `g₂`
-      refine' associated_iff_eq.mp (associated_of_dvd_dvd _ _)
+      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
       · exact (@lcm_dvd_iff _ _ g₁ ..).mpr ⟨@dvd_lcm_left _ _ g₂ _ _, @dvd_lcm_right _ _ g₂ _ _⟩
       · exact lcm_dvd_iff.mpr ⟨@dvd_lcm_left _ _ g₁ _ _, @dvd_lcm_right _ _ g₁ _ _⟩
     cases g₁
@@ -1007,7 +1007,7 @@ variable [CommRing α] [IsDomain α] [NormalizedGCDMonoid α]
 theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c := by
   apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
     rw [dvd_gcd_iff] <;>
-    refine' ⟨gcd_dvd_left _ _, _⟩
+    refine ⟨gcd_dvd_left _ _, ?_⟩
   · rcases h with ⟨d, hd⟩
     rcases gcd_dvd_right a b with ⟨e, he⟩
     rcases gcd_dvd_left a b with ⟨f, hf⟩
@@ -1268,7 +1268,7 @@ noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq
         · exact absurd ‹a = 0› h
         · exact absurd ‹b = 0› h_1
       apply mul_left_cancel₀ h0
-      refine' _root_.trans _ (Classical.choose_spec (exists_gcd a b))
+      refine _root_.trans ?_ (Classical.choose_spec (exists_gcd a b))
       conv_lhs =>
         congr
         rw [← normalize_lcm a b]
@@ -1421,9 +1421,9 @@ instance (priority := 100) : NormalizedGCDMonoid G₀ where
     · apply dvd_zero
     · rw [not_and_or] at h
       cases h
-      · refine' isUnit_iff_dvd_one.mp (isUnit_of_dvd_unit _ (IsUnit.mk0 _ ‹c ≠ 0›))
+      · refine isUnit_iff_dvd_one.mp (isUnit_of_dvd_unit ?_ (IsUnit.mk0 _ ‹c ≠ 0›))
         exact hac
-      · refine' isUnit_iff_dvd_one.mp (isUnit_of_dvd_unit _ (IsUnit.mk0 _ ‹b ≠ 0›))
+      · refine isUnit_iff_dvd_one.mp (isUnit_of_dvd_unit ?_ (IsUnit.mk0 _ ‹b ≠ 0›))
         exact hab
   gcd_mul_lcm a b := by
     by_cases ha : a = 0

Mathlib/Algebra/GeomSum.lean

@@ -253,7 +253,7 @@ protected theorem Commute.geom_sum₂_comm {α : Type u} [Semiring α] {x y : α
   cases n; · simp
   simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]
   rw [← Finset.sum_flip]
-  refine' Finset.sum_congr rfl fun i hi => _
+  refine Finset.sum_congr rfl fun i hi => ?_
   simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _
 #align commute.geom_sum₂_comm Commute.geom_sum₂_comm
 
@@ -286,7 +286,7 @@ protected theorem Commute.mul_geom_sum₂_Ico [Ring α] {x y : α} (h : Commute
   have :
     ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
       ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
-    refine' sum_congr rfl fun j j_in => _
+    refine sum_congr rfl fun j j_in => ?_
     rw [← pow_add]
     congr
     rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in
@@ -305,7 +305,7 @@ protected theorem Commute.geom_sum₂_succ_eq {α : Type u} [Ring α] {x y : α}
       x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) := by
   simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
     (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']
-  refine' sum_congr rfl fun i hi => _
+  refine sum_congr rfl fun i hi => ?_
   suffices n - 1 - i + 1 = n - i by rw [this]
   cases' n with n
   · exact absurd (List.mem_range.mp hi) i.not_lt_zero
@@ -331,7 +331,7 @@ protected theorem Commute.geom_sum₂_Ico_mul [Ring α] {x y : α} (h : Commute
   simp only [op_sub, op_mul, op_pow, op_sum]
   have : (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
       ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
-    refine' sum_congr rfl fun k _ => _
+    refine sum_congr rfl fun k _ => ?_
     have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
     simpa [Commute, SemiconjBy] using hp
   simp only [this]

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -1175,7 +1175,7 @@ def closureCommGroupOfComm {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y
     mul_comm := fun x y => by
       ext
       simp only [Subgroup.coe_mul]
-      refine'
+      refine
         closure_induction₂ x.prop y.prop hcomm (fun x => by simp only [mul_one, one_mul])
           (fun x => by simp only [mul_one, one_mul])
           (fun x y z h₁ h₂ => by rw [mul_assoc, h₂, ← mul_assoc, h₁, mul_assoc])
@@ -2331,7 +2331,7 @@ theorem le_normalClosure {H : Subgroup G} : H ≤ normalClosure ↑H := fun _ h
 /-- The normal closure of `s` is a normal subgroup. -/
 instance normalClosure_normal : (normalClosure s).Normal :=
   ⟨fun n h g => by
-    refine' Subgroup.closure_induction h (fun x hx => _) _ (fun x y ihx ihy => _) fun x ihx => _
+    refine Subgroup.closure_induction h (fun x hx => ?_) ?_ (fun x y ihx ihy => ?_) fun x ihx => ?_
     · exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
     · simpa using (normalClosure s).one_mem
     · rw [← conj_mul]