awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊥).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊥

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
⊢ ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊤).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊤

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

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ ((↑a : EReal) + ⊤).toENNReal ≤ (↑a : EReal).toENNReal + toENNReal ⊤

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (⊤ + (↑a : EReal)).toENNReal ≤ toENNReal ⊤ + (↑a : EReal).toENNReal

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

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
⊢ (⊤ + (↑a : EReal)).toENNReal ≤ toENNReal ⊤ + (↑a : EReal).toENNReal

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal ≤ toENNReal ⊤ + toENNReal ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal ≤ toENNReal ⊤ + toENNReal ⊤

Tactic:
{· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal ≤ toENNReal ⊤ + toENNReal ⊤

Tactic:
try {· simp}
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
⊢ ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal

Tactic:
ENNReal.ofReal_add_le

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, EReal.toENNReal, ENNReal.ofReal_add_le, EReal.toReal, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
⊢ ((↑a : EReal) + (↑a_1 : EReal)).toENNReal ≤ (↑a : EReal).toENNReal + (↑a_1 : EReal).toENNReal

Tactic:
exact ENNReal.ofReal_add_le

Premises used: ENNReal.ofReal_add_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
x z : ℝ
h : (↑x : EReal) + ⊤ ≤ (↑x : EReal) + (↑z : EReal)
⊢ ⊤ ≤ (↑z : EReal)

Tactic:
simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h

Premises used: EReal.coe_add_top, top_le_iff, EReal.coe_ne_top, EReal.coe_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
x_1 : EReal
h : (↑x : EReal) + x_1 ≤ (↑x : EReal) + ⊥
⊢ x_1 ≤ ⊥

Tactic:
simpa using h
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z : ℝ
h : (↑x : EReal) + (↑y : EReal) ≤ (↑x : EReal) + (↑z : EReal)
⊢ (↑y : EReal) ≤ (↑z : EReal)

Tactic:
simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

Premises used: EReal.coe_le_coe_iff, add_le_add_iff_left, EReal.coe_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x < y
z : ℝ
⊢ x + (↑z : EReal) < y + (↑z : EReal)

Tactic:
not_le.1 <| mt (addLECancellable_coe z).add_le_add_iff_right.1 h.not_ge

Premises used: not_le, EReal.addLECancellable_coe, mt, AddLECancellable.add_le_add_iff_right, Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x < y
z : ℝ
⊢ (↑z : EReal) + x < (↑z : EReal) + y

Tactic:
simpa [add_comm] using add_lt_add_right_coe h z

Premises used: add_comm, EReal.add_lt_add_right_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
inl : ∀ (h1 : ⊥ < y), ⊥ + z < y + t
inr : ∀ (hx : x ≠ ⊥), x + z < y + t
⊢ x + z < y + t

Tactic:
rcases eq_or_ne x ⊥ with (rfl | hx)

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

Tactic:
simp [h1, bot_le.trans_lt h2]

Premises used: LE.le.trans_lt, bot_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
⟨h1.ne_top, hx⟩

Premises used: LT.lt.ne_top, And.intro
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
inr : ∀ (x : ℝ) (h1 : (↑x : EReal) < y) (hx : (↑x : EReal) ≠ ⊥), (↑x : EReal) + z < y + t
⊢ x + z < y + t

Tactic:
lift x to ℝ using ⟨h1.ne_top, hx⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
y z t : EReal
h2 : z < t
x : ℝ
h1 : (↑x : EReal) < y
hx : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal) + z < (↑x : EReal) + t

Tactic:
add_lt_add_left_coe h2 _

Premises used: EReal.add_lt_add_left_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
y z t : EReal
h2 : z < t
x : ℝ
h1 : (↑x : EReal) < y
hx : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal) + t ≤ y + t

Tactic:
gcongr
-- Module: Mathlib.Data.EReal.Operations
Goal:
y z t : EReal
h2 : z < t
x : ℝ
h1 : (↑x : EReal) < y
hx : (↑x : EReal) ≠ ⊥
calc : (↑x : EReal) + t ≤ y + t
⊢ (↑x : EReal) + z < y + t

Tactic:
calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr

Premises used: EReal.add_lt_add_left_coe, Real.toEReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
inl : ∀ (h' : z ≤ z) (hbot : z ≠ ⊥) (htop : z = ⊤ → z = ⊤ → x = ⊥), x + z < y + z
inr : ∀ (hlt : z < t), x + z < y + t
⊢ x + z < y + t

Tactic:
rcases h'.eq_or_lt with (rfl | hlt)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
inl :
  ∀ (h' : LE.le (α := EReal) ⊤ ⊤) (hbot : Ne (α := EReal) ⊤ ⊥)
    (htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → x = ⊥), x + ⊤ < y + ⊤
inl₁ : ∀ (hz : z ≠ ⊤), x + z < y + z
⊢ x + z < y + z

Tactic:
rcases eq_or_ne z ⊤ with (rfl | hz)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x < y
h' : LE.le (α := EReal) ⊤ ⊤
hbot : Ne (α := EReal) ⊤ ⊥
htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → x = ⊥
inl :
  ∀ (h : ⊥ < y) (htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊥ ⊥),
    HAdd.hAdd (α := EReal) ⊥ ⊤ < y + ⊤
⊢ x + ⊤ < y + ⊤

Tactic:
obtain rfl := htop rfl rfl

Premises used: rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
h' : LE.le (α := EReal) ⊤ ⊤
hbot : Ne (α := EReal) ⊤ ⊥
h : ⊥ < y
htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊥ ⊥
⊢ HAdd.hAdd (α := EReal) ⊥ ⊤ < y + ⊤

Tactic:
simpa
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ z ≠ ⊤ ∧ z ≠ ⊥

Tactic:
⟨hz, hbot⟩

Premises used: And.intro
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
inl :
  ∀ (z : ℝ) (h' : (↑z : EReal) ≤ (↑z : EReal)) (hbot : (↑z : EReal) ≠ ⊥)
    (htop : (↑z : EReal) = ⊤ → (↑z : EReal) = ⊤ → x = ⊥) (hz : (↑z : EReal) ≠ ⊤), x + (↑z : EReal) < y + (↑z : EReal)
⊢ x + z < y + z

Tactic:
lift z to ℝ using ⟨hz, hbot⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x < y
z : ℝ
h' : (↑z : EReal) ≤ (↑z : EReal)
hbot : (↑z : EReal) ≠ ⊥
htop : (↑z : EReal) = ⊤ → (↑z : EReal) = ⊤ → x = ⊥
hz : (↑z : EReal) ≠ ⊤
⊢ x + (↑z : EReal) < y + (↑z : EReal)

Tactic:
add_lt_add_right_coe h z

Premises used: EReal.add_lt_add_right_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x < y
z : ℝ
h' : (↑z : EReal) ≤ (↑z : EReal)
hbot : (↑z : EReal) ≠ ⊥
htop : (↑z : EReal) = ⊤ → (↑z : EReal) = ⊤ → x = ⊥
hz : (↑z : EReal) ≠ ⊤
⊢ x + (↑z : EReal) < y + (↑z : EReal)

Tactic:
exact add_lt_add_right_coe h z

Premises used: EReal.add_lt_add_right_coe
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
add_lt_add h hlt

Premises used: EReal.add_lt_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
exact add_lt_add h hlt

Premises used: EReal.add_lt_add
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ x + z < y + t

Tactic:
add_lt_add_of_lt_of_le' h h' (ne_bot_of_le_ne_bot hz h') fun ht' => (ht ht').elim

Premises used: EReal.add_lt_add_of_lt_of_le', ne_bot_of_le_ne_bot, False.elim
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x + y < ⊤

Tactic:
add_lt_add hx.lt_top hy.lt_top

Premises used: WithBot.some, WithTop.map₂, Ne.lt_top, EReal.add_lt_add, WithBot.map₂, Option.map₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x + y ≠ ⊤

Tactic:
lt_top_iff_ne_top.mp <| add_lt_top hx hy

Premises used: EReal.add_lt_top, lt_top_iff_ne_top, Iff.mp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
⟨?_, fun h ↦ add_ne_top h.1 h.2⟩

Premises used: EReal.add_ne_top, And.right, And.left, Iff.intro
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
refine : x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊥), ⊥ + y ≠ ⊤ → Ne (α := EReal) ⊥ ⊤ ∧ y ≠ ⊤
coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊥), (↑a : EReal) + y ≠ ⊤ → (↑a : EReal) ≠ ⊤ ∧ y ≠ ⊤
top : ∀ (hx : Ne (α := EReal) ⊤ ⊥), ⊤ + y ≠ ⊤ → Ne (α := EReal) ⊤ ⊤ ∧ y ≠ ⊤
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hx : Ne (α := EReal) ⊥ ⊥
⊢ ⊥ + y ≠ ⊤ → Ne (α := EReal) ⊥ ⊤ ∧ y ≠ ⊤

Tactic:
simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]

Premises used: EReal.top_add_of_ne_bot, not_true_eq_false, ne_eq, not_false_eq_true, IsEmpty.forall_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
a : ℝ
hx : (↑a : EReal) ≠ ⊥
⊢ ¬y = ⊥

Tactic:
simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]

Premises used: EReal.top_add_of_ne_bot, not_true_eq_false, ne_eq, not_false_eq_true, IsEmpty.forall_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
a : ℝ
hx : (↑a : EReal) ≠ ⊥
hy₁ : ¬y = ⊥
⊢ ¬(↑a : EReal) = ⊥

Tactic:
simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]

Premises used: EReal.top_add_of_ne_bot, not_true_eq_false, ne_eq, not_false_eq_true, IsEmpty.forall_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hx : Ne (α := EReal) ⊤ ⊥
⊢ ⊤ + y ≠ ⊤ → Ne (α := EReal) ⊤ ⊤ ∧ y ≠ ⊤

Tactic:
simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]

Premises used: EReal.top_add_of_ne_bot, not_true_eq_false, ne_eq, not_false_eq_true, IsEmpty.forall_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
hy : ¬y = ⊥
hx : ¬(↑a : EReal) = ⊥
coe : ∀ (hy : ¬Eq (α := EReal) ⊥ ⊥), ¬(↑a : EReal) + ⊥ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊥ ⊤
coe₁ :
  ∀ (a_1 : ℝ) (hy : ¬(↑a_1 : EReal) = ⊥), ¬(↑a : EReal) + (↑a_1 : EReal) = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬(↑a_1 : EReal) = ⊤
coe₂ : ∀ (hy : ¬Eq (α := EReal) ⊤ ⊥), ¬(↑a : EReal) + ⊤ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊤ ⊤
⊢ ¬(↑a : EReal) + y = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬y = ⊤

Tactic:
cases y
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : ¬(↑a : EReal) = ⊥
hy : ¬Eq (α := EReal) ⊥ ⊥
⊢ ¬(↑a : EReal) + ⊥ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊥ ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

Premises used: and_self, not_true_eq_false, ne_eq, EReal.add_top_of_ne_bot, EReal.coe_ne_top, implies_true, not_false_eq_true
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : ¬(↑a : EReal) = ⊥
a_1 : ℝ
hy : ¬(↑a_1 : EReal) = ⊥
⊢ ¬(↑a : EReal) + (↑a_1 : EReal) = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬(↑a_1 : EReal) = ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

Premises used: and_self, not_true_eq_false, ne_eq, EReal.add_top_of_ne_bot, EReal.coe_ne_top, implies_true, not_false_eq_true
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
hx : ¬(↑a : EReal) = ⊥
hy : ¬Eq (α := EReal) ⊤ ⊥
⊢ ¬(↑a : EReal) + ⊤ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊤ ⊤

Tactic:
simp_all only [not_false_eq_true, ne_eq, add_top_of_ne_bot, not_true_eq_false,
    coe_ne_top, and_self, implies_true]

Premises used: and_self, not_true_eq_false, ne_eq, EReal.add_top_of_ne_bot, EReal.coe_ne_top, implies_true, not_false_eq_true
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
top : ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
cases x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a : ℝ
⊢ (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤

Tactic:
simp [add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : x ≠ ⊥
hx' : x ≠ ⊤
⊢ x + y ≠ ⊤ ↔ y ≠ ⊤

Tactic:
add_comm x y ▸ add_ne_top_iff_ne_top_left hx hx'

Premises used: EReal.add_ne_top_iff_ne_top_left, Eq.rec, add_comm, Eq.symm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
top : ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
a : ℝ
⊢ (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤

Tactic:
simp [EReal.add_ne_top_iff_ne_top₂, hy, hy']

Premises used: EReal.add_ne_top_iff_ne_top₂
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ Eq (α := EReal) (-⊤) ⊥

Tactic:
rfl

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

Tactic:
rfl

Premises used: EReal.neg, rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
⊢ (↑(-x) : EReal) = -(↑x : EReal)

Tactic:
rfl

Premises used: WithBot.some, EReal.neg, rfl, Real.toEReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
⊢ (↑(x - y) : EReal) = (↑x : EReal) - (↑y : EReal)

Tactic:
rfl

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

Tactic:
map_zsmul' (⟨⟨(↑), coe_zero⟩, coe_add⟩ : ℝ →+ EReal) coe_neg _ _

Premises used: WithBot.some, EReal.coe_neg, AddMonoidHom.mk, EReal.coe_zero, map_zsmul', ZeroHom.mk, EReal.coe_add, Real.toEReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ toReal (-⊤) = -toReal ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ toReal (-⊥) = -toReal ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ -x = ⊤ ↔ x = ⊥

Tactic:
neg_injective.eq_iff' rfl

Premises used: neg_injective, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ -x = ⊥ ↔ x = ⊤

Tactic:
neg_injective.eq_iff' rfl

Premises used: neg_injective, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
⊢ -x = 0 ↔ x = 0

Tactic:
neg_injective.eq_iff' neg_zero

Premises used: neg_injective, Function.Injective.eq_iff', neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ StrictAnti (β := EReal) fun (x : EReal) ↦ -x

Tactic:
WithBot.strictAnti_iff.2 ⟨WithTop.strictAnti_iff.2
    ⟨coe_strictMono.comp_strictAnti fun _ _ => neg_lt_neg, fun _ => bot_lt_coe _⟩,
      WithTop.forall.2 ⟨bot_lt_top, fun _ => coe_lt_top _⟩⟩

Premises used: Iff.mpr, WithTop.forall, EReal.bot_lt_coe, EReal, WithBot.strictAnti_iff, neg_lt_neg, EReal.coe_strictMono, WithTop.strictAnti_iff, bot_lt_top, And.intro, StrictMono.comp_strictAnti, Neg.neg, EReal.coe_lt_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
⊢ -a ≤ -b ↔ b ≤ a

Tactic:
neg_strictAnti.le_iff_ge

Premises used: EReal.neg_strictAnti, StrictAnti.le_iff_ge
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
⊢ -a < -b ↔ b < a

Tactic:
neg_strictAnti.lt_iff_gt

Premises used: EReal.neg_strictAnti, StrictAnti.lt_iff_gt
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw : -b ≤ - -a ↔ -b ≤ a
rw₁ rw₂ : -b ≤ a ↔ -b ≤ a
⊢ -a ≤ b ↔ -b ≤ a

Tactic:
rw [← neg_le_neg_iff, neg_neg]

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

Tactic:
EReal.neg_le.mp h

Premises used: Iff.mp, EReal.neg_le
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw : - -b ≤ -a ↔ b ≤ -a
rw₁ rw₂ : b ≤ -a ↔ b ≤ -a
⊢ a ≤ -b ↔ b ≤ -a

Tactic:
rw [← neg_le_neg_iff, neg_neg]

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

Tactic:
EReal.le_neg.mp h

Premises used: EReal.le_neg, Iff.mp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw : -b < - -a ↔ -b < a
rw₁ rw₂ : -b < a ↔ -b < a
⊢ -a < b ↔ -b < a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

Premises used: neg_neg, EReal.neg_lt_neg_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : -a < b
⊢ -b < a

Tactic:
neg_lt_comm.mp h

Premises used: EReal.neg_lt_comm, Iff.mp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw : - -b < -a ↔ b < -a
rw₁ rw₂ : b < -a ↔ b < -a
⊢ a < -b ↔ b < -a

Tactic:
rw [← neg_lt_neg_iff, neg_neg]

Premises used: neg_neg, EReal.neg_lt_neg_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
rw : -0 < a ↔ 0 < a
rw₁ rw₂ : 0 < a ↔ 0 < a
⊢ -a < 0 ↔ 0 < a

Tactic:
rw [neg_lt_comm, neg_zero]

Premises used: EReal.neg_lt_comm, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
rw : -0 ≤ a ↔ 0 ≤ a
rw₁ rw₂ : 0 ≤ a ↔ 0 ≤ a
⊢ -a ≤ 0 ↔ 0 ≤ a

Tactic:
rw [EReal.neg_le, neg_zero]

Premises used: EReal.neg_le, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
rw : a < -0 ↔ a < 0
rw₁ rw₂ : a < 0 ↔ a < 0
⊢ 0 < -a ↔ a < 0

Tactic:
rw [lt_neg_comm, neg_zero]

Premises used: EReal.lt_neg_comm, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : EReal
rw : a ≤ -0 ↔ a ≤ 0
rw₁ rw₂ : a ≤ 0 ↔ a ≤ 0
⊢ 0 ≤ -a ↔ a ≤ 0

Tactic:
rw [EReal.le_neg, neg_zero]

Premises used: EReal.le_neg, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a < -b
⊢ b < -a

Tactic:
lt_neg_comm.mp h

Premises used: Iff.mp, EReal.lt_neg_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊥), -(⊥ + y) = -⊥ - y
coe : ∀ (a : ℝ) (h1 : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊥), -((↑a : EReal) + y) = -(↑a : EReal) - y
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊥), -(⊤ + y) = -⊤ - y
⊢ -(x + y) = -x - y

Tactic:
induction x
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
h1 : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊥
bot :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
    -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₁ :
  ∀ (a : ℝ) (h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥),
    -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
bot₂ :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
    -HAdd.hAdd (α := EReal) ⊥ ⊤ = HSub.hSub (α := EReal) (-⊥) ⊤
⊢ -(⊥ + y) = -⊥ - y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊥
coe :
  ∀ (h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
    -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
coe₁ :
  ∀ (a_1 : ℝ) (h1 : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊥),
    -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
coe₂ :
  ∀ (h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
    -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
⊢ -((↑a : EReal) + y) = -(↑a : EReal) - y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
y : EReal
h1 : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
    -HAdd.hAdd (α := EReal) ⊤ ⊥ = HSub.hSub (α := EReal) (-⊤) ⊥
top₁ :
  ∀ (a : ℝ) (h1 : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊥),
    -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₂ :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
    -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -(⊤ + y) = -⊤ - y

Tactic:
induction y
-- Module: Mathlib.Data.EReal.Operations
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
bot :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₁ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₂ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₃ :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₄ bot₅ bot₆ bot₇ bot₈ bot₉ :
  ∀ (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) ⊥ ⊥
bot :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₁ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₂ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₃ :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
bot₄ bot₅ bot₆ bot₇ bot₈ bot₉ :
  ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥

Tactic:
try tauto