awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_2
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k ≤ f i

Tactic:
apply_rules
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_2
inst : Preorder ι
inst_1 : IsCodirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ g _k ≤ g j

Tactic:
apply_rules
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : ι → Sort u_2
f : (i : ι) → κ i → ℝ≥0∞
⊢ a + ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a + f i j

Tactic:
simp [add_iInf]

Premises used: ENNReal.add_iInf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : ι → Sort u_2
f : (i : ι) → κ i → ℝ≥0∞
⊢ (⨅ (i : ι), ⨅ (j : κ i), f i j) + a = ⨅ (i : ι), ⨅ (j : κ i), f i j + a

Tactic:
simp only [add_comm, add_iInf₂]

Premises used: add_comm, ENNReal.add_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
s : Set ℝ≥0∞
rw : a + ⨅ a ∈ s, a = ⨅ b ∈ s, a + b
rw₁ rw₂ : Eq (α := ℝ≥0∞) (⨅ i ∈ s, a + i) (⨅ b ∈ s, a + b)
⊢ a + sInf s = ⨅ b ∈ s, a + b

Tactic:
rw [sInf_eq_iInf, add_iInf₂]

Premises used: sInf_eq_iInf, ENNReal.add_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
simp_rw : a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b
⊢ a ≤ iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Premises used: ENNReal.add_iInf, ENNReal.iInf_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b

Tactic:
le_iInf₂ h

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ (i : ι), ⨅ (b : κ), f i + g b

Tactic:
exact le_iInf₂ h

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
simp_rw : a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1
⊢ a ≤ HAdd.hAdd (α := ℝ≥0∞) (⨅ (i : ι), ⨅ (qi : q₁ i), f i qi) (⨅ (k : κ), ⨅ (qk : q₂ k), g k qk)

Tactic:
simp_rw [iInf₂_add, add_iInf₂]

Premises used: ENNReal.iInf₂_add, ENNReal.add_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1

Tactic:
le_iInf₂ fun i hi => le_iInf₂ (h i hi)

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
κ : Sort u_2
q₁ : ι → Sort u_3
q₂ : κ → Sort u_4
f : (i : ι) → q₁ i → ℝ≥0∞
g : (k : κ) → q₂ k → ℝ≥0∞
h : ∀ (i : ι) (pi : q₁ i) (k : κ) (qk : q₂ k), a ≤ f i pi + g k qk
⊢ a ≤ ⨅ (i : ι), ⨅ (j : q₁ i), ⨅ (i_1 : κ), ⨅ (j_1 : q₂ i_1), f i j + g i_1 j_1

Tactic:
exact le_iInf₂ fun i hi => le_iInf₂ (h i hi)

Premises used: le_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b = a

Tactic:
le_antisymm ?_ (le_iInf₂ fun b hb ↦ hb.le)

Premises used: LT.lt.le, le_iInf₂, le_antisymm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
refine : ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b ≤ a
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b = a

Tactic:
refine le_antisymm ?_ (le_iInf₂ fun b hb ↦ hb.le)

Premises used: le_iInf₂, le_antisymm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b ≤ a

Tactic:
le_of_forall_gt fun c hac ↦ ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
refine : ∀ (c : ℝ≥0∞) (hac : a < c), ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b ≤ a

Tactic:
refine le_of_forall_gt fun c hac ↦ ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hac : a < c
obtain : ∀ (d : ℝ≥0∞) (had : a < d) (hdc : d < c), ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c

Tactic:
obtain ⟨d, had, hdc⟩ := exists_between hac

Premises used: exists_between
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hac : a < c
d : ℝ≥0∞
had : a < d
hdc : d < c
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c

Tactic:
(iInf₂_le_of_le d had le_rfl).trans_lt hdc

Premises used: le_rfl, iInf₂_le_of_le, LE.le.trans_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
hac : a < c
d : ℝ≥0∞
had : a < d
hdc : d < c
⊢ ⨅ (b : ℝ≥0∞), ⨅ (_ : a < b), b < c

Tactic:
exact (iInf₂_le_of_le d had le_rfl).trans_lt hdc

Premises used: le_rfl, iInf₂_le_of_le, LE.le.trans_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
h : y + z < x
contrapose! : ∀ (h : ∀ (y' : ℝ≥0∞) (_ : y' > y) (z' : ℝ≥0∞) (_ : z' > z), x ≤ y' + z'), x ≤ y + z
⊢ ∃ y' > y, ∃ z' > z, y' + z' < x

Tactic:
contrapose! h
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y z : ℝ≥0∞
h : ∀ (y' : ℝ≥0∞) (_ : y' > y) (z' : ℝ≥0∞) (_ : z' > z), x ≤ y' + z'
⊢ x ≤ y + z

Tactic:
simpa using le_iInf₂_add_iInf₂ h

Premises used: ENNReal.le_iInf₂_add_iInf₂
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ ∀ (i : ι), f i ≠ ∞

Tactic:
hf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
lift :
  ∀ (f : (i : ι) → ℝ≥0),
    ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)
⊢ (iSup f).toNNReal = ⨆ (i : ι), (f i).toNNReal

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
simp_rw : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)

Tactic:
simp_rw [toNNReal_coe]

Premises used: ENNReal.toNNReal_coe
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
pos : ∀ (h : BddAbove (range f)), ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
neg : ∀ (h : ¬BddAbove (range f)), ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i

Tactic:
by_cases h : BddAbove (range f)

Premises used: BddAbove, Set.range
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : BddAbove (range f)
pos : (↑(iSup f) : ℝ≥0∞).toNNReal = ⨆ (i : ι), f i
pos₁ pos₂ : iSup f = ⨆ (i : ι), f i
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i

Tactic:
rw [← coe_iSup h, toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, ENNReal.coe_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : (i : ι) → ℝ≥0
h : ¬BddAbove (range f)
neg : ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = 0
neg₁ : ENNReal.toNNReal ∞ = 0
neg₂ neg₃ : Eq (α := ℝ≥0) 0 0
⊢ ENNReal.toNNReal (⨆ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨆ (i : ι), f i

Tactic:
rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]

Premises used: Iff.mpr, ENNReal.toNNReal_top, NNReal.iSup_of_not_bddAbove, ENNReal.iSup_coe_eq_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
hf : ∀ (i : { x : ℝ≥0∞ // x ∈ s }), (↑i : ℝ≥0∞) ≠ ∞
⊢ (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)

Tactic:
simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)

Premises used: ENNReal.toNNReal_iSup, Subtype.range_coe_subtype, Set.image_eq_range, sSup_range
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toReal = ⨆ (i : ι), (f i).toReal

Tactic:
simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]

Premises used: NNReal.coe_iSup, ENNReal.toNNReal_iSup, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
hf : ∀ r ∈ s, r ≠ ∞
⊢ (sSup s).toReal = sSup (ENNReal.toReal '' s)

Tactic:
simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]

Premises used: Set.image_image, NNReal.coe_sSup, ENNReal.toNNReal_sSup, ENNReal.toReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ (⨆ (i : ι), f i) - a = ⨆ (i : ι), f i - a

Tactic:
le_antisymm (tsub_le_iff_right.2 <| iSup_le fun i => tsub_le_iff_right.1 <| le_iSup (f · - a) i)
    (iSup_le fun _ => tsub_le_tsub (le_iSup _ _) (le_refl a))

Premises used: Iff.mpr, le_refl, HSub.hSub, tsub_le_tsub, le_iSup, tsub_le_iff_right, le_antisymm, Iff.mp, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0

Tactic:
iSup_eq_bot

Premises used: iSup_eq_bot
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
⊢ Eq (α := ℝ≥0∞) (⨆ (x : ι), 0) 0

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), (↑n : ℝ≥0∞)) ∞

Tactic:
iSup_eq_top.2 fun _b hb => ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 hb)

Premises used: Iff.mpr, ENNReal.exists_nat_gt, iSup_eq_top, lt_top_iff_ne_top, Iff.mp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
inl : HAdd.hAdd (α := ℝ≥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.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
⊢ HAdd.hAdd (α := ℝ≥0∞) ∞ (⨆ (i : ι), f i) = ⨆ (i : ι), ∞ + f i

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
i : ι
grw : a + f i ≤ a + f i
i₁ : ι
grw₁ : a + f i ≤ a + f i
i₂ : ι
⊢ a + f i ≤ a + ⨆ (i : ι), f i

Tactic:
grw [← le_iSup]

Premises used: le_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
inr : a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i
⊢ a + ⨆ (i : ι), f i = ⨆ (i : ι), a + f i

Tactic:
refine le_antisymm ?_ <| iSup_le fun i ↦ by grw [← le_iSup]

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i

Tactic:
add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Premises used: le_iSup_of_le, Classical.arbitrary, add_le_of_le_tsub_left_of_le, le_self_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
inr : ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a
⊢ a + ⨆ (i : ι), f i ≤ ⨆ (i : ι), a + f i

Tactic:
refine add_le_of_le_tsub_left_of_le (le_iSup_of_le (Classical.arbitrary _) le_self_add) ?_

Premises used: le_iSup_of_le, Classical.arbitrary, add_le_of_le_tsub_left_of_le, le_self_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a

Tactic:
iSup_le fun i ↦ ENNReal.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Premises used: ENNReal.le_sub_of_add_le_left, le_iSup, HAdd.hAdd, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ ⨆ (i : ι), f i ≤ (⨆ (i : ι), a + f i) - a

Tactic:
exact iSup_le fun i ↦ ENNReal.le_sub_of_add_le_left ha <| le_iSup (a + f ·) i

Premises used: ENNReal.le_sub_of_add_le_left, le_iSup, HAdd.hAdd, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
inst : Nonempty ι
f : ι → ℝ≥0∞
⊢ (⨆ (i : ι), f i) + a = ⨆ (i : ι), f i + a

Tactic:
simp [add_comm, add_iSup]

Premises used: add_comm, ENNReal.add_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℝ≥0∞
⊢ Nonempty.{max 1 u_1} { i : ι // p i }

Tactic:
haveI : Nonempty {i // p i} := nonempty_subtype.2 h
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℝ≥0∞
this : Nonempty.{max 1 u_1} { i : ι // p i }
⊢ a + ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), a + f i

Tactic:
simp only [iSup_subtype', add_iSup]

Premises used: iSup_subtype', ENNReal.add_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ (i : ι), p i
f : ι → ℝ≥0∞
⊢ (⨆ (i : ι), ⨆ (_ : p i), f i) + a = ⨆ (i : ι), ⨆ (_ : p i), f i + a

Tactic:
simp only [add_comm, add_biSup' h]

Premises used: add_comm, ENNReal.add_biSup'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
ι : Type u_3
s : Set ι
hs : s.Nonempty
f : ι → ℝ≥0∞
⊢ a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i

Tactic:
add_biSup' hs _

Premises used: ENNReal.add_biSup'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
ι : Type u_3
s : Set ι
hs : s.Nonempty
f : ι → ℝ≥0∞
⊢ (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a

Tactic:
biSup_add' hs _

Premises used: ENNReal.biSup_add'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
rw : a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b
rw₁ rw₂ : Eq (α := ℝ≥0∞) (⨆ i ∈ s, a + i) (⨆ b ∈ s, a + b)
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
rw [sSup_eq_iSup, add_biSup hs]

Premises used: sSup_eq_iSup, ENNReal.add_biSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
rw : (⨆ a ∈ s, a) + a = ⨆ b ∈ s, b + a
rw₁ rw₂ : Eq (α := ℝ≥0∞) (⨆ i ∈ s, i + a) (⨆ b ∈ s, b + a)
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
rw [sSup_eq_iSup, biSup_add hs]

Premises used: ENNReal.biSup_add, sSup_eq_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
simp_rw : ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]

Premises used: ENNReal.iSup_add, ENNReal.add_iSup
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a

Tactic:
iSup₂_le h

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
inst_1 : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (i_1 : κ), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le h

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
simp_rw : ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (_ : p i), f i) (⨆ (j : κ), ⨆ (_ : q j), g j) ≤ a

Tactic:
simp_rw [biSup_add' hp, add_biSup' hq]

Premises used: ENNReal.biSup_add', ENNReal.add_biSup'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
iSup₂_le fun i hi => iSup₂_le (h i hi)

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
p : ι → Prop
q : κ → Prop
hp : ∃ (i : ι), p i
hq : ∃ (j : κ), q j
g : κ → ℝ≥0∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ (i : ι), ⨆ (_ : p i), ⨆ (i_1 : κ), ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

Premises used: iSup₂_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_3
κ : Type u_4
s : Set ι
t : Set κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → ℝ≥0∞
g : κ → ℝ≥0∞
a : ℝ≥0∞
h : ∀ i ∈ s, ∀ j ∈ t, f i + g j ≤ a
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ i ∈ s, f i) (⨆ j ∈ t, g j) ≤ a

Tactic:
biSup_add_biSup_le' hs ht h

Premises used: ENNReal.biSup_add_biSup_le'
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
inl : IsEmpty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
inr : Nonempty ι → iSup f + iSup g = ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : IsEmpty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Premises used: add_le_add, le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
inr : iSup f + iSup g ≤ ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g = ⨆ (i : ι), f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Premises used: add_le_add, le_iSup, le_antisymm, iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i

Tactic:
iSup_add_iSup_le fun i j => ?_

Premises used: ENNReal.iSup_add_iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
inr : ∀ (i j : ι), f i + g j ≤ ⨆ (i : ι), f i + g i
⊢ iSup f + iSup g ≤ ⨆ (i : ι), f i + g i

Tactic:
refine iSup_add_iSup_le fun i j => ?_

Premises used: ENNReal.iSup_add_iSup_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j : ι
inr : ∀ (k : ι) (hk : f i + g j ≤ f k + g k), f i + g j ≤ ⨆ (i : ι), f i + g i
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
rcases h i j with ⟨k, hk⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
le_iSup_of_le k hk

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f i + g j ≤ f k + g k
h_1 : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ (i : ι), f i + g i

Tactic:
exact le_iSup_of_le k hk

Premises used: le_iSup_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
h₁ : f i ≤ f _k
h₂ : g j ≤ g _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
gcongr
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i ≤ f _k

Tactic:
apply_rules
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Type u_3
inst : Preorder ι
inst_1 : IsDirectedOrder ι
f g : ι → ℝ≥0∞
hf : Monotone f
hg : Monotone g
i j _k : ι
h : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ g j ≤ g _k

Tactic:
apply_rules
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
inl : ∀ (i : ι) (hi : a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
inr : ∀ (h : ¬∃ (i : ι), a < f i), a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Premises used: Exists, em, LT.lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
inl : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), a - f i < b
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]

Premises used: Iff.mpr, ENNReal.bot_eq_zero, LT.lt.le, tsub_eq_zero_iff_le, le_iSup_of_le, iInf_eq_bot
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
x : ℝ≥0∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
simpa [hi.le, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, LT.lt.le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ (i : ι), a - f i < b

Tactic:
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ¬∃ (i : ι), a < f i
⊢ ∀ (x : ι), f x ≤ a

Tactic:
simp_rw [not_exists, not_lt] at h

Premises used: not_exists, not_lt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_

Premises used: ENNReal.le_sub_of_add_le_left, le_iInf, le_iSup, tsub_le_tsub_left, add_le_of_le_tsub_right_of_le, tsub_le_self, le_antisymm, ne_top_of_le_ne_top, Classical.arbitrary, iSup_le, iInf_le_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
inr : ∀ (i : ι), f i ≤ a - ⨅ (i : ι), a - f i
⊢ a - ⨆ (i : ι), f i = ⨅ (i : ι), a - f i

Tactic:
refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
    ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
    add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
    iSup_le fun i ↦ ?_

Premises used: ENNReal.le_sub_of_add_le_left, le_iInf, le_iSup, tsub_le_tsub_left, add_le_of_le_tsub_right_of_le, tsub_le_self, le_antisymm, ne_top_of_le_ne_top, Classical.arbitrary, iSup_le, iInf_le_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
inr : a - (a - f i) ≤ a - ⨅ (i : ι), a - f i
⊢ f i ≤ a - ⨅ (i : ι), a - f i

Tactic:
rw [← sub_sub_cancel ha (h _)]

Premises used: ENNReal.sub_sub_cancel
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ (i : ι), a - f i

Tactic:
tsub_le_tsub_left (iInf_le (a - f ·) i) _

Premises used: HSub.hSub, tsub_le_tsub_left, iInf_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ (i : ι), a - f i

Tactic:
exact tsub_le_tsub_left (iInf_le (a - f ·) i) _

Premises used: HSub.hSub, tsub_le_tsub_left, iInf_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b = a

Tactic:
le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_

Premises used: iSup₂_le, LT.lt.le, le_antisymm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
refine : a ≤ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b
⊢ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b = a

Tactic:
refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
⊢ a ≤ ⨆ (b : ℝ≥0∞), ⨆ (_ : b < a), b

Tactic:
le_of_forall_lt fun c hca ↦ ?_

Premises used: le_of_forall_lt