awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : x ≤ y
⊢ 0 = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal

Tactic:
(tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm

Premises used: Iff.mpr, EReal.coe_le_coe_iff, EReal.toENNReal_le_toENNReal, tsub_eq_zero_of_le, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : x ≤ y
⊢ 0 = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal

Tactic:
exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm

Premises used: Iff.mpr, EReal.coe_le_coe_iff, EReal.toENNReal_le_toENNReal, tsub_eq_zero_of_le, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : ¬x ≤ y
neg : ENNReal.ofReal x - ENNReal.ofReal y = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal

Tactic:
rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe,
      ofReal_sub x (EReal.coe_nonneg.mp hy)]

Premises used: EReal.toENNReal_of_ne_top, ne_of_beq_false, EReal.coe_sub, Ne.symm, EReal.coe_nonneg, EReal.toReal_coe, Iff.mp, ENNReal.ofReal_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : ¬x ≤ y
⊢ ENNReal.ofReal x - ENNReal.ofReal y = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
b : ℝ
bot : ⊥ + (↑b : EReal) - (↑b : EReal) = ⊥
coe : ∀ (a : ℝ), (↑a : EReal) + (↑b : EReal) - (↑b : EReal) = (↑a : EReal)
top : ⊤ + (↑b : EReal) - (↑b : EReal) = ⊤
⊢ a + (↑b : EReal) - (↑b : EReal) = a

Tactic:
cases a
-- Module: Mathlib.Data.EReal.Operations
Goal:
b : ℝ
⊢ ⊥ + (↑b : EReal) - (↑b : EReal) = ⊥

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
coe : a + b - b = a
⊢ (↑a : EReal) + (↑b : EReal) - (↑b : EReal) = (↑a : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b : ℝ
⊢ ⊤ + (↑b : EReal) - (↑b : EReal) = ⊤

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
⊢ a + b - b = a

Tactic:
_root_.add_sub_cancel_right _ _

Premises used: add_sub_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
⊢ a + b - b = a

Tactic:
exact _root_.add_sub_cancel_right _ _

Premises used: add_sub_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
b : ℝ
rw : a + (↑b : EReal) - (↑b : EReal) = a
rw₁ rw₂ : a = a
⊢ (↑b : EReal) + a - (↑b : EReal) = a

Tactic:
rw [add_comm, EReal.add_sub_cancel_right]

Premises used: add_comm, EReal.add_sub_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
b : ℝ
rw : (↑b : EReal) + (a - (↑b : EReal)) = a
rw₁ : (↑b : EReal) + a - (↑b : EReal) = a
rw₂ rw₃ : a = a
⊢ a - (↑b : EReal) + (↑b : EReal) = a

Tactic:
rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]

Premises used: add_sub_assoc, EReal.add_sub_cancel_left, add_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
b : ℝ
bot : (↑b : EReal) - (⊥ + (↑b : EReal)) = -⊥
coe : ∀ (a : ℝ), (↑b : EReal) - ((↑a : EReal) + (↑b : EReal)) = -(↑a : EReal)
top : (↑b : EReal) - (⊤ + (↑b : EReal)) = -⊤
⊢ (↑b : EReal) - (a + (↑b : EReal)) = -a

Tactic:
cases a
-- Module: Mathlib.Data.EReal.Operations
Goal:
b : ℝ
⊢ (↑b : EReal) - (⊥ + (↑b : EReal)) = -⊥

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
coe : b - (a + b) = -a
⊢ (↑b : EReal) - ((↑a : EReal) + (↑b : EReal)) = -(↑a : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b : ℝ
⊢ (↑b : EReal) - (⊤ + (↑b : EReal)) = -⊤

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
⊢ b - (a + b) = -a

Tactic:
_root_.sub_add_cancel_right _ _

Premises used: sub_add_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
b a : ℝ
⊢ b - (a + b) = -a

Tactic:
exact _root_.sub_add_cancel_right _ _

Premises used: sub_add_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
b : ℝ
rw : (↑b : EReal) - (a + (↑b : EReal)) = -a
rw₁ rw₂ : -a = -a
⊢ (↑b : EReal) - ((↑b : EReal) + a) = -a

Tactic:
rw [add_comm, sub_add_cancel_right]

Premises used: add_comm, EReal.sub_add_cancel_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊥ ⊥ ∨ c ≠ ⊥
ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤
⊢ ¬c = ⊥

Tactic:
simp only [ne_eq, not_true_eq_false, false_or] at hb

Premises used: not_true_eq_false, false_or, ne_eq
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤
hb : ¬c = ⊥
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c

Tactic:
simp only [sub_bot hb, le_top, add_bot, bot_le]

Premises used: EReal.add_bot, EReal.sub_bot, le_top, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
b : ℝ
hb : (↑b : EReal) ≠ ⊥ ∨ c ≠ ⊥
ht : (↑b : EReal) ≠ ⊤ ∨ c ≠ ⊤
coe : a + (↑b : EReal) ≤ c - (↑b : EReal) + (↑b : EReal) ↔ a + (↑b : EReal) ≤ c
coe₁ coe₂ : a + (↑b : EReal) ≤ c ↔ a + (↑b : EReal) ≤ c
⊢ a ≤ c - (↑b : EReal) ↔ a + (↑b : EReal) ≤ c

Tactic:
rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]

Premises used: EReal.addLECancellable_coe, EReal.sub_add_cancel, AddLECancellable.add_le_add_iff_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : Ne (α := EReal) ⊤ ⊤ ∨ c ≠ ⊤
top : ∀ (ht : ¬c = ⊤), a = ⊥ ↔ a + ⊤ ≤ c
⊢ a ≤ c - ⊤ ↔ a + ⊤ ≤ c

Tactic:
simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢

Premises used: le_bot_iff, EReal.sub_top, not_true_eq_false, false_or, ne_eq
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
⊢ a = ⊥ ↔ a + ⊤ ≤ c

Tactic:
⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩

Premises used: EReal.bot_add, Eq.rec, Iff.intro, Top.top, Eq.symm, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
top : ∀ (h : a + ⊤ ≤ c), a = ⊥
⊢ a = ⊥ ↔ a + ⊤ ≤ c

Tactic:
refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
top : ∀ (ha : ¬a = ⊥), False
⊢ a = ⊥

Tactic:
by_contra ha
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
ha : ¬a = ⊥
⊢ False

Tactic:
(h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Premises used: Iff.mpr, Ne.lt_top, EReal.add_top_iff_ne_bot, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Data.EReal.Operations
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
ha : ¬a = ⊥
⊢ False

Tactic:
exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Premises used: Iff.mpr, Ne.lt_top, EReal.add_top_iff_ne_bot, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
bot : ∀ (hb : Ne (α := EReal) ⊥ ⊥ ∨ c ≠ ⊥) (ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤), a ≤ c - ⊥ ↔ a + ⊥ ≤ c
coe :
  ∀ (b : ℝ) (hb : (↑b : EReal) ≠ ⊥ ∨ c ≠ ⊥) (ht : (↑b : EReal) ≠ ⊤ ∨ c ≠ ⊤), a ≤ c - (↑b : EReal) ↔ a + (↑b : EReal) ≤ c
top : ∀ (hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥) (ht : Ne (α := EReal) ⊤ ⊤ ∨ c ≠ ⊤), a ≤ c - ⊤ ↔ a + ⊤ ≤ c
⊢ a ≤ c - b ↔ a + b ≤ c

Tactic:
induction b with
  | bot =>
    simp only [ne_eq, not_true_eq_false, false_or] at hb
    simp only [sub_bot hb, le_top, add_bot, bot_le]
  | coe b =>
    rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
  | top =>
    simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
    refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
    by_contra ha
    exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

Premises used: le_bot_iff, EReal.sub_top, EReal.add_bot, not_true_eq_false, EReal.sub_add_cancel, false_or, ne_eq, le_top, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
this : a + -b ≤ c ↔ a ≤ c - -b
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
simpa [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
suffices : a + -b ≤ c ↔ a ≤ c - -b
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b

Tactic:
(le_sub_iff_add_le ?_ ?_).symm

Premises used: EReal.le_sub_iff_add_le, Iff.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
refine_1 : -b ≠ ⊥ ∨ c ≠ ⊥
refine_2 : -b ≠ ⊤ ∨ c ≠ ⊤
⊢ a + -b ≤ c ↔ a ≤ c - -b

Tactic:
refine (le_sub_iff_add_le ?_ ?_).symm

Premises used: EReal.le_sub_iff_add_le, Iff.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊥ ∨ c ≠ ⊥

Tactic:
simpa
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊤ ∨ c ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ c < a - b ↔ c + b < a

Tactic:
lt_iff_lt_of_le_iff_le (sub_le_iff_le_add h₁ h₂)

Premises used: EReal.sub_le_iff_le_add, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a ≤ b + ⊥
⊢ a = ⊥

Tactic:
rw [add_bot, le_bot_iff] at h

Premises used: le_bot_iff, EReal.add_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b

Tactic:
simp only [h, bot_sub, bot_le]

Premises used: EReal.bot_sub, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
c : ℝ
h : a ≤ b + (↑c : EReal)
⊢ a - (↑c : EReal) ≤ b

Tactic:
(sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h

Premises used: Iff.mpr, EReal.coe_ne_bot, EReal.coe_ne_top, Or.inl, EReal.sub_le_iff_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
c : ℝ
h : a ≤ b + (↑c : EReal)
⊢ a - (↑c : EReal) ≤ b

Tactic:
exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h

Premises used: Iff.mpr, EReal.coe_ne_bot, EReal.coe_ne_top, Or.inl, EReal.sub_le_iff_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a ≤ b + ⊤
⊢ a - ⊤ ≤ b

Tactic:
simp only [sub_top, bot_le]

Premises used: EReal.sub_top, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a ≤ b + c
bot : ∀ (h : a ≤ b + ⊥), a - ⊥ ≤ b
coe : ∀ (c : ℝ) (h : a ≤ b + (↑c : EReal)), a - (↑c : EReal) ≤ b
top : ∀ (h : a ≤ b + ⊤), a - ⊤ ≤ b
⊢ a - c ≤ b

Tactic:
induction c with
  | bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
  | coe c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
  | top => simp only [sub_top, bot_le]

Premises used: le_bot_iff, EReal.sub_top, EReal.add_bot, EReal.bot_sub, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a ≤ b + c
⊢ a - b ≤ c

Tactic:
sub_le_of_le_add (add_comm b c ▸ h)

Premises used: Eq.rec, add_comm, EReal.sub_le_of_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a ≤ b - c
rw : a + - -c ≤ b
⊢ a + c ≤ b

Tactic:
rw [← neg_neg c]

Premises used: neg_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a ≤ b - c
⊢ a + - -c ≤ b

Tactic:
sub_le_of_le_add h

Premises used: WithBot.map₂, EReal.sub_le_of_le_add, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a ≤ b - c
⊢ a + - -c ≤ b

Tactic:
exact sub_le_of_le_add h

Premises used: EReal.sub_le_of_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊥
h₂ : b ≠ ⊤ ∨ c ≠ ⊤
⊢ c - b < a ↔ c < a + b

Tactic:
lt_iff_lt_of_le_iff_le (le_sub_iff_add_le h₁ h₂)

Premises used: lt_iff_lt_of_le_iff_le, EReal.le_sub_iff_add_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a < b - c
contrapose! : ∀ (h : b ≤ a + c), b - c ≤ a
⊢ a + c < b

Tactic:
contrapose! h
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : b ≤ a + c
⊢ b - c ≤ a

Tactic:
sub_le_of_le_add h

Premises used: EReal.sub_le_of_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : b ≤ a + c
⊢ b - c ≤ a

Tactic:
exact sub_le_of_le_add h

Premises used: EReal.sub_le_of_le_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : a < b + c
rwa : a < b + - -c
rwa₁ rwa₂ rwa₃ rwa₄ : a < b + c
⊢ a < b - -c

Tactic:
rwa [sub_eq_add_neg, neg_neg]

Premises used: sub_eq_add_neg, neg_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h rwa rwa₁ rwa₂ rwa₃ : a < b + c
⊢ a < c + b

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ (∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)) ↔ y ≤ x

Tactic:
⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩

Premises used: WithBot.le_of_forall_lt_iff_le, LT.lt.le, Iff.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
refine :
  ∀ (h : ∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)) (z : WithTop ℝ),
    x < (↑z : WithBot (WithTop ℝ)) → y ≤ (↑z : WithBot (WithTop ℝ))
⊢ (∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : ∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)
rw :
  (x < (↑⊤ : WithBot (WithTop ℝ)) → y ≤ (↑⊤ : WithBot (WithTop ℝ))) ∧
    ∀ (x_1 : ℝ), x < (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) → y ≤ (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ))
⊢ ∀ (z : WithTop ℝ), x < (↑z : WithBot (WithTop ℝ)) → y ≤ (↑z : WithBot (WithTop ℝ))

Tactic:
rw [WithTop.forall]

Premises used: WithTop.forall
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : ∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)
⊢ (x < (↑⊤ : WithBot (WithTop ℝ)) → y ≤ (↑⊤ : WithBot (WithTop ℝ))) ∧
    ∀ (x_1 : ℝ), x < (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) → y ≤ (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ))

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ (∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x) ↔ y ≤ x

Tactic:
⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩

Premises used: WithBot.ge_of_forall_gt_iff_ge, LT.lt.le, Iff.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
refine :
  ∀ (h : ∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x) (z : WithTop ℝ),
    (↑z : WithBot (WithTop ℝ)) < y → (↑z : WithBot (WithTop ℝ)) ≤ x
⊢ (∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : ∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x
rw :
  ((↑⊤ : WithBot (WithTop ℝ)) < y → (↑⊤ : WithBot (WithTop ℝ)) ≤ x) ∧
    ∀ (x_1 : ℝ), (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) < y → (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) ≤ x
⊢ ∀ (z : WithTop ℝ), (↑z : WithBot (WithTop ℝ)) < y → (↑z : WithBot (WithTop ℝ)) ≤ x

Tactic:
rw [WithTop.forall]

Premises used: WithTop.forall
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : ∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x
⊢ ((↑⊤ : WithBot (WithTop ℝ)) < y → (↑⊤ : WithBot (WithTop ℝ)) ≤ x) ∧
    ∀ (x_1 : ℝ), (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) < y → (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) ≤ x

Tactic:
aesop
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < a + b
obtain : ∀ (a' : EReal) (hc' : c - b < a') (ha' : a' < a), ∃ a' < a, c < a' + b
⊢ ∃ a' < a, c < a' + b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)

Premises used: exists_between, EReal.sub_lt_of_lt_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' + b

Tactic:
⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩

Premises used: LT.lt.ne_top, EReal.sub_lt_iff, And.intro, Exists.intro, Iff.mp, Or.inl, Or.inr
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
refine : b ≠ ⊥
⊢ ∃ a' < a, c < a' + b

Tactic:
refine ⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
contrapose! : ∀ (hc : b = ⊥), a + b ≤ c
⊢ b ≠ ⊥

Tactic:
contrapose! hc
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c a' : EReal
hc' : c - b < a'
ha' : a' < a
hc : b = ⊥
⊢ a + b ≤ c

Tactic:
hc ▸ (add_bot a).symm ▸ bot_le

Premises used: EReal.add_bot, Eq.rec, Eq.symm, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c a' : EReal
hc' : c - b < a'
ha' : a' < a
hc : b = ⊥
⊢ a + b ≤ c

Tactic:
exact hc ▸ (add_bot a).symm ▸ bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < a + b
simp_rw : ∀ (hc : c < b + a), ∃ b' < b, c < b' + a
⊢ ∃ b' < b, c < a + b'

Tactic:
simp_rw [add_comm a] at hc ⊢

Premises used: add_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a

Tactic:
exists_lt_add_left hc

Premises used: _private.0.EReal.exists_lt_add_left
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a

Tactic:
exact exists_lt_add_left hc

Premises used: _private.0.EReal.exists_lt_add_left
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
⊢ a + b ≤ c

Tactic:
le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
refine : ∀ (d : EReal) (hd : d < a + b), d ≤ c
⊢ a + b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_

Premises used: le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd : d < a + b
obtain : ∀ (a' : EReal) (ha' : a' < a) (hd : d < a' + b), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd

Premises used: _private.0.EReal.exists_lt_add_left
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd_1 : d < a + b
a' : EReal
ha' : a' < a
hd : d < a' + b
obtain : ∀ (b' : EReal) (hb' : b' < b) (hd : d < a' + b'), d ≤ c
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd

Premises used: _private.0.EReal.exists_lt_add_right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd_1 : d < a + b
a' : EReal
ha' : a' < a
hd_2 : d < a' + b
b' : EReal
hb' : b' < b
hd : d < a' + b'
⊢ d ≤ c

Tactic:
hd.le.trans (h _ ha' _ hb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd_1 : d < a + b
a' : EReal
ha' : a' < a
hd_2 : d < a' + b
b' : EReal
hb' : b' < b
hd : d < a' + b'
⊢ d ≤ c

Tactic:
exact hd.le.trans (h _ ha' _ hb')

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
rw : -a - b ≤ -c
⊢ c ≤ a + b

Tactic:
rw [← neg_le_neg_iff, neg_add h₁ h₂]

Premises used: EReal.neg_le_neg_iff, EReal.neg_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c

Tactic:
add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_

Premises used: SubNegMonoid.sub', EReal.le_neg_of_le_neg, EReal.add_le_of_forall_lt, WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
refine : ∀ (a' : EReal) (ha' : a' < -a) (b' : EReal) (hb' : b' < -b), c ≤ -(a' + b')
⊢ -a - b ≤ -c

Tactic:
refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_

Premises used: EReal.le_neg_of_le_neg, EReal.add_le_of_forall_lt
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
rw : c ≤ -a' - b'
⊢ c ≤ -(a' + b')

Tactic:
rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]

Premises used: LT.lt.ne_top, EReal.neg_add, Or.inl, Or.inr
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'

Tactic:
h _ (EReal.lt_neg_of_lt_neg ha') _ (EReal.lt_neg_of_lt_neg hb')

Premises used: EReal.lt_neg_of_lt_neg, SubNegMonoid.sub', WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'

Tactic:
exact h _ (EReal.lt_neg_of_lt_neg ha') _ (EReal.lt_neg_of_lt_neg hb')

Premises used: EReal.lt_neg_of_lt_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ≥0∞
hy_top : y ≠ ∞
h_le : y ≤ x
⊢ y ≠ ∞

Tactic:
hy_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ≥0∞
hy_top : y ≠ ∞
h_le : y ≤ x
lift : ∀ (y : ℝ≥0) (h_le : (↑y : ℝ≥0∞) ≤ x), (↑(x - (↑y : ℝ≥0∞)) : EReal) = (↑x : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
⊢ (↑(x - y) : EReal) = (↑x : EReal) - (↑y : EReal)

Tactic:
lift y to ℝ≥0 using hy_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : ℝ≥0
h_le : (↑y : ℝ≥0∞) ≤ ∞
⊢ (↑(∞ - (↑y : ℝ≥0∞)) : EReal) = (↑∞ : EReal) - (↑(↑y : ℝ≥0∞) : EReal)

Tactic:
simp [coe_nnreal_eq_coe_real]

Premises used: EReal.coe_nnreal_eq_coe_real
-- Module: Mathlib.Data.EReal.Operations
Goal:
y x : ℝ≥0
h_le : (↑y : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
⊢ (↑((↑x : ℝ≥0∞) - (↑y : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) - (↑(↑y : ℝ≥0∞) : EReal)

Tactic:
simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

Premises used: EReal.coe_sub, ENNReal.coe_sub, EReal.coe_nnreal_eq_coe_real, NNReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ≥0∞
y : ℝ≥0
h_le : (↑y : ℝ≥0∞) ≤ x
top : ∀ (h_le : (↑y : ℝ≥0∞) ≤ ∞), (↑(∞ - (↑y : ℝ≥0∞)) : EReal) = (↑∞ : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
coe :
  ∀ (x : ℝ≥0) (h_le : (↑y : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)),
    (↑((↑x : ℝ≥0∞) - (↑y : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
⊢ (↑(x - (↑y : ℝ≥0∞)) : EReal) = (↑x : EReal) - (↑(↑y : ℝ≥0∞) : EReal)

Tactic:
cases x with
  | top => simp [coe_nnreal_eq_coe_real]
  | coe x =>
    simp only [coe_nnreal_eq_coe_real, ← ENNReal.coe_sub, NNReal.coe_sub (mod_cast h_le), coe_sub]

Premises used: EReal.coe_sub, ENNReal.coe_sub, EReal.coe_nnreal_eq_coe_real, NNReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊤ = ⊤

Tactic:
rfl

Premises used: WithBot.some, EReal.mul, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) ⊤ ⊥ = ⊥

Tactic:
rfl

Premises used: EReal.mul, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊤ = ⊥

Tactic:
rfl

Premises used: EReal.mul, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) ⊥ ⊥ = ⊤

Tactic:
rfl

Premises used: WithBot.some, EReal.mul, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ (↑x : EReal) * ⊤ = ⊤

Tactic:
if_pos h

Premises used: if_pos, EReal.mul, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ (↑x : EReal) * ⊤ = ⊥

Tactic:
(if_neg h.not_gt).trans (if_neg h.ne)

Premises used: EReal.mul, LT.lt.not_gt, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ ⊤ * (↑x : EReal) = ⊤

Tactic:
if_pos h

Premises used: if_pos, EReal.mul, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ ⊤ * (↑x : EReal) = ⊥

Tactic:
(if_neg h.not_gt).trans (if_neg h.ne)

Premises used: EReal.mul, LT.lt.not_gt, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
rw : x * ⊤ = ⊤
⊢ ⊤ * x = ⊤

Tactic:
rw [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤

Tactic:
mul_top_of_pos h

Premises used: EReal.mul_top_of_pos