awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a b : ℝ≥0∞
h : a = ∞ → b = ∞
h_nnreal : a ≠ ∞ → b ≠ ∞ → a.toNNReal ≤ b.toNNReal
hlt : b < a
lift :
  ∀ (b : ℝ≥0) (h : a = ∞ → (↑b : ℝ≥0∞) = ∞) (h_nnreal : a ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → a.toNNReal ≤ (↑b : ℝ≥0∞).toNNReal)
    (hlt : (↑b : ℝ≥0∞) < a), False
⊢ False

Tactic:
lift b to ℝ≥0 using hlt.ne_top

Premises used: LT.lt.ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : a ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → a.toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < a
⊢ a ≠ ∞

Tactic:
mt h coe_ne_top

Premises used: mt, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
a : ℝ≥0∞
b : ℝ≥0
h : a = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : a ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → a.toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < a
lift :
  ∀ (a : ℝ≥0) (h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞)
    (h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal)
    (hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)), False
⊢ False

Tactic:
lift a to ℝ≥0 using mt h coe_ne_top

Premises used: mt, ENNReal.coe_ne_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b a : ℝ≥0
h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)
⊢ False

Tactic:
hlt.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b a : ℝ≥0
h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)
refine : (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)
⊢ False

Tactic:
refine hlt.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
b a : ℝ≥0
h : (↑a : ℝ≥0∞) = ∞ → (↑b : ℝ≥0∞) = ∞
h_nnreal : (↑a : ℝ≥0∞) ≠ ∞ → (↑b : ℝ≥0∞) ≠ ∞ → (↑a : ℝ≥0∞).toNNReal ≤ (↑b : ℝ≥0∞).toNNReal
hlt : (↑b : ℝ≥0∞) < (↑a : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) ≤ (↑b : ℝ≥0∞)

Tactic:
simpa using h_nnreal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0∞
top : |ENNReal.toReal ∞| = ENNReal.toReal ∞
coe : ∀ (x : ℝ≥0), |(↑x : ℝ≥0∞).toReal| = (↑x : ℝ≥0∞).toReal
⊢ |x.toReal| = x.toReal

Tactic:
cases x
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
⊢ |ENNReal.toReal ∞| = ENNReal.toReal ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
x : ℝ≥0
⊢ |(↑x : ℝ≥0∞).toReal| = (↑x : ℝ≥0∞).toReal

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
s : Set ℝ≥0
⊢ BddAbove s → (↑(sSup s) : ℝ≥0∞) = ⨆ a ∈ s, (↑a : ℝ≥0∞)

Tactic:
WithTop.coe_sSup

Premises used: ENNReal.ofNNReal, WithTop.coe_sSup, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
s : Set ℝ≥0
hs : s.Nonempty
⊢ (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, (↑a : ℝ≥0∞)

Tactic:
WithTop.coe_sInf hs (OrderBot.bddBelow s)

Premises used: ENNReal.ofNNReal, ENNReal, OrderBot.bddBelow, WithTop.coe_sInf
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_3
f : ι → ℝ≥0
hf : BddAbove (range f)
⊢ (↑(iSup f) : ℝ≥0∞) = ⨆ (a : ι), (↑(f a) : ℝ≥0∞)

Tactic:
WithTop.coe_iSup _ hf

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.coe_iSup
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_3
inst : Nonempty ι
f : ι → ℝ≥0
⊢ (↑(iInf f) : ℝ≥0∞) = ⨅ (a : ι), (↑(f a) : ℝ≥0∞)

Tactic:
WithTop.coe_iInf (OrderBot.bddBelow _)

Premises used: ENNReal.ofNNReal, WithTop.coe_iInf, ENNReal, OrderBot.bddBelow
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
r : ℝ≥0
s : Set ℝ≥0
⊢ (↑r : ℝ≥0∞) ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s

Tactic:
simp +contextual [upperBounds, forall_mem_image, -mem_image, *]

Premises used: Set.mem_image, upperBounds, Set.forall_mem_image
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) ∞ ↔ ¬BddAbove (range f)

Tactic:
WithTop.iSup_coe_eq_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.iSup_coe_eq_top
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
⊢ LT.lt (α := ℝ≥0∞) (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) ∞ ↔ BddAbove (range f)

Tactic:
WithTop.iSup_coe_lt_top

Premises used: ENNReal.ofNNReal, WithTop.iSup_coe_lt_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) ∞ ↔ IsEmpty ι

Tactic:
WithTop.iInf_coe_eq_top

Premises used: ENNReal.ofNNReal, WithTop.iInf_coe_eq_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
ι : Sort u_2
f : ι → ℝ≥0
⊢ LT.lt (α := ℝ≥0∞) (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) ∞ ↔ Nonempty ι

Tactic:
WithTop.iInf_coe_lt_top

Premises used: ENNReal.ofNNReal, WithTop.iInf_coe_lt_top, ENNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
u : Set ℝ≥0∞
h : u.OrdConnected
⊢ (ofNNReal ⁻¹' u).OrdConnected

Tactic:
h.preimage_mono ENNReal.coe_mono

Premises used: Set.OrdConnected.preimage_mono, ENNReal.coe_mono
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
t : Set ℝ≥0
h : t.OrdConnected
⊢ (ofNNReal '' t).OrdConnected

Tactic:
⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩

Premises used: Iff.mpr, Set.OrdConnected.mk, Set.forall_mem_image
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
t : Set ℝ≥0
h : t.OrdConnected
refine :
  ∀ (x : ℝ≥0) (hx : x ∈ t) (y : ℝ≥0) (hy : y ∈ t) (z : ℝ≥0∞) (hz : z ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)), z ∈ ofNNReal '' t
⊢ (ofNNReal '' t).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0∞
hz : z ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)
rcases : ∀ (z : ℝ≥0) (hz : (↑z : ℝ≥0∞) ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)), (↑z : ℝ≥0∞) ∈ ofNNReal '' t
⊢ z ∈ ofNNReal '' t

Tactic:
rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩

Premises used: ENNReal.le_coe_iff, And.right, Iff.mp, rfl
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : (↑z : ℝ≥0∞) ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)
⊢ (↑z : ℝ≥0∞) ∈ ofNNReal '' t

Tactic:
mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

Premises used: ENNReal.coe_le_coe, Set.OrdConnected.out, And.right, And.left, Set.mem_image_of_mem, And.intro, Iff.mp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
t : Set ℝ≥0
h : t.OrdConnected
x : ℝ≥0
hx : x ∈ t
y : ℝ≥0
hy : y ∈ t
z : ℝ≥0
hz : (↑z : ℝ≥0∞) ∈ Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)
⊢ (↑z : ℝ≥0∞) ∈ ofNNReal '' t

Tactic:
exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

Premises used: ENNReal.coe_le_coe, Set.OrdConnected.out, And.right, And.left, Set.mem_image_of_mem, And.intro, Iff.mp
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
u : Set ℝ≥0∞
h : u.OrdConnected
⊢ (ENNReal.ofReal ⁻¹' u).OrdConnected

Tactic:
h.preimage_coe_nnreal_ennreal.preimage_real_toNNReal

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, Set.Mem, setOf, NNReal.mk, WithTop.some, Set.OrdConnected.preimage_coe_nnreal_ennreal, Set.preimage, Set.OrdConnected.preimage_real_toNNReal
-- Module: Mathlib.Data.ENNReal.Basic
Goal:
s : Set ℝ
h : s.OrdConnected
⊢ (ENNReal.ofReal '' s).OrdConnected

Tactic:
simpa only [image_image] using h.image_real_toNNReal.image_coe_nnreal_ennreal

Premises used: Set.image_image, Set.OrdConnected.image_real_toNNReal, Set.OrdConnected.image_coe_nnreal_ennreal
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0
⊢ (↑(∑ a ∈ s, f a) : ℝ≥0∞) = ∑ a ∈ s, (↑(f a) : ℝ≥0∞)

Tactic:
map_sum ofNNRealHom f s

Premises used: ENNReal.ofNNReal, map_sum, WithTop.some, ENNReal.ofNNRealHom
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0
⊢ (↑(∏ a ∈ s, f a) : ℝ≥0∞) = ∏ a ∈ s, (↑(f a) : ℝ≥0∞)

Tactic:
map_prod ofNNRealHom f s

Premises used: ENNReal.ofNNReal, map_prod, WithTop.some, ENNReal.ofNNRealHom
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
s : Finset ι
f : ι → ℝ≥0∞
⊢ ENNReal.toNNReal (∏ i ∈ s, f i) = ∏ i ∈ s, (f i).toNNReal

Tactic:
map_prod toNNRealHom _ _

Premises used: ENNReal.toNNRealHom, ENNReal.toNNReal, map_prod, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
s : Finset ι
f : ι → ℝ≥0∞
⊢ ENNReal.toReal (∏ i ∈ s, f i) = ∏ i ∈ s, (f i).toReal

Tactic:
map_prod toRealHom _ _

Premises used: ENNReal.toRealHom, map_prod, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
simp_rw : Real.toNNReal (∏ i ∈ s, f i) = ∏ a ∈ s, (f a).toNNReal
⊢ ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← coe_finsetProd, coe_inj]

Premises used: ENNReal.ofReal, ENNReal.coe_inj, ENNReal.coe_finsetProd
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Real.toNNReal (∏ i ∈ s, f i) = ∏ a ∈ s, (f a).toNNReal

Tactic:
Real.toNNReal_prod_of_nonneg hf

Premises used: Real.toNNReal_prod_of_nonneg
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_2
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Real.toNNReal (∏ i ∈ s, f i) = ∏ a ∈ s, (f a).toNNReal

Tactic:
exact Real.toNNReal_prod_of_nonneg hf

Premises used: Real.toNNReal_prod_of_nonneg
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)

Tactic:
simp only [Finset.sum_empty, ciInf_const]

Premises used: Finset.sum_empty, ciInf_const
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
cons : ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)

Tactic:
simp only [Finset.sum_cons, ← ih]

Premises used: Finset.sum_cons
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)

Tactic:
(iInf_add_iInf fun i j => ?_).symm

Premises used: ENNReal.iInf_add_iInf, Eq.symm
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
cons : ∀ (i j : ι), ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
⊢ ⨅ (i : ι), f i a + ∑ a ∈ s, f i a = HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), f i a) (⨅ (i : ι), ∑ a ∈ s, f i a)

Tactic:
refine (iInf_add_iInf fun i j => ?_).symm

Premises used: ENNReal.iInf_add_iInf, Eq.symm
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j : ι
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
(h (Finset.cons a s ha) i j).imp fun k hk => ?_

Premises used: Finset.cons, Exists.imp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j : ι
cons :
  ∀ (k : ι) (hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1),
    f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a
⊢ ∃ (k : ι), f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_

Premises used: Finset.cons, Exists.imp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j k : ι
hk : ∀ a_1 ∈ Finset.cons a s ha, f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x

Tactic:
rw [Finset.forall_mem_cons] at hk

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: add_le_add, And.right, And.left, Finset.sum_le_sum
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : a ∉ s
ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ x ∈ s, f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a ∈ s, f k a ≤ f i a + ∑ a ∈ s, f j a

Tactic:
exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: add_le_add, And.right, And.left, Finset.sum_le_sum
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_2
α : Type u_3
f : ι → α → ℝ≥0∞
s : Finset α
inst : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
empty : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ ∅, f i a) (∑ a ∈ ∅, ⨅ (i : ι), f i a)
cons :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)),
    Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ Finset.cons a s ha, f i a) (∑ a ∈ Finset.cons a s ha, ⨅ (i : ι), f i a)
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ∑ a ∈ s, f i a) (∑ a ∈ s, ⨅ (i : ι), f i a)

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp only [Finset.sum_empty, ciInf_const]
  | cons a s ha ih =>
    simp only [Finset.sum_cons, ← ih]
    refine (iInf_add_iInf fun i j => ?_).symm
    refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
    rw [Finset.forall_mem_cons] at hk
    exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)

Premises used: Finset.sum_cons, ENNReal.iInf_add_iInf, Finset.forall_mem_cons, Finset.sum_empty, Eq.symm, ciInf_const
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
h : ∀ a ∈ s, f a ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∏ a ∈ s, f a) ∞

Tactic:
WithTop.prod_ne_top h

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.prod_ne_top
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
h : ∀ a ∈ s, f a < ∞
⊢ LT.lt (α := ℝ≥0∞) (∏ a ∈ s, f a) ∞

Tactic:
WithTop.prod_lt_top h

Premises used: WithTop.prod_lt_top, ENNReal.ofNNReal, ENNReal
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, f x) ∞ ↔ ∃ a ∈ s, f a = ∞

Tactic:
WithTop.sum_eq_top

Premises used: ENNReal.ofNNReal, WithTop.sum_eq_top, ENNReal
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
⊢ Ne (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞ ↔ ∀ a ∈ s, f a ≠ ∞

Tactic:
WithTop.sum_ne_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.sum_ne_top
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
⊢ LT.lt (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞ ↔ ∀ a ∈ s, f a < ∞

Tactic:
WithTop.sum_lt_top

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.sum_lt_top
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) (∑ x ∈ s, f x) ∞
a : α
ha : a ∈ s
⊢ f a < ∞

Tactic:
sum_lt_top.1 h.lt_top a ha

Premises used: ENNReal.sum_lt_top, Ne.lt_top, Iff.mp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
rw : ∀ x ∈ s, f x = (↑(f x).toNNReal : ℝ≥0∞)
rw₁ : Ne (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞
⊢ ENNReal.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, coe_toNNReal, coe_finsetSum, sum_congr rfl]

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_finsetSum, ENNReal.coe_inj, Finset.sum_congr, rfl
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
x : α
hx : x ∈ s
⊢ f x = (↑(f x).toNNReal : ℝ≥0∞)

Tactic:
(coe_toNNReal (hf x hx)).symm

Premises used: ENNReal.coe_toNNReal, Eq.symm
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
x : α
hx : x ∈ s
⊢ f x = (↑(f x).toNNReal : ℝ≥0∞)

Tactic:
exact (coe_toNNReal (hf x hx)).symm

Premises used: ENNReal.coe_toNNReal, Eq.symm
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞

Tactic:
sum_ne_top.2 hf

Premises used: Iff.mpr, ENNReal.sum_ne_top
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ Ne (α := ℝ≥0∞) (∑ a ∈ s, f a) ∞

Tactic:
exact sum_ne_top.2 hf

Premises used: Iff.mpr, ENNReal.sum_ne_top
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
rw : Eq (α := ℝ) (∑ i ∈ s, (↑(f i).toNNReal : ℝ)) (∑ a ∈ s, (f a).toReal)
⊢ ENNReal.toReal (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toReal

Tactic:
rw [ENNReal.toReal, toNNReal_sum hf, NNReal.coe_sum]

Premises used: NNReal.coe_sum, ENNReal.toReal, ENNReal.toNNReal_sum
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ Eq (α := ℝ) (∑ i ∈ s, (↑(f i).toNNReal : ℝ)) (∑ a ∈ s, (f a).toReal)

Tactic:
rfl
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
simp_rw : Real.toNNReal (∑ i ∈ s, f i) = ∑ a ∈ s, (f a).toNNReal
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← coe_finsetSum, coe_inj]

Premises used: ENNReal.coe_finsetSum, ENNReal.ofReal, ENNReal.coe_inj
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Real.toNNReal (∑ i ∈ s, f i) = ∑ a ∈ s, (f a).toNNReal

Tactic:
Real.toNNReal_sum_of_nonneg hf

Premises used: Real.toNNReal_sum_of_nonneg
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Real.toNNReal (∑ i ∈ s, f i) = ∑ a ∈ s, (f a).toNNReal

Tactic:
exact Real.toNNReal_sum_of_nonneg hf

Premises used: Real.toNNReal_sum_of_nonneg
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a : α
Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)

Tactic:
simp [Hlt _ (Finset.mem_singleton_self _)]

Premises used: Finset.mem_singleton_self
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : ∀ i ∈ Finset.cons a s_1 h, f i < g i
cons : ∀ (Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x), f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ Finset.cons a s_1 h, f i) (∑ i ∈ Finset.cons a s_1 h, g i)

Tactic:
simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢

Premises used: Finset.sum_cons, Finset.forall_mem_cons
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x
⊢ f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i

Tactic:
ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: And.right, And.left, ENNReal.add_lt_add
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
f g : α → ℝ≥0∞
a : α
s_1 : Finset α
h : a ∉ s_1
hs : s_1.Nonempty
ih : ∀ (Hlt : ∀ i ∈ s_1, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s_1, f i) (∑ i ∈ s_1, g i)
Hlt : f a < g a ∧ ∀ x ∈ s_1, f x < g x
⊢ f a + ∑ i ∈ s_1, f i < g a + ∑ i ∈ s_1, g i

Tactic:
exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: And.right, And.left, ENNReal.add_lt_add
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
singleton :
  ∀ (a : α) (Hlt : ∀ (i : α), Membership.mem (γ := Finset α) {a} i → f i < g i),
    LT.lt (α := ℝ≥0∞) (∑ i ∈ {a}, f i) (∑ i ∈ {a}, g i)
cons :
  ∀ (a : α) (s : Finset α) (h : a ∉ s),
    s.Nonempty →
      ∀ (ih : ∀ (Hlt : ∀ i ∈ s, f i < g i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i))
        (Hlt : ∀ i ∈ Finset.cons a s h, f i < g i),
        LT.lt (α := ℝ≥0∞) (∑ i ∈ Finset.cons a s h, f i) (∑ i ∈ Finset.cons a s h, g i)
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Premises used: Finset.sum_cons, Finset.cons, Finset.forall_mem_cons, Singleton.singleton
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : LE.le (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
contrapose! : ∀ (Hle : ∀ (i : α) (_ : i ∈ s), g i < f i), LT.lt (α := ℝ≥0∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∀ (i : α) (_ : i ∈ s), g i < f i
⊢ LT.lt (α := ℝ≥0∞) (∑ i ∈ s, g i) (∑ i ∈ s, f i)

Tactic:
apply ENNReal.sum_lt_sum_of_nonempty hs Hle

Premises used: ENNReal.sum_lt_sum_of_nonempty
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ ∅, f i)⁻¹ (∏ i ∈ ∅, (f i)⁻¹)

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ Finset.cons i s hi, f i)⁻¹ (∏ i ∈ Finset.cons i s hi, (f i)⁻¹)

Tactic:
?_
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s : Finset ι
hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞),
        Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹))
    (hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞),
    Eq (α := ℝ≥0∞) (∏ i ∈ Finset.cons i s hi, f i)⁻¹ (∏ i ∈ Finset.cons i s hi, (f i)⁻¹)
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih => ?_
-- Module: Mathlib.Data.ENNReal.BigOperators
Goal:
ι : Type u_1
f : ι → ℝ≥0∞
s_1 : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hf : (↑s : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞), Eq (α := ℝ≥0∞) (∏ i ∈ s, f i)⁻¹ (∏ i ∈ s, (f i)⁻¹)
hf : (↑(Finset.cons i s hi) : Set ι).Pairwise fun (i j : ι) ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (↑s : Set ι) ⊆ (↑(Finset.cons i s hi) : Set ι)

Tactic:
simp