awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hb : b ≠ ∞
hab : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
(cancel_of_ne hb).tsub_lt_iff_left hab

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_lt_iff_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
hcb : c ≤ b
⊢ a ≤ b - c ↔ c + a ≤ b

Tactic:
⟨fun h ↦ add_le_of_le_tsub_left_of_le hcb h, le_sub_of_add_le_left hc⟩

Premises used: ENNReal.le_sub_of_add_le_left, Iff.intro, add_le_of_le_tsub_left_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
hc : c ≠ ∞
hcb : c ≤ b
⊢ a ≤ b - c ↔ a + c ≤ b

Tactic:
⟨fun h ↦ add_le_of_le_tsub_right_of_le hcb h, le_sub_of_add_le_right hc⟩

Premises used: ENNReal.le_sub_of_add_le_right, add_le_of_le_tsub_right_of_le, Iff.intro
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
ha₀ : a ≠ 0
hb : b ≠ 0
⊢ a - b < a

Tactic:
(cancel_of_ne ha).tsub_lt_self (pos_iff_ne_zero.2 ha₀) (pos_iff_ne_zero.2 hb)

Premises used: Iff.mpr, AddLECancellable.tsub_lt_self, ENNReal.cancel_of_ne, pos_iff_ne_zero
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
ha : a ≠ ∞
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
(cancel_of_ne ha).tsub_lt_self_iff

Premises used: ENNReal.cancel_of_ne, AddLECancellable.tsub_lt_self_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h₂ : c ≤ a
h₃ : a ≠ ∞ ∨ b ≠ ∞
h₁ : a - b < c
⊢ a - c < b

Tactic:
ENNReal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ENNReal.lt_add_of_sub_lt_right h₃ h₁)

Premises used: Eq.rec, add_comm, ENNReal.lt_add_of_sub_lt_right, ENNReal.sub_lt_of_lt_add
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
h : a ≠ ∞
h2 : b ≤ a
⊢ a - (a - b) = b

Tactic:
(cancel_of_ne <| sub_ne_top h).tsub_tsub_cancel_of_le h2

Premises used: ENNReal.sub_ne_top, ENNReal.cancel_of_ne, AddLECancellable.tsub_tsub_cancel_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
hb : b ≤ a
hc : c ≤ a
⊢ a - b = a - c ↔ b = c

Tactic:
(cancel_of_ne ha).tsub_right_inj (cancel_of_ne <| ne_top_of_le_ne_top ha hb)
    (cancel_of_ne <| ne_top_of_le_ne_top ha hc) hb hc

Premises used: ENNReal.cancel_of_ne, ne_top_of_le_ne_top, AddLECancellable.tsub_right_inj
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
inl : ∀ (hab : a ≤ b), (a - b) * c = a * c - b * c
inr : ∀ (hab : b < a), (a - b) * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c

Tactic:
rcases le_or_gt a b with hab | hab

Premises used: le_or_gt
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

Tactic:
simp [hab, mul_left_mono hab, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le, mul_left_mono
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
inr : ∀ (h : LT.lt (α := ℝ≥0∞) 0 0 → 0 < a → c ≠ ∞) (hab : 0 < a), (a - 0) * c = a * c - 0 * c
inr₁ : ∀ (hb : 0 < b), (a - b) * c = a * c - b * c
⊢ (a - b) * c = a * c - b * c

Tactic:
rcases eq_zero_or_pos b with (rfl | hb)

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a c : ℝ≥0∞
h : LT.lt (α := ℝ≥0∞) 0 0 → 0 < a → c ≠ ∞
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Tactic:
(cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul

Premises used: LT.lt.ne_top, ENNReal.cancel_of_ne, ENNReal.mul_ne_top, AddLECancellable.tsub_mul
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Tactic:
exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul

Premises used: LT.lt.ne_top, ENNReal.cancel_of_ne, ENNReal.mul_ne_top, AddLECancellable.tsub_mul
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ∞
simp : (b - c) * a = b * a - c * a
⊢ a * (b - c) = a * b - a * c

Tactic:
simp only [mul_comm a]

Premises used: mul_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ∞
⊢ (b - c) * a = b * a - c * a

Tactic:
ENNReal.sub_mul h

Premises used: ENNReal.sub_mul
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : 0 < c → c < b → a ≠ ∞
⊢ (b - c) * a = b * a - c * a

Tactic:
exact ENNReal.sub_mul h

Premises used: ENNReal.sub_mul
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
h : c ≤ a
h' : a ≠ ∞
⊢ a - b ≤ a - c ↔ c ≤ b

Tactic:
(cancel_of_ne h').tsub_le_tsub_iff_left (cancel_of_ne (ne_top_of_le_ne_top h' h)) h

Premises used: AddLECancellable.tsub_le_tsub_iff_left, ENNReal.cancel_of_ne, ne_top_of_le_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
⊢ b ≠ ∞

Tactic:
hb
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
lift : ∀ (b : ℝ≥0), a.toReal - (↑b : ℝ≥0∞).toReal ≤ (a - (↑b : ℝ≥0∞)).toReal
⊢ a.toReal - b.toReal ≤ (a - b).toReal

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
b : ℝ≥0
top : ENNReal.toReal ∞ - (↑b : ℝ≥0∞).toReal ≤ (∞ - (↑b : ℝ≥0∞)).toReal
coe : ∀ (x : ℝ≥0), (↑x : ℝ≥0∞).toReal - (↑b : ℝ≥0∞).toReal ≤ ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toReal
⊢ a.toReal - (↑b : ℝ≥0∞).toReal ≤ (a - (↑b : ℝ≥0∞)).toReal

Tactic:
induction a
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b : ℝ≥0
⊢ ENNReal.toReal ∞ - (↑b : ℝ≥0∞).toReal ≤ (∞ - (↑b : ℝ≥0∞)).toReal

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b x : ℝ≥0
coe : (↑x : ℝ) - (↑b : ℝ) ≤ max ((↑x : ℝ) - (↑b : ℝ)) 0
⊢ (↑x : ℝ≥0∞).toReal - (↑b : ℝ≥0∞).toReal ≤ ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toReal

Tactic:
simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]

Premises used: ENNReal.coe_toReal, Real.coe_toNNReal', NNReal.sub_def, ENNReal.coe_sub
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b x : ℝ≥0
⊢ (↑x : ℝ) - (↑b : ℝ) ≤ max ((↑x : ℝ) - (↑b : ℝ)) 0

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b x : ℝ≥0
⊢ (↑x : ℝ) - (↑b : ℝ) ≤ max ((↑x : ℝ) - (↑b : ℝ)) 0

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hb : b ≠ ∞
lift : ∀ (b : ℝ≥0), (a - (↑b : ℝ≥0∞)).toNNReal = a.toNNReal - (↑b : ℝ≥0∞).toNNReal
⊢ (a - b).toNNReal = a.toNNReal - b.toNNReal

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
b : ℝ≥0
top : (∞ - (↑b : ℝ≥0∞)).toNNReal = ENNReal.toNNReal ∞ - (↑b : ℝ≥0∞).toNNReal
coe : ∀ (x : ℝ≥0), ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toNNReal = (↑x : ℝ≥0∞).toNNReal - (↑b : ℝ≥0∞).toNNReal
⊢ (a - (↑b : ℝ≥0∞)).toNNReal = a.toNNReal - (↑b : ℝ≥0∞).toNNReal

Tactic:
induction a
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b : ℝ≥0
⊢ (∞ - (↑b : ℝ≥0∞)).toNNReal = ENNReal.toNNReal ∞ - (↑b : ℝ≥0∞).toNNReal

Tactic:
simp [← coe_sub]

Premises used: ENNReal.coe_sub
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b x : ℝ≥0
⊢ ((↑x : ℝ≥0∞) - (↑b : ℝ≥0∞)).toNNReal = (↑x : ℝ≥0∞).toNNReal - (↑b : ℝ≥0∞).toNNReal

Tactic:
simp [← coe_sub]

Premises used: ENNReal.coe_sub
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0∞
hba : b ≤ a
ha : a ≠ ∞
⊢ (a - b).toReal = a.toReal - b.toReal

Tactic:
simp [ENNReal.toReal, ne_top_of_le_ne_top ha hba, toNNReal_mono ha hba]

Premises used: ENNReal.toNNReal_mono, ENNReal.toReal, ne_top_of_le_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
p q : ℝ
hq : 0 ≤ q
inl : ∀ (h : p ≤ q), ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
inr : ∀ (h : q ≤ p), ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
obtain h | h := le_total p q

Premises used: le_total
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
inl : 0 = ENNReal.ofReal p - ENNReal.ofReal q
inl₁ inl₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]

Premises used: tsub_eq_zero_of_le, ENNReal.ofReal_le_ofReal, ENNReal.ofReal_of_nonpos, sub_nonpos_of_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq, ENNReal.ofReal_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
inr : ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_

Premises used: ENNReal.eq_sub_of_add_eq, ENNReal.ofReal_ne_top
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
inr : ENNReal.ofReal (p - q + q) = ENNReal.ofReal p
inr₁ inr₂ : ENNReal.ofReal p = ENNReal.ofReal p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p

Tactic:
rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]

Premises used: sub_nonneg_of_le, ENNReal.ofReal_add, sub_add_cancel
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
⊢ b ≠ ∞

Tactic:
have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
hb : b ≠ ∞
⊢ a ≠ ∞

Tactic:
ha
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
hb : b ≠ ∞
lift : ∀ (a : ℝ≥0) (h : b ≤ (↑a : ℝ≥0∞)), (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - b) = b - c
⊢ a - c - (a - b) = b - c

Tactic:
lift a to ℝ≥0 using ha
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b c : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
h : b ≤ (↑a : ℝ≥0∞)
⊢ b ≠ ∞

Tactic:
hb
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
b c : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
h : b ≤ (↑a : ℝ≥0∞)
lift : ∀ (b : ℝ≥0) (h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)), (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - c
⊢ (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - b) = b - c

Tactic:
lift b to ℝ≥0 using hb
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
c : ℝ≥0∞
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
top : (↑a : ℝ≥0∞) - ∞ - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - ∞
coe : ∀ (x : ℝ≥0), (↑a : ℝ≥0∞) - (↑x : ℝ≥0∞) - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - (↑x : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) - c - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - c

Tactic:
cases c
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
⊢ (↑a : ℝ≥0∞) - ∞ - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - ∞

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
coe : a - x - (a - b) = b - x
⊢ (↑a : ℝ≥0∞) - (↑x : ℝ≥0∞) - ((↑a : ℝ≥0∞) - (↑b : ℝ≥0∞)) = (↑b : ℝ≥0∞) - (↑x : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
coe : b ≤ a
⊢ a - x - (a - b) = b - x

Tactic:
rw [tsub_tsub_tsub_cancel_left]

Premises used: tsub_tsub_tsub_cancel_left
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
⊢ b ≤ a

Tactic:
mod_cast h

Premises used: cast, ENNReal.coe_le_coe._simp_1
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a b : ℝ≥0
h : (↑b : ℝ≥0∞) ≤ (↑a : ℝ≥0∞)
x : ℝ≥0
⊢ b ≤ a

Tactic:
exact mod_cast h
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
y : ℝ≥0∞
⊢ Ico 0 y = Iio y

Tactic:
Ico_bot

Premises used: Set.Ico_bot
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x ε : ℝ≥0∞
⊢ x ≠ ∞ → ε ≠ 0 → x ∈ Iio (x + ε)

Tactic:
fun xt ε0 => lt_add_right xt ε0

Premises used: Set.Mem, ENNReal.lt_add_right, setOf, Set.Iio
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x ε₁ ε₂ : ℝ≥0∞
⊢ x ≠ ∞ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Ioo (x - ε₁) (x + ε₂)

Tactic:
fun xt x0 ε0 ε0' => ⟨ENNReal.sub_lt_self xt x0 ε0, lt_add_right xt ε0'⟩

Premises used: Set.Mem, ENNReal.lt_add_right, setOf, ENNReal.sub_lt_self, And.intro, Set.Ioo
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x : ℝ≥0
⊢ ofNNReal '' Iic x = Iic (↑x : ℝ≥0∞)

Tactic:
WithTop.image_coe_Iic

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Iic, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x : ℝ≥0
⊢ ofNNReal '' Ici x = Ico (↑x : ℝ≥0∞) ∞

Tactic:
WithTop.image_coe_Ici

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Ici, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x : ℝ≥0
⊢ ofNNReal '' Iio x = Iio (↑x : ℝ≥0∞)

Tactic:
WithTop.image_coe_Iio

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Iio, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x : ℝ≥0
⊢ ofNNReal '' Ioi x = Ioo (↑x : ℝ≥0∞) ∞

Tactic:
WithTop.image_coe_Ioi

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Ioi, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' Icc x y = Icc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
WithTop.image_coe_Icc

Premises used: ENNReal.ofNNReal, ENNReal, WithTop.image_coe_Icc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' Ico x y = Ico (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
WithTop.image_coe_Ico

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Ico, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' Ioc x y = Ioc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
WithTop.image_coe_Ioc

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Ioc, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' Ioo x y = Ioo (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
WithTop.image_coe_Ioo

Premises used: ENNReal.ofNNReal, WithTop.image_coe_Ioo, ENNReal
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' uIcc x y = uIcc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
simp [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' uIoc x y = uIoc (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
simp [uIoc]

Premises used: Set.uIoc
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
x y : ℝ≥0
⊢ ofNNReal '' uIoo x y = uIoo (↑x : ℝ≥0∞) (↑y : ℝ≥0∞)

Tactic:
simp [uIoo]

Premises used: Set.uIoo
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
inl : IsEmpty ι → (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
inr : Nonempty ι → (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : IsEmpty ι
inl : ENNReal.toNNReal ∞ = ⨅ (i : ι), (f i).toNNReal
inl₁ : Eq (α := ℝ≥0) 0 (⨅ (i : ι), (f i).toNNReal)
inl₂ inl₃ : Eq (α := ℝ≥0) 0 0
⊢ (iInf f).toNNReal = ⨅ (i : ι), (f i).toNNReal

Tactic:
rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]

Premises used: ENNReal.toNNReal_top, iInf_of_empty, NNReal.iInf_empty
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h : Nonempty ι
⊢ ∀ (i : ι), f i ≠ ∞

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

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
h : Nonempty ι
f : (i : ι) → ℝ≥0
inr inr₁ : ENNReal.toNNReal (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨅ (i : ι), (↑(f i) : ℝ≥0∞).toNNReal
inr₂ : (↑(iInf f) : ℝ≥0∞).toNNReal = ⨅ (i : ι), (↑(f i) : ℝ≥0∞).toNNReal
⊢ ENNReal.toNNReal (⨅ (i : ι), (↑(f i) : ℝ≥0∞)) = ⨅ (i : ι), ENNReal.toNNReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) i)

Tactic:
simp_rw [← coe_iInf, toNNReal_coe]

Premises used: ENNReal.toNNReal_coe, ENNReal.coe_iInf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
⊢ ∀ (i : { x : ℝ≥0∞ // x ∈ s }), (↑i : ℝ≥0∞) ≠ ∞

Tactic:
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
s : Set ℝ≥0∞
hs : ∀ r ∈ s, r ≠ ∞
hf : ∀ (i : { x : ℝ≥0∞ // x ∈ s }), (↑i : ℝ≥0∞) ≠ ∞
⊢ (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)

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

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

Tactic:
simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]

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

Tactic:
simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]

Premises used: Set.image_image, ENNReal.toReal, ENNReal.toNNReal_sInf, NNReal.coe_sInf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
inl : ∀ (i : ι) (hi : f i ≤ 0), ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
inr : ∀ (h : ¬∃ (i : ι), f i ≤ 0), ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

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

Premises used: Exists, em, LE.le, OfNat.ofNat
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
x : ℝ≥0∞
h : ⊥ < x
⊢ ENNReal.ofReal (f i) < x

Tactic:
simpa [ofReal_of_nonpos hi]

Premises used: ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
inl : ENNReal.ofReal (⨅ (i : ι), f i) = ⊥
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

Tactic:
rw [iInf_eq_bot.2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]

Premises used: Iff.mpr, Exists.intro, iInf_eq_bot
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⊥

Tactic:
simp [Real.iInf_nonpos' ⟨i, hi⟩]

Premises used: Real.iInf_nonpos', Exists.intro
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ¬∃ (i : ι), f i ≤ 0
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
replace h i : 0 ≤ f i := le_of_not_ge fun hi ↦ h ⟨i, hi⟩
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

Tactic:
eq_of_forall_le_iff fun a ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
inr : ∀ (a : ℝ≥0∞), a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
⊢ ENNReal.ofReal (⨅ (i : ι), f i) = ⨅ (i : ι), ENNReal.ofReal (f i)

Tactic:
refine eq_of_forall_le_iff fun a ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
inr : ∞ ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ LE.le (α := ℝ≥0∞) ∞ (⨅ (i : ι), ENNReal.ofReal (f i))
inr₁ : ∀ (ha : a ≠ ∞), a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (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 : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ∞ ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ LE.le (α := ℝ≥0∞) ∞ (⨅ (i : ι), ENNReal.ofReal (f i))

Tactic:
simp
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Membership.mem (γ := Set ℝ) (lowerBounds (range fun (i : ι) ↦ f i)) 0

Tactic:
simpa [mem_lowerBounds]

Premises used: mem_lowerBounds
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
inr : (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)
inr₁ : LE.le (α := ℝ) 0 (⨅ (i : ι), f i)
⊢ a ≤ ENNReal.ofReal (⨅ (i : ι), f i) ↔ a ≤ ⨅ (i : ι), ENNReal.ofReal (f i)

Tactic:
rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]

Premises used: le_iInf_iff, ENNReal.le_ofReal_iff_toReal_le, Exists.intro, OfNat.ofNat, le_ciInf_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

Tactic:
forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm

Premises used: ENNReal.le_ofReal_iff_toReal_le, forall_congr', Iff.symm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

Tactic:
exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm

Premises used: ENNReal.le_ofReal_iff_toReal_le, forall_congr', Iff.symm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ LE.le (α := ℝ) 0 (⨅ (i : ι), f i)

Tactic:
Real.iInf_nonneg h

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

Tactic:
exact Real.iInf_nonneg h

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

Tactic:
le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) <| le_rfl)
    (tsub_le_iff_right.1 <| le_iInf fun _ => tsub_le_iff_right.2 <| iInf_le _ _)

Premises used: Iff.mpr, le_rfl, add_le_add, le_iInf, tsub_le_iff_right, le_antisymm, HAdd.hAdd, Iff.mp, iInf_le
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
refine : ∀ (c : ℝ≥0∞), a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c
⊢ a - ⨅ (i : ι), f i = ⨆ (i : ι), a - f i

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
rw : a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c
⊢ a - ⨅ (i : ι), f i ≤ c ↔ ⨆ (i : ι), a - f i ≤ c

Tactic:
rw [tsub_le_iff_right, add_comm, iInf_add]

Premises used: ENNReal.iInf_add, tsub_le_iff_right, add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a c : ℝ≥0∞
⊢ a ≤ ⨅ (i : ι), f i + c ↔ ⨆ (i : ι), a - f i ≤ c

Tactic:
simp [tsub_le_iff_right, add_comm]

Premises used: tsub_le_iff_right, add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
a : ℝ≥0∞
s : Set ℝ≥0∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
simp [sInf_eq_iInf, iInf_add]

Premises used: ENNReal.iInf_add, sInf_eq_iInf
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
rw : Eq (α := ℝ≥0∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)
⊢ a + iInf f = ⨅ (b : ι), a + f b

Tactic:
rw [add_comm, iInf_add]

Premises used: ENNReal.iInf_add, add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), f i + a) (⨅ (b : ι), a + f b)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.ENNReal.Operations
Goal:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ (k : ι), f k + g k ≤ f i + g j
simp_rw : Eq (α := ℝ≥0∞) (⨅ (a : ι), ⨅ (a' : ι), f a + g a') (⨅ (i : ι), f i + iInf g)
⊢ ⨅ (a : ι), ⨅ (a' : ι), f a + g 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:
ι : 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
h₁ : f _k ≤ f i
h₂ : g _k ≤ g j
⊢ f _k + g _k ≤ f i + g j

Tactic:
gcongr