awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥
bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁ : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₄ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₆ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₇ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₈ bot₉ bot₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₁ bot₁₂ bot₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥
bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁ : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₄ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₆ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₇ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₈ bot₉ bot₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₁ bot₁₂ bot₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊤ = HSub.hSub (α := EReal) (-⊥) ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊤ = HSub.hSub (α := EReal) (-⊥) ⊤

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₂ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₅ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₆ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₇ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₈ coe₉ coe₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₁ coe₁₂ coe₁₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₅ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₂ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₅ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₆ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₇ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₈ coe₉ coe₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₁ coe₁₂ coe₁₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁₅ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₂ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₃ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₅ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₆ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₇ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₈ coe₉ coe₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₁ coe₁₂ coe₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₂ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₃ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₅ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₆ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₇ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₈ coe₉ coe₁₀ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₁ coe₁₂ coe₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₄ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
coe₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊥ = HSub.hSub (α := EReal) (-⊤) ⊥

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊥ = HSub.hSub (α := EReal) (-⊤) ⊥

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₄ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₆ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₇ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₈ top₉ top₁₀ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₁ top₁₂ top₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₄ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₄ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₆ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₇ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₈ top₉ top₁₀ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₁ top₁₂ top₁₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₄ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁₅ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₁ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₂ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₃ :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₄ top₅ top₆ top₇ top₈ top₉ :
  ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₁ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₂ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₃ :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₄ top₅ top₆ top₇ top₈ top₉ :
  ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤

Tactic:
try tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊥
coe : -(↑(a + a_1) : EReal) = -(↑a : EReal) - (↑a_1 : EReal)
coe₁ : (↑(-(a + a_1)) : EReal) = -(↑a : EReal) - (↑a_1 : EReal)
coe₂ : (↑(-(a + a_1)) : EReal) = (↑(-a) : EReal) - (↑a_1 : EReal)
coe₃ : (↑(-(a + a_1)) : EReal) = (↑(-a - a_1) : EReal)
coe₄ coe₅ : (↑(-a - a_1) : EReal) = (↑(-a - a_1) : EReal)
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)

Tactic:
rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

Premises used: EReal.coe_neg, EReal.coe_sub, neg_add', EReal.coe_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
rw : x ≠ ⊥ ∨ -y ≠ ⊤
rw₁ : x ≠ ⊤ ∨ -y ≠ ⊥
⊢ -(x - y) = -x + y

Tactic:
rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg]

Premises used: sub_eq_add_neg, neg_neg, EReal.neg_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊥ ∨ -y ≠ ⊤

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ x ≠ ⊤ ∨ -y ≠ ⊥

Tactic:
simp_all
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : EReal
hx : ¬0 ≤ x
⊢ 0 < -x

Tactic:
simpa using hx
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
rw : x = - -x
rw₁ rw₂ : x = x
⊢ x = -(↑(-x).toENNReal : EReal)

Tactic:
rw [coe_toENNReal H₁.le, neg_neg]

Premises used: neg_neg, LT.lt.le, EReal.coe_toENNReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
H₂ : x = -(↑(-x).toENNReal : EReal)
⊢ 0 < (-x).toENNReal

Tactic:
positivity
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : ℝ≥0∞
suffices : ∀ (y : EReal), (↑x : EReal) = y → recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y ≍ coe x
⊢ recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe (↑x : EReal) = coe x

Tactic:
suffices ∀ y : EReal, x = y → (recENNReal coe neg_coe y : motive y) ≍ coe x from
    heq_iff_eq.mp (this x rfl)
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : ℝ≥0∞
y : EReal
hy : (↑x : EReal) = y
⊢ 0 ≤ y

Tactic:
have H₁ : 0 ≤ y := hy ▸ coe_ennreal_nonneg x
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : ℝ≥0∞
y : EReal
hy : (↑x : EReal) = y
H₁ : 0 ≤ y
⊢ y.toENNReal = x

Tactic:
simp [← hy]
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : ℝ≥0∞
y : EReal
hy : (↑x : EReal) = y
H₁ : 0 ≤ y
obtain :
  ∀ (hy : (↑y.toENNReal : EReal) = y),
    HEq (recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y) (β := motive (↑y.toENNReal : EReal))
      (coe y.toENNReal)
⊢ recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y ≍ coe x

Tactic:
obtain rfl : y.toENNReal = x := by simp [← hy]

Premises used: EReal.toENNReal, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
y : EReal
H₁ : 0 ≤ y
hy : (↑y.toENNReal : EReal) = y
⊢ HEq (recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y) (β := motive (↑y.toENNReal : EReal))
    (coe y.toENNReal)

Tactic:
simp [recENNReal, H₁]
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ ⊥ - x = ⊥

Tactic:
bot_add x

Premises used: EReal.bot_add, SubNegMonoid.sub', WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ x - ⊤ = ⊥

Tactic:
add_bot x

Premises used: EReal.add_bot, SubNegMonoid.sub', EReal.neg, WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊤ ⊥ = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, SubNegMonoid.sub', WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
⊢ ⊤ - (↑x : EReal) = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, SubNegMonoid.sub', WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
⊢ (↑x : EReal) - ⊥ = ⊤

Tactic:
rfl

Premises used: WithBot.some, WithTop.map₂, SubNegMonoid.sub', WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = ⊤
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), (↑a : EReal) - ⊥ = ⊤
top : ∀ (h : Ne (α := EReal) ⊤ ⊥), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
⊢ x - ⊥ = ⊤

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ ⊥
⊢ HSub.hSub (α := EReal) ⊥ ⊥ = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ ⊥
⊢ (↑a : EReal) - ⊥ = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ ⊥
⊢ HSub.hSub (α := EReal) ⊤ ⊥ = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
hx : x ≠ ⊤
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊤), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊤), ⊤ - (↑a : EReal) = ⊤
top : ∀ (hx : Ne (α := EReal) ⊤ ⊤), HSub.hSub (α := EReal) ⊤ ⊤ = ⊤
⊢ ⊤ - x = ⊤

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : Ne (α := EReal) ⊥ ⊤
⊢ HSub.hSub (α := EReal) ⊤ ⊥ = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : (↑a : EReal) ≠ ⊤
⊢ ⊤ - (↑a : EReal) = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
hx : Ne (α := EReal) ⊤ ⊤
⊢ HSub.hSub (α := EReal) ⊤ ⊤ = ⊤

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
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
top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥), HSub.hSub (α := EReal) ⊤ ⊤ = 0
⊢ x - x = 0

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
h_top : Ne (α := EReal) ⊥ ⊤
h_bot : Ne (α := EReal) ⊥ ⊥
⊢ HSub.hSub (α := EReal) ⊥ ⊥ = 0

Tactic:
simp_all [← coe_sub]

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

Tactic:
simp_all [← coe_sub]

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

Tactic:
simp_all [← coe_sub]

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

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

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (↑a : EReal) - (↑a : EReal) ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HSub.hSub (α := EReal) ⊤ ⊤ ≤ 0

Tactic:
simp
-- 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 ≠ ⊥), 0 ≤ ⊥ - y ↔ y ≤ ⊥
coe :
  ∀ (a : ℝ) (h_top : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊤) (h_bot : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊥),
    0 ≤ (↑a : EReal) - y ↔ y ≤ (↑a : EReal)
top : ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊥), 0 ≤ ⊤ - y ↔ y ≤ ⊤
⊢ 0 ≤ x - y ↔ y ≤ x

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) ⊥ ⊥),
    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) ≤ ⊥
bot₂ :
  ∀ (h_top : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊥ ⊤ ↔ LE.le (α := EReal) ⊤ ⊥
⊢ 0 ≤ ⊥ - y ↔ 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) ⊥ ⊥),
    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)
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)

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) ⊥ ⊥),
    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) ≤ ⊤
top₂ :
  ∀ (h_top : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊤) (h_bot : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊥),
    0 ≤ HSub.hSub (α := EReal) ⊤ ⊤ ↔ LE.le (α := EReal) ⊤ ⊤
⊢ 0 ≤ ⊤ - y ↔ y ≤ ⊤

Tactic:
cases y
-- 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