-- Mathlib/Data/ENNReal/Inv.lean
lemma le_iInf_mul_iInf {g : κ → ℝ≥0∞} (hf : ∃ i, f i ≠ ∞) (hg : ∃ j, g j ≠ ∞)
    (ha : ∀ i j, a ≤ f i * g j) : a ≤ (⨅ i, f i) * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f i) * ⨅ j, g j

Tactic:
rw [← iInf_ne_top_subtype]

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Tactic:
rw [iInf_mul fun h ↦ (hg h).elim, le_iInf_iff]

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
⊢ ∀ (i : { i // f i ≠ ⊤ }), a ≤ f ↑i * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this : Nonempty { a // f a ≠ ⊤ }
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Tactic:
have := hg.nonempty

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Tactic:
have := nonempty_subtype.2 hf

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this : Nonempty { a // f a ≠ ⊤ }
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
⊢ ∀ (i : { i // f i ≠ ⊤ }), a ≤ f ↑i * ⨅ j, g j

Tactic:
rintro ⟨i, hi⟩

Result:
case mk
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
i : ι
hi : f i ≠ ⊤
⊢ a ≤ f ↑⟨i, hi⟩ * ⨅ j, g j

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Tactic:
replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg

Result:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
⊢ a ≤ (⨅ i, f ↑i) * ⨅ j, g j

Proof state:
case mk
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ⊤
i : ι
hi : f i ≠ ⊤
⊢ a ≤ f ↑⟨i, hi⟩ * ⨅ j, g j

Tactic:
simpa [mul_iInf fun h ↦ (hi h).elim] using ha i

Result:
no goals

Proof state:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ⊤
hg : ∃ j, g j ≠ ⊤
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ⊤ }
this : Nonempty κ
⊢ ⨅ j, g j ≠ ⊤

Tactic:
simpa using hg

Result:
no goals