fix: change refine to exact in files where it speeds up (#11896)

See #11890 and this [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Usage.20of.20refine') for an in-depth explanation of why these `refine`s and not others.

The short answer is that the files in which these replacements took place were more performant after the change than before.

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -365,7 +365,7 @@ theorem affine_openCover_TFAE {X Y : Scheme.{u}} [IsAffine Y] (f : X ⟶ Y) :
   tfae_have 4 → 3
   · intro H 𝒰 _ i; apply H
   tfae_have 3 → 2
-  · intro H; refine' ⟨X.affineCover, inferInstance, H _⟩
+  · intro H; exact ⟨X.affineCover, inferInstance, H _⟩
   tfae_have 2 → 1
   · rintro ⟨𝒰, _, h𝒰⟩
     exact sourceAffineLocally_of_source_openCover hP f 𝒰 h𝒰
@@ -392,7 +392,7 @@ theorem openCover_TFAE {X Y : Scheme.{u}} [IsAffine Y] (f : X ⟶ Y) :
   tfae_have 4 → 3
   · intro H 𝒰 _ i; apply H
   tfae_have 3 → 2
-  · intro H; refine' ⟨X.affineCover, H _⟩
+  · intro H; exact ⟨X.affineCover, H _⟩
   tfae_have 2 → 1
   · rintro ⟨𝒰, h𝒰⟩
     -- Porting note: this has metavariable if I put it directly into rw
@@ -505,7 +505,7 @@ theorem affineLocally_of_isOpenImmersion (hP : RingHom.PropertyIsLocal @P) {X Y
     convert @this esto eso _ _ ?_ ?_ ?_
     · exact 1
     -- Porting note: again we have to bypass TC synthesis to keep Lean from running away
-    · refine'
+    · exact
         @IsLocalization.away_of_isUnit_of_bijective _ _ _ _ (_) _ isUnit_one Function.bijective_id
   · intro; exact H
 #align ring_hom.property_is_local.affine_locally_of_is_open_immersion RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion

Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

@@ -190,7 +190,7 @@ theorem norm_eval_le_injectiveSeminorm (f : ContinuousMultilinearMap 𝕜 E F) (
   suffices h : ‖lift f'.toMultilinearMap x‖ ≤ ‖f'‖ * injectiveSeminorm x by
     change ‖(e (lift f'.toMultilinearMap x)).1‖ ≤ _ at h
     rw [heq] at h
-    refine le_trans h (mul_le_mul_of_nonneg_right hnorm (apply_nonneg _ _))
+    exact le_trans h (mul_le_mul_of_nonneg_right hnorm (apply_nonneg _ _))
   have hle : Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
       (toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E)) ≤ injectiveSeminorm := by
     simp only [injectiveSeminorm]

Mathlib/CategoryTheory/Subobject/MonoOver.lean

@@ -366,7 +366,7 @@ def image : Over X ⥤ MonoOver X where
   map {f g} k := by
     apply (forget X).preimage _
     apply Over.homMk _ _
-    refine'
+    exact
       image.lift
         { I := Limits.image _
           m := image.ι g.hom
@@ -387,7 +387,7 @@ def imageForgetAdj : image ⊣ forget X :=
             apply image.fac
           invFun := fun k => by
             refine' Over.homMk _ _
-            refine'
+            exact
               image.lift
                 { I := g.obj.left
                   m := g.arrow

Mathlib/RepresentationTheory/Rep.lean

@@ -665,7 +665,7 @@ set_option linter.uppercaseLean3 false in
 def counitIsoAddEquiv {M : ModuleCat.{u} (MonoidAlgebra k G)} :
     (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M ≃+ M := by
   dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
-  refine' (Representation.ofModule M).asModuleEquiv.trans
+  exact (Representation.ofModule M).asModuleEquiv.trans
     (RestrictScalars.addEquiv k (MonoidAlgebra k G) _)
 set_option linter.uppercaseLean3 false in
 #align Rep.counit_iso_add_equiv Rep.counitIsoAddEquiv