chore: reduce usage of refine' (#5042)

src/Init/Control/ExceptCps.lean

@@ -34,7 +34,7 @@ instance : Monad (ExceptCpsT ε m) where
   bind x f := fun _ k₁ k₂ => x _ (fun a => f a _ k₁ k₂) k₂
 
 instance : LawfulMonad (ExceptCpsT σ m) := by
-  refine' { .. } <;> intros <;> rfl
+  refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
 instance : MonadExceptOf ε (ExceptCpsT ε m) where
   throw e  := fun _ _ k => k e

src/Init/Control/Lawful/Basic.lean

@@ -153,7 +153,7 @@ namespace Id
 @[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
 
 instance : LawfulMonad Id := by
-  refine' { .. } <;> intros <;> rfl
+  refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
 end Id
 

src/Init/Control/StateCps.lean

@@ -35,7 +35,7 @@ instance : Monad (StateCpsT σ m) where
   bind x f := fun δ s k => x δ s fun a s => f a δ s k
 
 instance : LawfulMonad (StateCpsT σ m) := by
-  refine' { .. } <;> intros <;> rfl
+  refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
 @[always_inline]
 instance : MonadStateOf σ (StateCpsT σ m) where

src/Init/Data/List/TakeDrop.lean

@@ -127,7 +127,7 @@ theorem drop_tail (l : List α) (n : Nat) : l.tail.drop n = l.drop (n + 1) := by
 
 @[simp]
 theorem drop_eq_nil_iff_le {l : List α} {k : Nat} : l.drop k = [] ↔ l.length ≤ k := by
-  refine' ⟨fun h => _, drop_eq_nil_of_le⟩
+  refine ⟨fun h => ?_, drop_eq_nil_of_le⟩
   induction k generalizing l with
   | zero =>
     simp only [drop] at h

src/lake/Lake/Config/Package.lean

@@ -240,7 +240,7 @@ structure Package where
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
-  by refine' ⟨{..}⟩ <;> exact default
+  ⟨by constructor <;> exact default⟩
 
 hydrate_opaque_type OpaquePackage Package
 

src/lake/Lake/Config/Workspace.lean

@@ -32,7 +32,7 @@ structure Workspace : Type where
 
 instance : Nonempty Workspace :=
   have : Inhabited Package := Classical.inhabited_of_nonempty inferInstance
-  by refine' ⟨{..}⟩ <;> exact default
+  ⟨by constructor <;> exact default⟩
 
 hydrate_opaque_type OpaqueWorkspace Workspace
 

tests/lean/1870.lean

@@ -16,8 +16,9 @@ instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
 instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
   one := 1
 
+set_option pp.mvars false in
 theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  refine' congrArg _ (congrArg _ _)
+  refine congrArg _ (congrArg _ ?_)
   rfl
 
 example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by

tests/lean/1870.lean.expected.out

@@ -1,15 +1,15 @@
-1870.lean:20:2-20:35: error: type mismatch
-  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?m)
+1870.lean:21:2-21:35: error: type mismatch
+  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
 has type
   OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:24:2-24:16: error: tactic 'apply' failed, failed to unify
+1870.lean:25:2-25:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:29:2-29:16: error: tactic 'apply' failed, failed to unify
+1870.lean:30:2-30:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1

tests/lean/run/2461.lean

@@ -93,7 +93,7 @@ instance instRingHomClass (R S : Type) [Semiring R] [Semiring S] :
 
 -- this is needed to create the troublesome instance `Algebra.instid`
 def RingHom.id (α : Type) [Semiring α] : α →+* α := by
-  refine' { toFun := _root_.id.. }
+  refine { toFun := _root_.id.. }
 
 end algebra_hierarchy_morphisms
 

tests/lean/run/structWithAlgTCSynth.lean

@@ -572,7 +572,7 @@ infixr:25 " →+* " => RingHom
 namespace RingHom
 
 def id (α : Type _) : α →+* α := by
-  refine' { toFun := _root_.id.. }
+  refine { toFun := _root_.id.. }
 
 def comp (g : β →+* γ) (f : α →+* β) : α →+* γ :=
   { toFun := g.toFun ∘ f.toFun }