awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
simp only [sSup_eq_iSup, iSup_mul]

Premises used: sSup_eq_iSup, ENNReal.iSup_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ iSup f / a = ⨆ (i : ι), f i / a

Tactic:
iSup_mul ..

Premises used: DivInvMonoid.div', ENNReal.iSup_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ sSup s / a = ⨆ b ∈ s, b / a

Tactic:
sSup_mul ..

Premises used: DivInvMonoid.div', ENNReal.sSup_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
inl :
  ∀ (hinfty : Eq (α := ℝ≥0∞) 0 ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
    (h₀ : Eq (α := ℝ≥0∞) 0 0 → Nonempty ι), HMul.hMul (α := ℝ≥0∞) 0 (⨅ (i : ι), f i) = ⨅ (i : ι), 0 * f i
inr : ∀ (ha₀ : a ≠ 0), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) 0 ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) 0 0 → Nonempty ι
⊢ HMul.hMul (α := ℝ≥0∞) 0 (⨅ (i : ι), f i) = ⨅ (i : ι), 0 * f i

Tactic:
simp [h₀ rfl]

Premises used: rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
ha₀ : a ≠ 0
inr :
  ∀ (hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0)
    (h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι) (ha₀ : Ne (α := ℝ≥0∞) ∞ 0),
    HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
inr₁ : ∀ (ha : a ≠ ∞), a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
inr : ∀ (i : ι) (hi : f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
inr₁ : ∀ (hf : ¬∃ (i : ι), f i = 0), HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i

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

Premises used: Exists, em, OfNat.ofNat, Eq
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
inr : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), ∞ * f i < b
inr₁ : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), f i < b
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i

Tactic:
rw [iInf_eq_bot.2, iInf_eq_bot.2, bot_eq_zero, mul_zero]

Premises used: Iff.mpr, ENNReal.bot_eq_zero, MulZeroClass.mul_zero, iInf_eq_bot
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
x : ℝ≥0∞
h : ⊥ < x
⊢ ∞ * f i < x

Tactic:
simpa [hi]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), ∞ * f i < b

Tactic:
exact fun _ _ ↦ ⟨i, by simpa [hi]⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
x : ℝ≥0∞
h : ⊥ < x
⊢ f i < x

Tactic:
simpa [hi]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), f i < b

Tactic:
exact fun _ _ ↦ ⟨i, by simpa [hi]⟩
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
hf : ¬∃ (i : ι), f i = 0
inr : ∀ (i : ι), ∞ * f i = ∞
⊢ HMul.hMul (α := ℝ≥0∞) ∞ (⨅ (i : ι), f i) = ⨅ (i : ι), ∞ * f i

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

Premises used: iInf_eq_top, mt, eq_comm, ENNReal.top_mul, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
hf : ¬∃ (i : ι), f i = 0
⊢ ∀ (i : ι), ∞ * f i = ∞

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

Premises used: ENNReal.top_mul, Exists.intro
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : Eq (α := ℝ≥0∞) ∞ ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : Eq (α := ℝ≥0∞) ∞ 0 → Nonempty ι
ha₀ : Ne (α := ℝ≥0∞) ∞ 0
hf : ¬∃ (i : ι), f i = 0
⊢ ∀ (i : ι), ∞ * f i = ∞

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

Premises used: ENNReal.top_mul, Exists.intro
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (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:
(mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iInf _

Premises used: Iff.mpr, OrderIso.map_iInf, And.intro, ENNReal.mulLeftOrderIso, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (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 _

Premises used: Iff.mpr, OrderIso.map_iInf, And.intro, ENNReal.mulLeftOrderIso, ENNReal.isUnit_iff
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = 0 → Nonempty ι
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Tactic:
simpa only [mul_comm a] using mul_iInf' hinfty h₀

Premises used: ENNReal.mul_iInf', mul_comm
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0

Tactic:
simp [ha]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = 0 → Nonempty ι

Tactic:
simp [ha₀]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
mul_iInf' hinfty fun _ ↦ ‹Nonempty ι›

Premises used: ENNReal.mul_iInf'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
hinfty : a = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Tactic:
iInf_mul' hinfty fun _ ↦ ‹Nonempty ι›

Premises used: ENNReal.iInf_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = ∞ → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
h₀ : a = ∞ → Nonempty ι
⊢ a⁻¹ = 0 → Nonempty ι

Tactic:
simpa
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = 0 → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0

Tactic:
simp [ha₀]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ a = ∞ → Nonempty ι

Tactic:
simp [ha]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
hinfty : a = 0 → Eq (α := ℝ≥0∞) (⨅ (i : ι), f i) 0 → ∃ (i : ι), f i = 0
⊢ (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

Tactic:
iInf_div' hinfty fun _ ↦ ‹Nonempty ι›

Premises used: ENNReal.iInf_div'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), f i)⁻¹ (⨆ (i : ι), (f i)⁻¹)

Tactic:
OrderIso.invENNReal.map_iInf _

Premises used: OrderIso.invENNReal, iSup, setOf, OrderIso.map_iInf, ENNReal, WithTop, ite
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), f i)⁻¹ (⨅ (i : ι), (f i)⁻¹)

Tactic:
OrderIso.invENNReal.map_iSup _

Premises used: OrderIso.invENNReal, iInf, OrderIso.map_iSup, setOf, ENNReal, WithTop, ite
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
s : Set ℝ≥0∞
⊢ (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Tactic:
simp [sInf_eq_iInf, inv_iInf]

Premises used: ENNReal.inv_iInf, sInf_eq_iInf
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
s : Set ℝ≥0∞
⊢ (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹

Tactic:
simp [sSup_eq_iSup, inv_iSup]

Premises used: ENNReal.inv_iSup, sSup_eq_iSup
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Type u_3
u v : ι → ℝ≥0∞
⊢ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), u i) (⨅ (i : ι), v i) ≤ ⨅ (i : ι), u i * v i

Tactic:
le_iInf fun i ↦ mul_le_mul' (iInf_le u i) (iInf_le v i)

Premises used: le_iInf, iInf_le, mul_le_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Type u_3
u v : ι → ℝ≥0∞
⊢ ⨆ (i : ι), u i * v i ≤ HMul.hMul (α := ℝ≥0∞) (⨆ (i : ι), u i) (⨆ (i : ι), v i)

Tactic:
iSup_le fun i ↦ mul_le_mul' (le_iSup u i) (le_iSup v i)

Premises used: le_iSup, iSup_le, mul_le_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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
rw : a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), f i) (⨅ (j : κ), g j)

Tactic:
rw [← iInf_ne_top_subtype]

Premises used: iInf_ne_top_subtype
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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
⊢ Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }

Tactic:
have := nonempty_subtype.2 hf
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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.{max 1 u_1} { a : ι // f a ≠ ∞ }
⊢ Nonempty κ

Tactic:
have := hg.nonempty
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
⊢ Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞

Tactic:
simpa using hg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
⊢ Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞

Tactic:
replace hg : ⨅ j, g j ≠ ∞ := by simpa using hg
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
hg : Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞
rw : ∀ (i : { i : ι // f i ≠ ∞ }), a ≤ f (↑i : ι) * ⨅ (j : κ), g j
⊢ a ≤ HMul.hMul (α := ℝ≥0∞) (⨅ (i : { i : ι // f i ≠ ∞ }), f (↑i : ι)) (⨅ (j : κ), g j)

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

Premises used: False.elim, le_iInf_iff, ENNReal.iInf_mul
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : 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_1 : Nonempty.{max 1 u_1} { a : ι // f a ≠ ∞ }
this : Nonempty κ
hg : Ne (α := ℝ≥0∞) (⨅ (j : κ), g j) ∞
i : ι
hi : f i ≠ ∞
⊢ a ≤ f (↑(Subtype.mk (p := fun (i : ι) ↦ f i ≠ ∞) i hi) : ι) * ⨅ (j : κ), g j

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

Premises used: ENNReal.mul_iInf, False.elim
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
⊢ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), f i) (⨅ (i : ι), g i) = ⨅ (i : ι), f i * g i

Tactic:
le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
    (le_iInf_mul_iInf hf hg fun i j ↦ ?_)

Premises used: le_iInf, ENNReal.le_iInf_mul_iInf, le_antisymm, iInf_le, mul_le_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
refine : ∀ (i j : ι), ⨅ (i : ι), f i * g i ≤ f i * g j
⊢ HMul.hMul (α := ℝ≥0∞) (⨅ (i : ι), f i) (⨅ (i : ι), g i) = ⨅ (i : ι), f i * g i

Tactic:
refine le_antisymm (le_iInf fun i ↦ mul_le_mul' (iInf_le ..) (iInf_le ..))
    (le_iInf_mul_iInf hf hg fun i j ↦ ?_)

Premises used: le_iInf, ENNReal.le_iInf_mul_iInf, le_antisymm, iInf_le, mul_le_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
i j : ι
obtain : ∀ (k : ι) (hk : f k * g k ≤ f i * g j), ⨅ (i : ι), f i * g i ≤ f i * g j
⊢ ⨅ (i : ι), f i * g i ≤ f i * g j

Tactic:
obtain ⟨k, hk⟩ := h i j
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ (i : ι), f i * g i ≤ f i * g j

Tactic:
iInf_le_of_le k hk

Premises used: iInf_le_of_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
hf : ∃ (i : ι), f i ≠ ∞
hg : ∃ (j : ι), g j ≠ ∞
h : ∀ (i j : ι), ∃ (k : ι), f k * g k ≤ f i * g j
i j k : ι
hk : f k * g k ≤ f i * g j
⊢ ⨅ (i : ι), f i * g i ≤ f i * g j

Tactic:
exact iInf_le_of_le k hk

Premises used: iInf_le_of_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
ι : Sort u_1
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : ι → ℝ≥0∞
c : R
⊢ HSMul.hSMul (β := ℝ≥0∞) c (⨆ (i : ι), f i) = ⨆ (i : ι), c • f i

Tactic:
simp only [← smul_one_mul c (f _), ← smul_one_mul c (iSup _), ENNReal.mul_iSup]

Premises used: iSup, smul_one_mul, ENNReal.mul_iSup
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
simp_rw : HSMul.hSMul (β := ℝ≥0∞) c 1 * sSup s = ⨆ a ∈ s, c • a
simp_rw₁ : Eq (α := ℝ≥0∞) (⨆ b ∈ s, HSMul.hSMul (β := ℝ≥0∞) c 1 * b) (⨆ a ∈ s, c • a)
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
simp_rw [← smul_one_mul c (sSup s), ENNReal.mul_sSup, smul_one_mul]

Premises used: ENNReal.mul_sSup, smul_one_mul, SupSet.sSup
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ
hx : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
simp [hx]
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ
hx : 0 < x
rw : (↑x⁻¹.toNNReal : ℝ≥0∞) = (ENNReal.ofReal x)⁻¹
rw₁ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal : ℝ≥0∞)⁻¹
rw₂ : (↑x⁻¹.toNNReal : ℝ≥0∞) = (↑x.toNNReal⁻¹ : ℝ≥0∞)
rw₃ : x⁻¹.toNNReal = x.toNNReal⁻¹
rw₄ rw₅ : x⁻¹.toNNReal = x⁻¹.toNNReal
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]

Premises used: ENNReal.coe_inv, ENNReal.ofReal, ENNReal.coe_inj, Real.toNNReal_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ
inl : ∀ (hx : 0 < x), ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
inr : ∀ (hx : x ≤ 0), ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
obtain hx | hx := lt_or_ge 0 x

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
simp [ofReal_inv_of_pos hx]

Premises used: ENNReal.ofReal_inv_of_pos
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x : ℝ
hx : x ≤ 0
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
simp [ofReal_of_nonpos hx]

Premises used: ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ
hy : 0 ≤ y
simp_rw : ENNReal.ofReal x * ENNReal.ofReal y⁻¹ ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
⊢ ENNReal.ofReal (x / y) ≤ ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
simp_rw [div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy)]

Premises used: Iff.mpr, div_eq_mul_inv, inv_nonneg, ENNReal.ofReal_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ
hy : 0 ≤ y
bc : ENNReal.ofReal y⁻¹ ≤ (ENNReal.ofReal y)⁻¹
⊢ ENNReal.ofReal x * ENNReal.ofReal y⁻¹ ≤ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹

Tactic:
gcongr
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal y⁻¹ ≤ (ENNReal.ofReal y)⁻¹

Tactic:
ofReal_inv_le

Premises used: ENNReal.ofReal_inv_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ
hy : 0 ≤ y
⊢ ENNReal.ofReal y⁻¹ ≤ (ENNReal.ofReal y)⁻¹

Tactic:
exact ofReal_inv_le

Premises used: ENNReal.ofReal_inv_le
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
x y : ℝ
hy : 0 < y
rw : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x / ENNReal.ofReal y
rw₁ : ENNReal.ofReal (x * y⁻¹) = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
rw₂ : ENNReal.ofReal x * ENNReal.ofReal y⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
rw₃ rw₄ : ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]

Premises used: Iff.mpr, LT.lt.le, div_eq_mul_inv, ENNReal.ofReal_inv_of_pos, inv_nonneg, ENNReal.ofReal_mul'
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ ENNReal.toNNReal ∞⁻¹ = (ENNReal.toNNReal ∞)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
coe : (↑0 : ℝ≥0∞)⁻¹.toNNReal = (↑0 : ℝ≥0∞).toNNReal⁻¹
coe₁ : ∀ (ha : a ≠ 0), (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
⊢ (↑0 : ℝ≥0∞)⁻¹.toNNReal = (↑0 : ℝ≥0∞).toNNReal⁻¹

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0
ha : a ≠ 0
coe : (↑a⁻¹ : ℝ≥0∞).toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
coe₁ : a⁻¹ = (↑a : ℝ≥0∞).toNNReal⁻¹
coe₂ coe₃ : a⁻¹ = a⁻¹
⊢ (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹

Tactic:
rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

Premises used: ENNReal.coe_inv, ENNReal.toNNReal_coe
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
top : ENNReal.toNNReal ∞⁻¹ = (ENNReal.toNNReal ∞)⁻¹
coe : ∀ (a : ℝ≥0), (↑a : ℝ≥0∞)⁻¹.toNNReal = (↑a : ℝ≥0∞).toNNReal⁻¹
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹

Tactic:
cases a with
  | top => simp
  | coe a =>
    rcases eq_or_ne a 0 with (rfl | ha); · simp
    rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toNNReal = a.toNNReal / b.toNNReal
rw₁ : a.toNNReal * b⁻¹.toNNReal = a.toNNReal / b.toNNReal
rw₂ : a.toNNReal * b.toNNReal⁻¹ = a.toNNReal / b.toNNReal
rw₃ rw₄ : a.toNNReal * b.toNNReal⁻¹ = a.toNNReal * b.toNNReal⁻¹
⊢ (a / b).toNNReal = a.toNNReal / b.toNNReal

Tactic:
rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv, ENNReal.toNNReal_mul, ENNReal.toNNReal_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a : ℝ≥0∞
⊢ a⁻¹.toReal = a.toReal⁻¹

Tactic:
simp only [ENNReal.toReal, toNNReal_inv, NNReal.coe_inv]

Premises used: NNReal.coe_inv, ENNReal.toReal, ENNReal.toNNReal_inv
-- Module: Mathlib.Data.ENNReal.Inv
Goal:
a b : ℝ≥0∞
rw : (a * b⁻¹).toReal = a.toReal / b.toReal
rw₁ : a.toReal * b⁻¹.toReal = a.toReal / b.toReal
rw₂ : a.toReal * b.toReal⁻¹ = a.toReal / b.toReal
rw₃ rw₄ : a.toReal * b.toReal⁻¹ = a.toReal * b.toReal⁻¹
⊢ (a / b).toReal = a.toReal / b.toReal

Tactic:
rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]

Premises used: ENNReal.toReal_inv, div_eq_mul_inv, ENNReal.toReal_mul
-- Module: Mathlib.Data.ENNReal.Lemmas
Goal:
α : Type u_2
s : Set α
f : α → ℝ≥0
a : α
⊢ (↑(s.indicator f a) : ℝ≥0∞) = s.indicator (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) a

Tactic:
map_indicator ofNNRealHom _ _ _

Premises used: ENNReal.ofNNReal, WithTop.some, map_indicator, ENNReal.ofNNRealHom
-- Module: Mathlib.Data.ENNReal.Lemmas
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0
⊢ (↑(s.sup f) : ℝ≥0∞) = s.sup fun (x : α) ↦ (↑(f x) : ℝ≥0∞)

Tactic:
Finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl

Premises used: Finset.comp_sup_eq_sup_comp_of_is_total, ENNReal.ofNNReal, Set.Ici, Set.Mem, setOf, NNReal, WithTop.some, ENNReal.coe_mono, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c d : ℝ≥0∞
ac : a < c
bd : b < d
⊢ a * b < c * d

Tactic:
WithTop.mul_lt_mul ac bd

Premises used: WithTop.mul_lt_mul
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictMono (β := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ n

Tactic:
WithTop.pow_right_strictMono hn

Premises used: WithTop.pow_right_strictMono, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ b ^ n ↔ a ≤ b

Tactic:
(ENNReal.pow_right_strictMono hn).le_iff_le

Premises used: ENNReal.pow_right_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
n : ℕ
hn : n ≠ 0
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
(ENNReal.pow_right_strictMono hn).lt_iff_lt

Premises used: ENNReal.pow_right_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
n : ℕ
h : a ≤ b
⊢ a ^ n ≤ b ^ n

Tactic:
pow_le_pow_left' h n

Premises used: pow_le_pow_left'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h₀ : a ≠ 0
hinf : a ≠ ∞
⊢ StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ x * a

Tactic:
WithTop.mul_left_strictMono (pos_iff_ne_zero.2 h₀) hinf

Premises used: Iff.mpr, ENNReal, WithTop.mul_left_strictMono, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
h₀ : a ≠ 0
hinf : a ≠ ∞
⊢ StrictMono (β := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ a * x

Tactic:
WithTop.mul_right_strictMono (pos_iff_ne_zero.2 h₀) hinf

Premises used: Iff.mpr, ENNReal, pos_iff_ne_zero, WithTop.mul_right_strictMono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ∞
bc : b < c
⊢ a * b < a * c

Tactic:
ENNReal.mul_right_strictMono h0 hinf bc

Premises used: ENNReal.mul_right_strictMono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ∞
bc : b < c
⊢ b * a < c * a

Tactic:
mul_comm b a ▸ mul_comm c a ▸ ENNReal.mul_right_strictMono h0 hinf bc

Premises used: Eq.rec, ENNReal.mul_right_strictMono, mul_comm, Eq.symm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ∞
⊢ a * b = a * c ↔ b = c

Tactic:
(mul_right_strictMono h0 hinf).injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, ENNReal.mul_right_strictMono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : c ≠ 0
hinf : c ≠ ∞
⊢ a * c = b * c ↔ a = b

Tactic:
mul_comm c a ▸ mul_comm c b ▸ ENNReal.mul_right_inj h0 hinf

Premises used: Eq.rec, ENNReal.mul_right_inj, mul_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ∞
⊢ a * b ≤ a * c ↔ b ≤ c

Tactic:
(mul_right_strictMono h0 hinf).le_iff_le

Premises used: ENNReal.mul_right_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : c ≠ 0
hinf : c ≠ ∞
⊢ a * c ≤ b * c ↔ a ≤ b

Tactic:
(mul_left_strictMono h0 hinf).le_iff_le

Premises used: StrictMono.le_iff_le, ENNReal.mul_left_strictMono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h0 : a ≠ 0
hinf : a ≠ ∞
⊢ a * b < a * c ↔ b < c

Tactic:
(mul_right_strictMono h0 hinf).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, ENNReal.mul_right_strictMono