chore(data/real/ennreal): move x ≠ 0 case of mul_infi to `mul_inf…

…i_of_ne` (#8345)

src/data/real/ennreal.lean

@@ -1522,20 +1522,36 @@ finset.induction_on s (by simp) $ assume a s ha ih,
       assume a ha, (hk _ $ finset.mem_insert_of_mem ha).right⟩,
   by simp [ha, ih.symm, infi_add_infi this]
 
+/-- If `x ≠ 0` and `x ≠ ∞`, then right multiplication by `x` maps infimum to infimum.
+See also `ennreal.infi_mul` that assumes `[nonempty ι]` but does not require `x ≠ 0`. -/
+lemma infi_mul_of_ne {ι} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x ≠ 0) (h : x ≠ ∞) :
+  infi f * x = ⨅ i, f i * x :=
+le_antisymm
+  mul_right_mono.map_infi_le
+  ((div_le_iff_le_mul (or.inl h0) $ or.inl h).mp $ le_infi $
+    λ i, (div_le_iff_le_mul (or.inl h0) $ or.inl h).mpr $ infi_le _ _)
 
+/-- If `x ≠ ∞`, then right multiplication by `x` maps infimum over a nonempty type to infimum. See
+also `ennreal.infi_mul_of_ne` that assumes `x ≠ 0` but does not require `[nonempty ι]`. -/
 lemma infi_mul {ι} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ≠ ∞) :
-  infi f * x = ⨅i, f i * x :=
+  infi f * x = ⨅ i, f i * x :=
 begin
-  by_cases h2 : x = 0, simp only [h2, mul_zero, infi_const],
-  refine le_antisymm
-    (le_infi $ λ i, mul_right_mono $ infi_le _ _)
-    ((div_le_iff_le_mul (or.inl h2) $ or.inl h).mp $ le_infi $
-      λ i, (div_le_iff_le_mul (or.inl h2) $ or.inl h).mpr $ infi_le _ _)
+  by_cases h0 : x = 0,
+  { simp only [h0, mul_zero, infi_const] },
+  { exact infi_mul_of_ne h0 h }
 end
 
+/-- If `x ≠ ∞`, then left multiplication by `x` maps infimum over a nonempty type to infimum. See
+also `ennreal.mul_infi_of_ne` that assumes `x ≠ 0` but does not require `[nonempty ι]`. -/
 lemma mul_infi {ι} [nonempty ι] {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h : x ≠ ∞) :
-  x * infi f = ⨅i, x * f i :=
-by { rw [mul_comm, infi_mul h], simp only [mul_comm], assumption }
+  x * infi f = ⨅ i, x * f i :=
+by simpa only [mul_comm] using infi_mul h
+
+/-- If `x ≠ 0` and `x ≠ ∞`, then left multiplication by `x` maps infimum to infimum.
+See also `ennreal.mul_infi` that assumes `[nonempty ι]` but does not require `x ≠ 0`. -/
+lemma mul_infi_of_ne {ι} {f : ι → ℝ≥0∞} {x : ℝ≥0∞} (h0 : x ≠ 0) (h : x ≠ ∞) :
+  x * infi f = ⨅ i, x * f i :=
+by simpa only [mul_comm] using infi_mul_of_ne h0 h
 
 /-! `supr_mul`, `mul_supr` and variants are in `topology.instances.ennreal`. -/