fix

Author: SnirBroshi

Mathlib/Analysis/Normed/Lp/lpSpace.lean

@@ -469,8 +469,7 @@ theorem norm_nonneg' (f : lp E p) : 0 ≤ ‖f‖ := by
   rcases p.trichotomy with (rfl | rfl | hp)
   · simp [lp.norm_eq_card_dsupport f]
   · rcases isEmpty_or_nonempty α with _i | _i
-    · rw [lp.norm_eq_ciSup]
-      simp [Real.iSup_of_isEmpty]
+    · simp [lp.norm_eq_ciSup]
     inhabit α
     exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)
   · rw [lp.norm_eq_tsum_rpow hp f]

Mathlib/Data/Nat/Lattice.lean

@@ -55,21 +55,15 @@ lemma iSup_of_not_bddAbove {ι : Sort*} {f : ι → ℕ} (h : ¬ BddAbove (Set.r
 
 @[simp]
 theorem sInf_eq_zero {s : Set ℕ} : sInf s = 0 ↔ 0 ∈ s ∨ s = ∅ := by
-  cases eq_empty_or_nonempty s with
-  | inl h => subst h
-             simp only [or_true, InfSet.sInf,
-                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
-  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]
+  rcases eq_empty_or_nonempty s with (rfl | h)
+  · simp [sInf]
+  · simp [h, h.ne_empty, Nat.sInf_def]
 
-@[simp]
 theorem sInf_empty : sInf ∅ = 0 := by
-  rw [sInf_eq_zero]
-  right
-  rfl
+  simp
 
-@[simp]
 theorem iInf_of_empty {ι : Sort*} [IsEmpty ι] (f : ι → ℕ) : iInf f = 0 := by
-  rw [iInf_of_isEmpty, sInf_empty]
+  simp
 
 /-- This combines `Nat.iInf_of_empty` with `ciInf_const`. -/
 @[simp]

Mathlib/Data/Set/Finite/Lattice.lean

@@ -380,7 +380,7 @@ theorem _root_.iInf_iSup_eq_of_finite {ι : Sort v} {κ : ι → Sort w} [Order.
   intro ι κ _ f
   induction ι using Finite.induction_empty_option with
   | of_equiv e h => simp [← e.iInf_comp, ← e.piCongrLeft κ |>.iSup_comp, h]
-  | h_empty => simp [iInf_of_empty, iSup_const]
+  | h_empty => simp [iSup_const]
   | h_option h =>
     simp only [iInf_option, h, ← (Equiv.piOptionEquivProd (β := κ)).symm.iSup_comp,
       Equiv.piOptionEquivProd_symm_apply, iSup_prod, ← inf_iSup_eq, ← iSup_inf_eq]

Mathlib/Order/Filter/Basic.lean

@@ -525,7 +525,7 @@ theorem iInf_neBot_of_directed {f : ι → Filter α} [hn : Nonempty α] (hd : D
     (hb : ∀ i, NeBot (f i)) : NeBot (iInf f) := by
   cases isEmpty_or_nonempty ι
   · constructor
-    simp [iInf_of_empty f, top_ne_bot]
+    simp [top_ne_bot]
   · exact iInf_neBot_of_directed' hd hb
 
 theorem sInf_neBot_of_directed' {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (· ≥ ·) s)

Mathlib/Order/Filter/Lift.lean

@@ -195,7 +195,7 @@ theorem lift_iInf_of_map_univ {f : ι → Filter α} {g : Set α → Filter β}
     (hg : ∀ s t, g (s ∩ t) = g s ⊓ g t) (hg' : g univ = ⊤) :
     (iInf f).lift g = ⨅ i, (f i).lift g := by
   cases isEmpty_or_nonempty ι
-  · simp [iInf_of_empty, hg']
+  · simp [hg']
   · exact lift_iInf hg
 
 end lift