awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
bot : (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal
have coe : ∀ (a : ℝ), ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
bot : (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
coe : ∀ (a : ℝ), ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal
have top : (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
⊢ (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
have bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥
⊢ (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
have bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊥ - (↑a : EReal)).toENNReal = toENNReal ⊥ - (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
bot : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥
bot₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊥ - (↑a : EReal)).toENNReal = toENNReal ⊥ - (↑a : EReal).toENNReal
⊢ (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
have bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HSub.hSub (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ - toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
⊢ ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
have coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥
⊢ ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
have coe₁ : ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
  ((↑a : EReal) - (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal - (↑a_1 : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
a : ℝ
coe : ∀ (hy : LE.le (α := EReal) 0 ⊥), ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥
coe₁ :
  ∀ (a_1 : ℝ) (hy : 0 ≤ (↑a_1 : EReal)),
    ((↑a : EReal) - (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal - (↑a_1 : EReal).toENNReal
⊢ ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
have coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), ((↑a : EReal) - ⊤).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
⊢ (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal
have top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥
⊢ (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal
have top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊤ - (↑a : EReal)).toENNReal = toENNReal ⊤ - (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : 0 ≤ y
top : ∀ (hy : LE.le (α := EReal) 0 ⊥), (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥
top₁ : ∀ (a : ℝ) (hy : 0 ≤ (↑a : EReal)), (⊤ - (↑a : EReal)).toENNReal = toENNReal ⊤ - (↑a : EReal).toENNReal
⊢ (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal
have top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HSub.hSub (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ - toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
have pos : ∀ (hxy : x ≤ y), ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
Tactic: by_cases hxy : x ≤ y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
pos : ∀ (hxy : x ≤ y), ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
have neg : ∀ (hxy : ¬x ≤ y), ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
Tactic: by_cases hxy : x ≤ y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : x ≤ y
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
have pos : 0 = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
Tactic: rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : ¬x ≤ y
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
have neg : ENNReal.ofReal x - ENNReal.ofReal y = (↑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)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
⊢ a + (↑b : EReal) - (↑b : EReal) = a
have bot : ⊥ + (↑b : EReal) - (↑b : EReal) = ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
bot : ⊥ + (↑b : EReal) - (↑b : EReal) = ⊥
⊢ a + (↑b : EReal) - (↑b : EReal) = a
have coe : ∀ (a : ℝ), (↑a : EReal) + (↑b : EReal) - (↑b : EReal) = (↑a : EReal)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
bot : ⊥ + (↑b : EReal) - (↑b : EReal) = ⊥
coe : ∀ (a : ℝ), (↑a : EReal) + (↑b : EReal) - (↑b : EReal) = (↑a : EReal)
⊢ a + (↑b : EReal) - (↑b : EReal) = a
have top : ⊤ + (↑b : EReal) - (↑b : EReal) = ⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b a : ℝ
⊢ (↑a : EReal) + (↑b : EReal) - (↑b : EReal) = (↑a : EReal)
have coe : a + b - b = a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
⊢ (↑b : EReal) + a - (↑b : EReal) = a
have rw : a + (↑b : EReal) - (↑b : EReal) = a
Tactic: rw [add_comm, EReal.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
rw : a + (↑b : EReal) - (↑b : EReal) = a
⊢ (↑b : EReal) + a - (↑b : EReal) = a
have rw₁ : a = a
Tactic: rw [add_comm, EReal.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
⊢ a - (↑b : EReal) + (↑b : EReal) = a
have rw : (↑b : EReal) + (a - (↑b : EReal)) = a
Tactic: rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
rw : (↑b : EReal) + (a - (↑b : EReal)) = a
⊢ a - (↑b : EReal) + (↑b : EReal) = a
have rw₁ : (↑b : EReal) + a - (↑b : EReal) = a
Tactic: rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
rw : (↑b : EReal) + (a - (↑b : EReal)) = a
rw₁ : (↑b : EReal) + a - (↑b : EReal) = a
⊢ a - (↑b : EReal) + (↑b : EReal) = a
have rw₂ : a = a
Tactic: rw [add_comm, ← add_sub_assoc, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
⊢ (↑b : EReal) - (a + (↑b : EReal)) = -a
have bot : (↑b : EReal) - (⊥ + (↑b : EReal)) = -⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
bot : (↑b : EReal) - (⊥ + (↑b : EReal)) = -⊥
⊢ (↑b : EReal) - (a + (↑b : EReal)) = -a
have coe : ∀ (a : ℝ), (↑b : EReal) - ((↑a : EReal) + (↑b : EReal)) = -(↑a : EReal)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
bot : (↑b : EReal) - (⊥ + (↑b : EReal)) = -⊥
coe : ∀ (a : ℝ), (↑b : EReal) - ((↑a : EReal) + (↑b : EReal)) = -(↑a : EReal)
⊢ (↑b : EReal) - (a + (↑b : EReal)) = -a
have top : (↑b : EReal) - (⊤ + (↑b : EReal)) = -⊤
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b a : ℝ
⊢ (↑b : EReal) - ((↑a : EReal) + (↑b : EReal)) = -(↑a : EReal)
have coe : b - (a + b) = -a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
⊢ (↑b : EReal) - ((↑b : EReal) + a) = -a
have rw : (↑b : EReal) - (a + (↑b : EReal)) = -a
Tactic: rw [add_comm, sub_add_cancel_right]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
b : ℝ
rw : (↑b : EReal) - (a + (↑b : EReal)) = -a
⊢ (↑b : EReal) - ((↑b : EReal) + a) = -a
have rw₁ : -a = -a
Tactic: rw [add_comm, sub_add_cancel_right]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
a c : EReal
hb : Ne (α := EReal) ⊥ ⊥ ∨ c ≠ ⊥
ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c
have hb₁ : ¬c = ⊥
Tactic: simp only [ne_eq, not_true_eq_false, false_or] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a c : EReal
b : ℝ
hb : (↑b : EReal) ≠ ⊥ ∨ c ≠ ⊥
ht : (↑b : EReal) ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - (↑b : EReal) ↔ a + (↑b : EReal) ≤ c
have coe : a + (↑b : EReal) ≤ c - (↑b : EReal) + (↑b : EReal) ↔ a + (↑b : EReal) ≤ c
Tactic: rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ a ≤ c - (↑b : EReal) ↔ a + (↑b : EReal) ≤ c
have coe₁ : a + (↑b : EReal) ≤ c ↔ a + (↑b : EReal) ≤ c
Tactic: rw [← (addLECancellable_coe b).add_le_add_iff_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : Ne (α := EReal) ⊤ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊤ ↔ a + ⊤ ≤ c
have top : ∀ (ht : ¬c = ⊤), a = ⊥ ↔ a + ⊤ ≤ c
Tactic: simp only [ne_eq, not_true_eq_false, false_or, sub_top, le_bot_iff] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
⊢ a = ⊥ ↔ a + ⊤ ≤ c
have top : ∀ (h : a + ⊤ ≤ c), a = ⊥
Tactic: refine ⟨fun h ↦ h ▸ (bot_add ⊤).symm ▸ bot_le, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a c : EReal
hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
⊢ a = ⊥
have top : ∀ (ha : ¬a = ⊥), False
Tactic: by_contra ha
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - b ↔ a + b ≤ c
have bot : ∀ (hb : Ne (α := EReal) ⊥ ⊥ ∨ c ≠ ⊥) (ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤), a ≤ c - ⊥ ↔ a + ⊥ ≤ 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)
Cleared hypotheses: b, hb, ht
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
bot : ∀ (hb : Ne (α := EReal) ⊥ ⊥ ∨ c ≠ ⊥) (ht : Ne (α := EReal) ⊥ ⊤ ∨ c ≠ ⊤), a ≤ c - ⊥ ↔ a + ⊥ ≤ c
⊢ a ≤ c - b ↔ a + b ≤ c
have coe : ∀ (b : ℝ) (hb : (↑b : EReal) ≠ ⊥ ∨ c ≠ ⊥) (ht : (↑b : EReal) ≠ ⊤ ∨ c ≠ ⊤), a ≤ c - (↑b : EReal) ↔ a + (↑b : EReal) ≤ 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)
Cleared hypotheses: b, hb, ht
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ a ≤ c - b ↔ a + b ≤ c
have top : ∀ (hb : Ne (α := EReal) ⊤ ⊥ ∨ c ≠ ⊥) (ht : Ne (α := EReal) ⊤ ⊤ ∨ c ≠ ⊤), a ≤ c - ⊤ ↔ a + ⊤ ≤ 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)
Cleared hypotheses: b, hb, ht
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a - b ≤ c ↔ a ≤ c + b
have suffices : a + -b ≤ c ↔ a ≤ c - -b
Tactic: suffices a + (-b) ≤ c ↔ a ≤ c - (-b) by simpa [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b
have refine_1 : -b ≠ ⊥ ∨ c ≠ ⊥
Tactic: refine (le_sub_iff_add_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
refine_1 : -b ≠ ⊥ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b
have refine_2 : -b ≠ ⊤ ∨ c ≠ ⊤
Tactic: refine (le_sub_iff_add_le ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
a b : EReal
h : a ≤ b + ⊥
⊢ a - ⊥ ≤ b
have h₁ : a = ⊥
Tactic: rw [add_bot, le_bot_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : a ≤ b + c
⊢ a - c ≤ b
have bot : ∀ (h : a ≤ b + ⊥), a - ⊥ ≤ 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]
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : a ≤ b + c
bot : ∀ (h : a ≤ b + ⊥), a - ⊥ ≤ b
⊢ a - c ≤ b
have coe : ∀ (c : ℝ) (h : a ≤ b + (↑c : EReal)), a - (↑c : EReal) ≤ 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]
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ a - c ≤ b
have top : ∀ (h : a ≤ b + ⊤), a - ⊤ ≤ 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]
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : a ≤ b - c
⊢ a + c ≤ b
have rw : a + - -c ≤ b
Tactic: rw [← neg_neg c]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : a < b - c
⊢ a + c < b
have contrapose! : ∀ (h : b ≤ a + c), b - c ≤ a
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : a < b + c
⊢ a < b - -c
have rwa : a < b + - -c
Tactic: rwa [sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ (∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)) ↔ y ≤ x
have refine : ∀ (h : ∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)) (z : WithTop ℝ),
  x < (↑z : WithBot (WithTop ℝ)) → y ≤ (↑z : WithBot (WithTop ℝ))
Tactic: refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : ∀ (z : ℝ), x < (↑z : EReal) → y ≤ (↑z : EReal)
⊢ ∀ (z : WithTop ℝ), x < (↑z : WithBot (WithTop ℝ)) → y ≤ (↑z : WithBot (WithTop ℝ))
have rw : (x < (↑⊤ : WithBot (WithTop ℝ)) → y ≤ (↑⊤ : WithBot (WithTop ℝ))) ∧
  ∀ (x_1 : ℝ), x < (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) → y ≤ (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ))
Tactic: rw [WithTop.forall]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ (∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x) ↔ y ≤ x
have refine : ∀ (h : ∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x) (z : WithTop ℝ),
  (↑z : WithBot (WithTop ℝ)) < y → (↑z : WithBot (WithTop ℝ)) ≤ x
Tactic: refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : ∀ (z : ℝ), (↑z : EReal) < y → (↑z : EReal) ≤ x
⊢ ∀ (z : WithTop ℝ), (↑z : WithBot (WithTop ℝ)) < y → (↑z : WithBot (WithTop ℝ)) ≤ x
have rw : ((↑⊤ : WithBot (WithTop ℝ)) < y → (↑⊤ : WithBot (WithTop ℝ)) ≤ x) ∧
  ∀ (x_1 : ℝ), (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) < y → (↑(↑x_1 : WithTop ℝ) : WithBot (WithTop ℝ)) ≤ x
Tactic: rw [WithTop.forall]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hc : c < a + b
⊢ ∃ a' < a, c < a' + b
have obtain : ∀ (a' : EReal) (hc' : c - b < a') (ha' : a' < a), ∃ a' < a, c < a' + b
Tactic: obtain ⟨a', hc', ha'⟩ := exists_between (sub_lt_of_lt_add hc)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ ∃ a' < a, c < a' + b
have refine : b ≠ ⊥
Tactic: refine ⟨a', ha', (sub_lt_iff (.inl ?_) (.inr hc.ne_top)).1 hc'⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hc : c < a + b
a' : EReal
hc' : c - b < a'
ha' : a' < a
⊢ b ≠ ⊥
have contrapose! : ∀ (hc : b = ⊥), a + b ≤ c
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
hc : c < a + b
⊢ ∃ b' < b, c < a + b'
have simp_rw : ∀ (hc : c < b + a), ∃ b' < b, c < b' + a
Tactic: simp_rw [add_comm a] at hc ⊢
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
⊢ a + b ≤ c
have refine : ∀ (d : EReal) (hd : d < a + b), d ≤ c
Tactic: refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h : ∀ a' < a, ∀ b' < b, a' + b' ≤ c
d : EReal
hd : d < a + b
⊢ d ≤ c
have obtain : ∀ (a' : EReal) (ha' : a' < a) (hd : d < a' + b), d ≤ c
Tactic: obtain ⟨a', ha', hd⟩ := exists_lt_add_left hd
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ d ≤ c
have obtain : ∀ (b' : EReal) (hb' : b' < b) (hd : d < a' + b'), d ≤ c
Tactic: obtain ⟨b', hb', hd⟩ := exists_lt_add_right hd
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ c ≤ a + b
have rw : -a - b ≤ -c
Tactic: rw [← neg_le_neg_iff, neg_add h₁ h₂]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c
have refine : ∀ (a' : EReal) (ha' : a' < -a) (b' : EReal) (hb' : b' < -b), c ≤ -(a' + b')
Tactic: refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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')
have rw : c ≤ -a' - b'
Tactic: rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ≥0∞
hy_top : y ≠ ∞
h_le : y ≤ x
⊢ (↑(x - y) : EReal) = (↑x : EReal) - (↑y : EReal)
have lift : ∀ (y : ℝ≥0) (h_le : (↑y : ℝ≥0∞) ≤ x), (↑(x - (↑y : ℝ≥0∞)) : EReal) = (↑x : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
Tactic: lift y to ℝ≥0 using hy_top
Cleared hypotheses: y, hy_top, h_le
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ≥0∞
y : ℝ≥0
h_le : (↑y : ℝ≥0∞) ≤ x
⊢ (↑(x - (↑y : ℝ≥0∞)) : EReal) = (↑x : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
have top : ∀ (h_le : (↑y : ℝ≥0∞) ≤ ∞), (↑(∞ - (↑y : ℝ≥0∞)) : EReal) = (↑∞ : 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]
Cleared hypotheses: x, h_le
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ≥0∞
y : ℝ≥0
h_le : (↑y : ℝ≥0∞) ≤ x
top : ∀ (h_le : (↑y : ℝ≥0∞) ≤ ∞), (↑(∞ - (↑y : ℝ≥0∞)) : EReal) = (↑∞ : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
⊢ (↑(x - (↑y : ℝ≥0∞)) : EReal) = (↑x : EReal) - (↑(↑y : ℝ≥0∞) : EReal)
have coe : ∀ (x : ℝ≥0) (h_le : (↑y : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)),
  (↑((↑x : ℝ≥0∞) - (↑y : ℝ≥0∞)) : EReal) = (↑(↑x : ℝ≥0∞) : 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]
Cleared hypotheses: x, h_le
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : 0 < x
⊢ ⊤ * x = ⊤
have rw : x * ⊤ = ⊤
Tactic: rw [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x < 0
⊢ ⊤ * x = ⊥
have rw : x * ⊤ = ⊥
Tactic: rw [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ 0
⊢ (↑x : EReal) * ⊤ = ⊤
have rw : ⊤ * (↑x : EReal) = ⊤
Tactic: rw [EReal.mul_comm, top_mul_coe_ennreal hx]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ 0
rw : ⊤ * (↑x : EReal) = ⊤
⊢ (↑x : EReal) * ⊤ = ⊤
have rw₁ : Eq (α := EReal) ⊤ ⊤
Tactic: rw [EReal.mul_comm, top_mul_coe_ennreal hx]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : 0 < x
⊢ ⊥ * x = ⊥
have rw : x * ⊥ = ⊥
Tactic: rw [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x < 0
⊢ ⊥ * x = ⊤
have rw : x * ⊥ = ⊤
Tactic: rw [EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : (x * y).toReal = x.toReal * y.toReal
⊢ (y * x).toReal = y.toReal * x.toReal
have symm : (y * x).toReal = x.toReal * y.toReal
Tactic: rwa [mul_comm, EReal.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
⊢ ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
have coe_coe : (↑(x * y) : EReal).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
Tactic: norm_cast