-- Mathlib/Data/ENNReal/Inv.lean
/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.mul_iInf_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.mul_iInf` for the special case assuming `Nonempty ι`. -/
lemma mul_iInf' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
    a * ⨅ i, f i = ⨅ i, a * f i

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : x✝¹ > ⊥
⊢ f i < x✝¹

Tactic:
simpa [hi]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Result:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : 0 = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : 0 = 0 → Nonempty ι
⊢ 0 * ⨅ i, f i = ⨅ i, 0 * f i

case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Proof state:
case inr.inl.inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
i : ι
hi : f i = 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

Tactic:
rw [(iInf_eq_bot _).2, (iInf_eq_bot _).2, bot_eq_zero, mul_zero] <;>
  exact fun _ _↦ ⟨i, by simpa [hi]⟩

Result:
no goals

Proof state:
case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _

Result:
no goals

Proof state:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : 0 = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : 0 = 0 → Nonempty ι
⊢ 0 * ⨅ i, f i = ⨅ i, 0 * f i

Tactic:
simp [h₀ rfl]

Result:
no goals

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Result:
case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

case inr.inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Proof state:
case inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

Tactic:
obtain ⟨i, hi⟩ | hf := em (∃ i, f i = 0)

Result:
case inr.inl.inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
i : ι
hi : f i = 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

Proof state:
case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ⊤ * ⨅ i, f i = ⨅ i, ⊤ * f i

Tactic:
rw [top_mul (mt (hinfty rfl) hf), eq_comm, iInf_eq_top]

Result:
case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∀ (i : ι), ⊤ * f i = ⊤

Proof state:
case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ⊤ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ⊤ = 0 → Nonempty ι
ha₀ : ⊤ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∀ (i : ι), ⊤ * f i = ⊤

Tactic:
exact fun i ↦ top_mul fun hi ↦ hf ⟨i, hi⟩

Result:
no goals