awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥
⊢ 0 ≤ ⊥ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ 0 ≤ HSub.hSub (α := EReal) ⊥ ⊤ ↔ LE.le (α := EReal) ⊤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥
⊢ 0 ≤ (↑a : EReal) - ⊥ ↔ ⊥ ≤ (↑a : EReal)

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a 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:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ 0 ≤ (↑a : EReal) - ⊤ ↔ ⊤ ≤ (↑a : EReal)

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥
⊢ 0 ≤ HSub.hSub (α := EReal) ⊤ ⊥ ↔ LE.le (α := EReal) ⊥ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥
⊢ 0 ≤ ⊤ - (↑a : EReal) ↔ (↑a : EReal) ≤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ 0 ≤ HSub.hSub (α := EReal) ⊤ ⊤ ↔ LE.le (α := EReal) ⊤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
bot : ⊥ - y ≤ 0 ↔ ⊥ ≤ y
coe : ∀ (a : ℝ), (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y
top : ⊤ - y ≤ 0 ↔ ⊤ ≤ y
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
bot : HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), ⊥ - (↑a : EReal) ≤ 0 ↔ ⊥ ≤ (↑a : EReal)
bot₂ : HSub.hSub (α := EReal) ⊥ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊤
⊢ ⊥ - y ≤ 0 ↔ ⊥ ≤ y

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
coe : (↑a : EReal) - ⊥ ≤ 0 ↔ (↑a : EReal) ≤ ⊥
coe₁ : ∀ (a_1 : ℝ), (↑a : EReal) - (↑a_1 : EReal) ≤ 0 ↔ (↑a : EReal) ≤ (↑a_1 : EReal)
coe₂ : (↑a : EReal) - ⊤ ≤ 0 ↔ (↑a : EReal) ≤ ⊤
⊢ (↑a : EReal) - y ≤ 0 ↔ (↑a : EReal) ≤ y

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
top : HSub.hSub (α := EReal) ⊤ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊥
top₁ : ∀ (a : ℝ), ⊤ - (↑a : EReal) ≤ 0 ↔ ⊤ ≤ (↑a : EReal)
top₂ : HSub.hSub (α := EReal) ⊤ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊤
⊢ ⊤ - y ≤ 0 ↔ ⊤ ≤ y

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊥ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ⊥ - (↑a : EReal) ≤ 0 ↔ ⊥ ≤ (↑a : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊥ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊥ ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (↑a : EReal) - ⊥ ≤ 0 ↔ (↑a : EReal) ≤ ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
⊢ (↑a : EReal) - (↑a_1 : EReal) ≤ 0 ↔ (↑a : EReal) ≤ (↑a_1 : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (↑a : EReal) - ⊤ ≤ 0 ↔ (↑a : EReal) ≤ ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊤ ⊥ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ⊤ - (↑a : EReal) ≤ 0 ↔ ⊤ ≤ (↑a : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊤ ⊤ ≤ 0 ↔ LE.le (α := EReal) ⊤ ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
bot : 0 < ⊥ - y ↔ y < ⊥
coe : ∀ (a : ℝ), 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)
top : 0 < ⊤ - y ↔ y < ⊤
⊢ 0 < x - y ↔ y < x

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
bot : 0 < HSub.hSub (α := EReal) ⊥ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊥
bot₁ : ∀ (a : ℝ), 0 < ⊥ - (↑a : EReal) ↔ (↑a : EReal) < ⊥
bot₂ : 0 < HSub.hSub (α := EReal) ⊥ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊥
⊢ 0 < ⊥ - y ↔ y < ⊥

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
coe : 0 < (↑a : EReal) - ⊥ ↔ ⊥ < (↑a : EReal)
coe₁ : ∀ (a_1 : ℝ), 0 < (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) < (↑a : EReal)
coe₂ : 0 < (↑a : EReal) - ⊤ ↔ ⊤ < (↑a : EReal)
⊢ 0 < (↑a : EReal) - y ↔ y < (↑a : EReal)

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
top : 0 < HSub.hSub (α := EReal) ⊤ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊤
top₁ : ∀ (a : ℝ), 0 < ⊤ - (↑a : EReal) ↔ (↑a : EReal) < ⊤
top₂ : 0 < HSub.hSub (α := EReal) ⊤ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊤
⊢ 0 < ⊤ - y ↔ y < ⊤

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HSub.hSub (α := EReal) ⊥ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ 0 < ⊥ - (↑a : EReal) ↔ (↑a : EReal) < ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HSub.hSub (α := EReal) ⊥ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊥

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ 0 < (↑a : EReal) - ⊥ ↔ ⊥ < (↑a : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
⊢ 0 < (↑a : EReal) - (↑a_1 : EReal) ↔ (↑a_1 : EReal) < (↑a : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ 0 < (↑a : EReal) - ⊤ ↔ ⊤ < (↑a : EReal)

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HSub.hSub (α := EReal) ⊤ ⊥ ↔ LT.lt (α := EReal) ⊥ ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ 0 < ⊤ - (↑a : EReal) ↔ (↑a : EReal) < ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HSub.hSub (α := EReal) ⊤ ⊤ ↔ LT.lt (α := EReal) ⊤ ⊤

Tactic:
simp [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
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
top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥), ⊤ - y < 0 ↔ ⊤ < y
⊢ x - y < 0 ↔ x < y

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
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)
bot₂ :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
    HSub.hSub (α := EReal) ⊥ ⊤ < 0 ↔ LT.lt (α := EReal) ⊥ ⊤
⊢ ⊥ - y < 0 ↔ ⊥ < y

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
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)
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

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
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)
top₂ :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
    HSub.hSub (α := EReal) ⊤ ⊤ < 0 ↔ LT.lt (α := EReal) ⊤ ⊤
⊢ ⊤ - y < 0 ↔ ⊤ < y

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊥
⊢ HSub.hSub (α := EReal) ⊥ ⊥ < 0 ↔ LT.lt (α := EReal) ⊥ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊥
⊢ ⊥ - (↑a : EReal) < 0 ↔ ⊥ < (↑a : EReal)

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ HSub.hSub (α := EReal) ⊥ ⊤ < 0 ↔ LT.lt (α := EReal) ⊥ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊥
⊢ (↑a : EReal) - ⊥ < 0 ↔ (↑a : EReal) < ⊥

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a 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:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ (↑a : EReal) - ⊤ < 0 ↔ (↑a : EReal) < ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊥
⊢ HSub.hSub (α := EReal) ⊤ ⊥ < 0 ↔ LT.lt (α := EReal) ⊤ ⊥

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_top : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊥
⊢ ⊤ - (↑a : EReal) < 0 ↔ ⊤ < (↑a : EReal)

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤
h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥
⊢ HSub.hSub (α := EReal) ⊤ ⊤ < 0 ↔ LT.lt (α := EReal) ⊤ ⊤

Tactic:
simp_all [← EReal.coe_sub]

Premises used: EReal.coe_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x ≤ y
h' : t ≤ z
⊢ x - z ≤ y - t

Tactic:
add_le_add h (neg_le_neg_iff.2 h')

Premises used: Iff.mpr, EReal.neg_le_neg_iff, add_le_add, SubNegMonoid.sub', WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥

Tactic:
simp [ht]
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -z ≠ ⊤

Tactic:
simp [hz]
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
inl : ∀ (h : 0 ≤ x), (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
inr : ∀ (h : x ≤ 0), (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)

Tactic:
rcases le_total 0 x with (h | h)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x

Tactic:
h
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 ≤ x
inl :
  ∀ (x : ℝ≥0), (↑(↑x : ℝ) : EReal) = (↑(↑(↑x : ℝ).toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-(↑x : ℝ)).toNNReal : ℝ≥0∞) : EReal)
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)

Tactic:
lift x to ℝ≥0 using h
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ≥0
inl : (↑(↑x : ℝ) : EReal) = (↑(↑x : ℝ≥0∞) : EReal)
⊢ (↑(↑x : ℝ) : EReal) = (↑(↑(↑x : ℝ).toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-(↑x : ℝ)).toNNReal : ℝ≥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]

Premises used: Iff.mpr, sub_zero, EReal.coe_ennreal_zero, neg_nonpos, ENNReal.coe_zero, Real.toNNReal_of_nonpos, NNReal.coe_nonneg, Real.toNNReal_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ≥0
⊢ (↑(↑x : ℝ) : EReal) = (↑(↑x : ℝ≥0∞) : EReal)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x ≤ 0
inr : 0 ≤ -x
⊢ (↑x : EReal) = (↑(↑x.toNNReal : ℝ≥0∞) : EReal) - (↑(↑(-x).toNNReal : ℝ≥0∞) : EReal)

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]

Premises used: EReal.coe_neg, EReal.coe_ennreal_zero, neg_neg, Real.coe_toNNReal, ENNReal.coe_zero, Real.toNNReal_of_nonpos, EReal.coe_nnreal_eq_coe_real, zero_sub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
neg_nonneg.2 h

Premises used: Iff.mpr, neg_nonneg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 ≤ -x

Tactic:
exact neg_nonneg.2 h

Premises used: Iff.mpr, neg_nonneg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
lift :
  ∀ (x : ℝ) (hx : (↑x : EReal) ≠ ⊤) (h'x : (↑x : EReal) ≠ ⊥), ((↑x : EReal) - y).toReal = (↑x : EReal).toReal - y.toReal
⊢ (x - y).toReal = x.toReal - y.toReal

Tactic:
lift x to ℝ using ⟨hx, h'x⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊤
h'y : y ≠ ⊥
x : ℝ
hx : (↑x : EReal) ≠ ⊤
h'x : (↑x : EReal) ≠ ⊥
lift :
  ∀ (y : ℝ) (hy : (↑y : EReal) ≠ ⊤) (h'y : (↑y : EReal) ≠ ⊥),
    ((↑x : EReal) - (↑y : EReal)).toReal = (↑x : EReal).toReal - (↑y : EReal).toReal
⊢ ((↑x : EReal) - y).toReal = (↑x : EReal).toReal - y.toReal

Tactic:
lift y to ℝ using ⟨hy, h'y⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx : (↑x : EReal) ≠ ⊤
h'x : (↑x : EReal) ≠ ⊥
y : ℝ
hy : (↑y : EReal) ≠ ⊤
h'y : (↑y : EReal) ≠ ⊥
⊢ ((↑x : EReal) - (↑y : EReal)).toReal = (↑x : EReal).toReal - (↑y : EReal).toReal

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hy : 0 ≤ y
bot : (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal
coe : ∀ (a : ℝ), ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal
top : (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
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
bot₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HSub.hSub (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ - toENNReal ⊤
⊢ (⊥ - y).toENNReal = toENNReal ⊥ - y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
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
coe₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), ((↑a : EReal) - ⊤).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊤
⊢ ((↑a : EReal) - y).toENNReal = (↑a : EReal).toENNReal - y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
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
top₂ : ∀ (hy : LE.le (α := EReal) 0 ⊤), (HSub.hSub (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ - toENNReal ⊤
⊢ (⊤ - y).toENNReal = toENNReal ⊤ - y.toENNReal

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ - toENNReal ⊥

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ - (↑a : EReal)).toENNReal = toENNReal ⊥ - (↑a : EReal).toENNReal

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ - (↑a : EReal)).toENNReal = toENNReal ⊥ - (↑a : EReal).toENNReal

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊥ - (↑a : EReal)).toENNReal = toENNReal ⊥ - (↑a : EReal).toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ - toENNReal ⊤

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ - toENNReal ⊤

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ - toENNReal ⊤

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊥
⊢ ((↑a : EReal) - ⊥).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊥

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
hy : 0 ≤ (↑a_1 : EReal)
⊢ ((↑a : EReal) - (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal - (↑a_1 : EReal).toENNReal

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) - ⊤).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊤

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) - ⊤).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊤

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : LE.le (α := EReal) 0 ⊤
⊢ ((↑a : EReal) - ⊤).toENNReal = (↑a : EReal).toENNReal - toENNReal ⊤

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊥
⊢ (HSub.hSub (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ - toENNReal ⊥

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ - (↑a : EReal)).toENNReal = toENNReal ⊤ - (↑a : EReal).toENNReal

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ - (↑a : EReal)).toENNReal = toENNReal ⊤ - (↑a : EReal).toENNReal

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hy : 0 ≤ (↑a : EReal)
⊢ (⊤ - (↑a : EReal)).toENNReal = toENNReal ⊤ - (↑a : EReal).toENNReal

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ - toENNReal ⊤

Tactic:
simp_all [zero_tsub, ENNReal.sub_top]

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ - toENNReal ⊤

Tactic:
{· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
hy : LE.le (α := EReal) 0 ⊤
⊢ (HSub.hSub (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ - toENNReal ⊤

Tactic:
try {· simp_all [zero_tsub, ENNReal.sub_top]}

Premises used: ENNReal.sub_top, zero_tsub
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
pos : ∀ (hxy : x ≤ y), ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
neg : ∀ (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

Tactic:
by_cases hxy : x ≤ y
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
hy : 0 ≤ (↑y : EReal)
hxy : x ≤ y
pos : 0 = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal
⊢ ((↑x : EReal) - (↑y : EReal)).toENNReal = (↑x : EReal).toENNReal - (↑y : EReal).toENNReal

Tactic:
rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]

Premises used: Iff.mpr, EReal.coe_le_coe_iff, EReal.sub_nonpos, EReal.toENNReal_of_nonpos