feat(Data/ENat/Lattice): fill in proof_wanted (#24201)

Fills in two `proof_wanted`s (`ENat.smul_iSup` and `ENat.smul_sSup`).

Author: plp127

Mathlib/Data/ENat/Lattice.lean

@@ -15,12 +15,6 @@ This instance is not in `Data.ENat.Basic` to avoid dependency on `Finset`s.
 We also restate some lemmas about `WithTop` for `ENat` to have versions that use `Nat.cast` instead
 of `WithTop.some`.
 
-## TODO
-
-Currently (2024-Nov-12), `shake` does not check `proof_wanted` and insist that
-`Mathlib.Algebra.Group.Action.Defs` should not be imported. Once `shake` is fixed, please remove the
-corresponding `noshake.json` entry.
-
 -/
 
 assert_not_exists Field
@@ -238,11 +232,13 @@ lemma iSup_add_iSup_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· 
     (hf : Monotone f) (hg : Monotone g) : iSup f + iSup g = ⨆ a, f a + g a :=
   iSup_add_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ ↦ by gcongr <;> apply_rules
 
-proof_wanted smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) :
-    c • ⨆ i, f i = ⨆ i, c • f i
+lemma smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) :
+    c • ⨆ i, f i = ⨆ i, c • f i := by
+  simpa using mul_iSup (c • 1) f
 
-proof_wanted smul_sSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R) :
-    c • sSup s = ⨆ a ∈ s, c • a
+lemma smul_sSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R) :
+    c • sSup s = ⨆ a ∈ s, c • a := by
+  simp_rw [sSup_eq_iSup, smul_iSup]
 
 lemma sub_iSup [Nonempty ι] (ha : a ≠ ⊤) : a - ⨆ i, f i = ⨅ i, a - f i := by
   obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

scripts/noshake.json

@@ -442,7 +442,6 @@
   "Mathlib.Data.FunLike.Basic": ["Mathlib.Logic.Function.Basic"],
   "Mathlib.Data.Finsupp.Notation": ["Mathlib.Data.Finsupp.Single"],
   "Mathlib.Data.Finset.Insert": ["Mathlib.Data.Finset.Attr"],
-  "Mathlib.Data.ENat.Lattice": ["Mathlib.Algebra.Group.Action.Defs"],
   "Mathlib.Data.ByteArray": ["Batteries.Data.ByteSubarray"],
   "Mathlib.Data.Bool.Basic": ["Batteries.Tactic.Init"],
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],