chore: fix two porting notes (#11682)

Fix two porting notes (one that should have been a porting note!) while looking at `on_goals`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Analysis/Analytic/Constructions.lean

@@ -46,14 +46,14 @@ lemma FormalMultilinearSeries.radius_prod_eq_min
     rw [le_min_iff]
     have := (p.prod q).isLittleO_one_of_lt_radius hr
     constructor
-    all_goals { -- kludge, there is no "work_on_goal" in Lean 4?
+    all_goals
       apply FormalMultilinearSeries.le_radius_of_isBigO
       refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
       rw [norm_mul, norm_norm, norm_mul, norm_norm]
       refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
       rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]
-      try apply le_max_left
-      try apply le_max_right }
+    · apply le_max_left
+    · apply le_max_right
   · refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
     rw [lt_min_iff] at hr
     have := ((p.isLittleO_one_of_lt_radius hr.1).add

Mathlib/Data/Nat/Bitwise.lean

@@ -451,14 +451,7 @@ theorem xor_trichotomy {a b c : ℕ} (h : a ≠ b ^^^ c) :
   on_goal 2 => right; left; rw [hac]
   on_goal 3 => right; right; rw [hab]
   all_goals
-    exact lt_of_testBit i (by
-      -- Porting note: this was originally `simp [h, hi]`
-      rw [Nat.testBit_xor, h, Bool.xor, Bool.true_xor, hi]
-      rfl
-    ) h fun j hj => by
-      -- Porting note: this was originally `simp [hi' _ hj]`
-      rw [Nat.testBit_xor, hi' _ hj, Bool.xor, Bool.xor_false, eq_self_iff_true]
-      trivial
+    exact lt_of_testBit i (by simp [h, hi]) h fun j hj => by simp [hi' _ hj]
 #align nat.lxor_trichotomy Nat.xor_trichotomy
 
 theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b < c :=