From 1b157463d03af160009f16485b995f5607e5ad48 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 26 Mar 2024 09:53:40 +0000 Subject: [PATCH] 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 --- Mathlib/Analysis/Analytic/Constructions.lean | 6 +++--- Mathlib/Data/Nat/Bitwise.lean | 9 +-------- 2 files changed, 4 insertions(+), 11 deletions(-) diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index b06ef7696fc99..9d3eade622286 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index 209dac0f3c0ee..629129bed381d 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/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 :=