awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
hx : x ≠ ⊤
⊢ ⊤ - x = ⊤
have bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
hx : x ≠ ⊤
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
⊢ ⊤ - x = ⊤
have coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊤), ⊤ - (↑a : EReal) = ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
hx : x ≠ ⊤
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊤), ⊤ - (↑a : EReal) = ⊤
⊢ ⊤ - x = ⊤
have top : ∀ (hx : Ne (α := EReal) ⊤ ⊤), HSub.hSub (α := EReal) ⊤ ⊤ = ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
⊢ x - x = 0
have bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = 0
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = 0
⊢ x - x = 0
have coe : ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥), (↑a : EReal) - (↑a : EReal) = 0
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = 0
coe : ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥), (↑a : EReal) - (↑a : EReal) = 0
⊢ x - x = 0
have top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥), HSub.hSub (α := EReal) ⊤ ⊤ = 0
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
⊢ x - x ≤ 0
have bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0
⊢ x - x ≤ 0
have coe : ∀ (a : ℝ), (↑a : EReal) - (↑a : EReal) ≤ 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0
coe : ∀ (a : ℝ), (↑a : EReal) - (↑a : EReal) ≤ 0
⊢ x - x ≤ 0
have top : HSub.hSub (α := EReal) ⊤ ⊤ ≤ 0
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x
have bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), 0 ≤ ⊥ - y ↔ y ≤ ⊥
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), 0 ≤ ⊥ - y ↔ y ≤ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x
have coe : ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥), 0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), 0 ≤ ⊥ - y ↔ y ≤ ⊥
coe :
  ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥),
    0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
⊢ 0 ≤ x - y ↔ y ≤ x
have top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥), 0 ≤ ⊤ - y ↔ y ≤ ⊤
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥
have bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  0 ≤ HSub.hSub (α := EReal) ⊥ ⊥ ↔ LE.le (α := EReal) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
bot :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊥ ⊥ ↔ LE.le (α := EReal) ⊥ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥
have bot₁ : ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥),
  0 ≤ ⊥ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
bot :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊥ ⊥ ↔ LE.le (α := EReal) ⊥ ⊥
bot₁ :
  ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥),
    0 ≤ ⊥ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊥
⊢ 0 ≤ ⊥ - y ↔ y ≤ ⊥
have bot₂ : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  0 ≤ HSub.hSub (α := EReal) ⊥ ⊤ ↔ LE.le (α := EReal) ⊤ ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
have coe : ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  0 ≤ (↑a : EReal) - ⊥ ↔ ⊥ ≤ (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
coe :
  ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ (↑a : EReal) - ⊥ ↔ ⊥ ≤ (↑a : EReal)
⊢ 0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
have coe₁ : ∀ (a_1 : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊥),
  0 ≤ (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) ≤ (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
coe :
  ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ (↑a : EReal) - ⊥ ↔ ⊥ ≤ (↑a : EReal)
coe₁ :
  ∀ (a_1 : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊥),
    0 ≤ (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) ≤ (↑a : EReal)
⊢ 0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
have coe₂ : ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  0 ≤ (↑a : EReal) - ⊤ ↔ ⊤ ≤ (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤
have top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  0 ≤ HSub.hSub (α := EReal) ⊤ ⊥ ↔ LE.le (α := EReal) ⊥ ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
top :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊤ ⊥ ↔ LE.le (α := EReal) ⊥ ⊤
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤
have top₁ : ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥),
  0 ≤ ⊤ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
top :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊤ ⊥ ↔ LE.le (α := EReal) ⊥ ⊤
top₁ :
  ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥),
    0 ≤ ⊤ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊤
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤
have top₂ : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  0 ≤ HSub.hSub (α := EReal) ⊤ ⊤ ↔ LE.le (α := EReal) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y
have bot : ⊥ - y ≤ 0 ↔ ⊥ ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : ⊥ - y ≤ 0 ↔ ⊥ ≤ y
⊢ x - y ≤ 0 ↔ x ≤ y
have coe : ∀ (a : ℝ), (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : ⊥ - y ≤ 0 ↔ ⊥ ≤ y
coe : ∀ (a : ℝ), (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
⊢ x - y ≤ 0 ↔ x ≤ y
have top : ⊤ - y ≤ 0 ↔ ⊤ ≤ y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y
have bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊥
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y
have bot₁ : ∀ (a : ℝ), ⊥ - (↑a : EReal) ≤ 0 ↔ ⊥ ≤ (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), ⊥ - (↑a : EReal) ≤ 0 ↔ ⊥ ≤ (↑a : EReal)
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y
have bot₂ : HSub.hSub (α := EReal) ⊥ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
⊢ (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
have coe : (↑a : EReal) - ⊥ ≤ 0 ↔ (↑a : EReal) ≤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) - ⊥ ≤ 0 ↔ (↑a : EReal) ≤ ⊥
⊢ (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
have coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) - (↑a_1 : EReal) ≤ 0 ↔ (↑a : EReal) ≤ (↑a_1 : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) - ⊥ ≤ 0 ↔ (↑a : EReal) ≤ ⊥
coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) - (↑a_1 : EReal) ≤ 0 ↔ (↑a : EReal) ≤ (↑a_1 : EReal)
⊢ (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
have coe₂ : (↑a : EReal) - ⊤ ≤ 0 ↔ (↑a : EReal) ≤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y
have top : HSub.hSub (α := EReal) ⊤ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : HSub.hSub (α := EReal) ⊤ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊥
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y
have top₁ : ∀ (a : ℝ), ⊤ - (↑a : EReal) ≤ 0 ↔ ⊤ ≤ (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : HSub.hSub (α := EReal) ⊤ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊥
top₁ : ∀ (a : ℝ), ⊤ - (↑a : EReal) ≤ 0 ↔ ⊤ ≤ (↑a : EReal)
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y
have top₂ : HSub.hSub (α := EReal) ⊤ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ 0 < x - y ↔ y < x
have bot : 0 < ⊥ - y ↔ y < ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : 0 < ⊥ - y ↔ y < ⊥
⊢ 0 < x - y ↔ y < x
have coe : ∀ (a : ℝ), 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
bot : 0 < ⊥ - y ↔ y < ⊥
coe : ∀ (a : ℝ), 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
⊢ 0 < x - y ↔ y < x
have top : 0 < ⊤ - y ↔ y < ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ 0 < ⊥ - y ↔ y < ⊥
have bot : 0 < HSub.hSub (α := EReal) ⊥ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : 0 < HSub.hSub (α := EReal) ⊥ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊥
⊢ 0 < ⊥ - y ↔ y < ⊥
have bot₁ : ∀ (a : ℝ), 0 < ⊥ - (↑a : EReal) ↔ (↑a : EReal) < ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
bot : 0 < HSub.hSub (α := EReal) ⊥ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), 0 < ⊥ - (↑a : EReal) ↔ (↑a : EReal) < ⊥
⊢ 0 < ⊥ - y ↔ y < ⊥
have bot₂ : 0 < HSub.hSub (α := EReal) ⊥ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊥
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
⊢ 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
have coe : 0 < (↑a : EReal) - ⊥ ↔ ⊥ < (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : 0 < (↑a : EReal) - ⊥ ↔ ⊥ < (↑a : EReal)
⊢ 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
have coe₁ : ∀ (a_1 : ℝ), 0 < (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) < (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
coe : 0 < (↑a : EReal) - ⊥ ↔ ⊥ < (↑a : EReal)
coe₁ : ∀ (a_1 : ℝ), 0 < (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) < (↑a : EReal)
⊢ 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
have coe₂ : 0 < (↑a : EReal) - ⊤ ↔ ⊤ < (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
⊢ 0 < ⊤ - y ↔ y < ⊤
have top : 0 < HSub.hSub (α := EReal) ⊤ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : 0 < HSub.hSub (α := EReal) ⊤ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊤
⊢ 0 < ⊤ - y ↔ y < ⊤
have top₁ : ∀ (a : ℝ), 0 < ⊤ - (↑a : EReal) ↔ (↑a : EReal) < ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : 0 < HSub.hSub (α := EReal) ⊤ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊤
top₁ : ∀ (a : ℝ), 0 < ⊤ - (↑a : EReal) ↔ (↑a : EReal) < ⊤
⊢ 0 < ⊤ - y ↔ y < ⊤
have top₂ : 0 < HSub.hSub (α := EReal) ⊤ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y
have bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), ⊥ - y < 0 ↔ ⊥ < y
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), ⊥ - y < 0 ↔ ⊥ < y
⊢ x - y < 0 ↔ x < y
have coe : ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥), (↑a : EReal) - y < 0 ↔ (↑a : EReal) < y
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥), ⊥ - y < 0 ↔ ⊥ < y
coe :
  ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥),
    (↑a : EReal) - y < 0 ↔ (↑a : EReal) < y
⊢ x - y < 0 ↔ x < y
have top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥), ⊤ - y < 0 ↔ ⊤ < y
Tactic: cases x
Cleared hypotheses: x, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
⊢ ⊥ - y < 0 ↔ ⊥ < y
have bot : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  HSub.hSub (α := EReal) ⊥ ⊥ < 0 ↔ LT.lt (α := EReal) ⊥ ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
bot :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    HSub.hSub (α := EReal) ⊥ ⊥ < 0 ↔ LT.lt (α := EReal) ⊥ ⊥
⊢ ⊥ - y < 0 ↔ ⊥ < y
have bot₁ : ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥),
  ⊥ - (↑a : EReal) < 0 ↔ ⊥ < (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊥
bot :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    HSub.hSub (α := EReal) ⊥ ⊥ < 0 ↔ LT.lt (α := EReal) ⊥ ⊥
bot₁ :
  ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥),
    ⊥ - (↑a : EReal) < 0 ↔ ⊥ < (↑a : EReal)
⊢ ⊥ - y < 0 ↔ ⊥ < y
have bot₂ : ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  HSub.hSub (α := EReal) ⊥ ⊤ < 0 ↔ LT.lt (α := EReal) ⊥ ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
⊢ (↑a : EReal) - y < 0 ↔ (↑a : EReal) < y
have coe : ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  (↑a : EReal) - ⊥ < 0 ↔ (↑a : EReal) < ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
coe :
  ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    (↑a : EReal) - ⊥ < 0 ↔ (↑a : EReal) < ⊥
⊢ (↑a : EReal) - y < 0 ↔ (↑a : EReal) < y
have coe₁ : ∀ (a_1 : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊥),
  (↑a : EReal) - (↑a_1 : EReal) < 0 ↔ (↑a : EReal) < (↑a_1 : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥
coe :
  ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    (↑a : EReal) - ⊥ < 0 ↔ (↑a : EReal) < ⊥
coe₁ :
  ∀ (a_1 : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊥),
    (↑a : EReal) - (↑a_1 : EReal) < 0 ↔ (↑a : EReal) < (↑a_1 : EReal)
⊢ (↑a : EReal) - y < 0 ↔ (↑a : EReal) < y
have coe₂ : ∀ (h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  (↑a : EReal) - ⊤ < 0 ↔ (↑a : EReal) < ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
⊢ ⊤ - y < 0 ↔ ⊤ < y
have top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
  HSub.hSub (α := EReal) ⊤ ⊥ < 0 ↔ LT.lt (α := EReal) ⊤ ⊥
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
top :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    HSub.hSub (α := EReal) ⊤ ⊥ < 0 ↔ LT.lt (α := EReal) ⊤ ⊥
⊢ ⊤ - y < 0 ↔ ⊤ < y
have top₁ : ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥),
  ⊤ - (↑a : EReal) < 0 ↔ ⊤ < (↑a : EReal)
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥
top :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥),
    HSub.hSub (α := EReal) ⊤ ⊥ < 0 ↔ LT.lt (α := EReal) ⊤ ⊥
top₁ :
  ∀ (a : ℝ) (h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥),
    ⊤ - (↑a : EReal) < 0 ↔ ⊤ < (↑a : EReal)
⊢ ⊤ - y < 0 ↔ ⊤ < y
have top₂ : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
  HSub.hSub (α := EReal) ⊤ ⊤ < 0 ↔ LT.lt (α := EReal) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y, h_top, h_bot
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
have inl : ∀ (h : 0 ≤ x), (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
Tactic: rcases le_total 0 x with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
inl : ∀ (h : 0 ≤ x), (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
have inr : ∀ (h : x ≤ 0), (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
Tactic: rcases le_total 0 x with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
have inl : ∀ (x : ℝ≥0), (↑(↑x : ℝ) : EReal) = (↑(↑(↑x : ℝ).toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-(↑x : ℝ)).toNNReal : ℝ≥0∞) : EReal)
Tactic: lift x to ℝ≥0 using h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ) : EReal) = (↑(↑(↑x : ℝ).toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-(↑x : ℝ)).toNNReal : ℝ≥0∞) : EReal)
have inl : (↑(↑x : ℝ) : EReal) = (↑(↑x : ℝ≥0∞) : EReal)
Tactic: rw [Real.toNNReal_of_nonpos (neg_nonpos.mpr x.coe_nonneg), Real.toNNReal_coe, ENNReal.coe_zero,
      coe_ennreal_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : x ≤ 0
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
have inr : 0 ≤ -x
Tactic: rw [Real.toNNReal_of_nonpos h, ENNReal.coe_zero, coe_ennreal_zero, coe_nnreal_eq_coe_real,
      Real.coe_toNNReal, zero_sub, coe_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x - y).toReal = x.toReal - y.toReal
have lift : ∀ (x : ℝ) (hx : (↑x : EReal) ≠ ⊤) (h'x : (↑x : EReal) ≠ ⊥), ((↑x : EReal) - y).toReal = (↑x : EReal).toReal - y.toReal
Tactic: lift x to ℝ using ⟨hx, h'x⟩
Cleared hypotheses: x, hx, h'x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : (↑x : EReal) ≠ ⊤
h'x : (↑x : EReal) ≠ ⊥
⊢ ((↑x : EReal) - y).toReal = (↑x : EReal).toReal - y.toReal
have lift : ∀ (y : ℝ) (hy : (↑y : EReal) ≠ ⊤) (h'y : (↑y : EReal) ≠ ⊥),
  ((↑x : EReal) - (↑y : EReal)).toReal = (↑x : EReal).toReal - (↑y : EReal).toReal
Tactic: lift y to ℝ using ⟨hy, h'y⟩
Cleared hypotheses: y, hy, h'y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : 0 ≤ y
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal
have bot : (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
Tactic: induction x
Cleared hypotheses: x