chore: deal with a few convert porting notes (#3887)

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -483,26 +483,15 @@ instance (priority := 100) semi_normed_ring_top_monoid [NonUnitalSeminormedRing
             _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
               norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
         refine squeeze_zero (fun e => norm_nonneg _) this ?_
-        -- porting note: the new `convert` sucks, it's way too dumb without using the type
-        -- of the goal to figure out how to match things up. The rest of this proof was:
-        /- convert
+        convert
           ((continuous_fst.tendsto x).norm.mul
                 ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
             (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul _)
-        show tendsto _ _ _
+        -- Porting note: `show` used to select a goal to work on
+        rotate_right
+        show Tendsto _ _ _
         exact tendsto_const_nhds
-        simp -/
-        rw [←zero_add 0]
-        refine Tendsto.add ?_ ?_
-        · rw [←mul_zero (‖x.fst‖)]
-          refine Filter.Tendsto.mul ?_ ?_
-          · exact (continuous_fst.tendsto x).norm
-          · rw [←norm_zero (E := α), ←sub_self x.snd]
-            exact ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm
-        · rw [←zero_mul (‖x.snd‖)]
-          refine' Filter.Tendsto.mul _ tendsto_const_nhds
-          rw [←norm_zero (E := α), ←sub_self x.fst]
-          exact ((continuous_fst.tendsto x).sub tendsto_const_nhds).norm⟩
+        simp⟩
 #align semi_normed_ring_top_monoid semi_normed_ring_top_monoid
 
 -- see Note [lower instance priority]

Mathlib/Analysis/Normed/Order/Lattice.lean

@@ -142,9 +142,8 @@ instance (priority := 100) NormedLatticeAddCommGroup.continuousInf : ContinuousI
   have : ∀ p : α × α, ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖ := fun _ =>
     norm_inf_sub_inf_le_add_norm _ _ _ _
   refine' squeeze_zero (fun e => norm_nonneg _) this _
-  -- porting note: I wish `convert` were better at unification.
-  convert ((continuous_fst.tendsto q).sub <| tendsto_const_nhds (a := q.fst)).norm.add
-    ((continuous_snd.tendsto q).sub <| tendsto_const_nhds (a := q.snd)).norm
+  convert ((continuous_fst.tendsto q).sub <| tendsto_const_nhds).norm.add
+    ((continuous_snd.tendsto q).sub <| tendsto_const_nhds).norm
   simp
 #align normed_lattice_add_comm_group_has_continuous_inf NormedLatticeAddCommGroup.continuousInf
 

Mathlib/CategoryTheory/Adjunction/Opposites.lean

@@ -226,9 +226,9 @@ theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (a
     (adj2 : F ⊣ G') (x : D) :
     (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x := by
   apply Quiver.Hom.op_inj
-  -- Porting note: is `convert` more aggresive in Lean4?
   convert homEquiv_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ F adj2)
-    (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
+    (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x)
+  -- Porting note: was `simpa`
   simp only [opAdjointOpOfAdjoint, Functor.op_obj, Opposite.unop_op, mkOfHomEquiv_unit_app,
     Equiv.trans_apply, homEquiv_counit, Functor.id_obj]
   erw [F.map_id] -- Porting note: Yet another `erw`...

Mathlib/CategoryTheory/Category/Basic.lean

@@ -294,16 +294,12 @@ theorem cancel_mono (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} : g ≫ f = h ≫ f 
 #align category_theory.cancel_mono CategoryTheory.cancel_mono
 
 theorem cancel_epi_id (f : X ⟶ Y) [Epi f] {h : Y ⟶ Y} : f ≫ h = f ↔ h = 𝟙 Y := by
-  -- Porting note: `convert` became less powerful!
-  -- It used to suffice to write `cancel_epi f` here.
-  convert @cancel_epi _ _ _ _ _ f _ h (𝟙 Y)
+  convert cancel_epi f
   simp
 #align category_theory.cancel_epi_id CategoryTheory.cancel_epi_id
 
 theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g = 𝟙 X := by
-  -- Porting note: `convert` became less powerful!
-  -- It used to suffice to write `cancel_mono f` here.
-  convert @cancel_mono _ _ _ _ _ f _ g (𝟙 X)
+  convert cancel_mono f
   simp
 #align category_theory.cancel_mono_id CategoryTheory.cancel_mono_id