awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥
⊢ (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal
have top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).toENNReal ≤ toENNReal ⊤ + (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
top : (HAdd.hAdd (α := EReal) ⊤ ⊥).toENNReal ≤ toENNReal ⊤ + toENNReal ⊥
top₁ : ∀ (a : ℝ), (⊤ + (↑a : EReal)).toENNReal ≤ toENNReal ⊤ + (↑a : EReal).toENNReal
⊢ (⊤ + y).toENNReal ≤ toENNReal ⊤ + y.toENNReal
have top₂ : (HAdd.hAdd (α := EReal) ⊤ ⊤).toENNReal ≤ toENNReal ⊤ + toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
⊢ x + z < y + t
have inl : ∀ (h1 : ⊥ < y), ⊥ + z < y + t
Tactic: rcases eq_or_ne x ⊥ with (rfl | hx)
Cleared hypotheses: x, h1
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
inl : ∀ (h1 : ⊥ < y), ⊥ + z < y + t
⊢ x + z < y + t
have inr : ∀ (hx : x ≠ ⊥), x + z < y + t
Tactic: rcases eq_or_ne x ⊥ with (rfl | hx)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t
have inr : ∀ (x : ℝ) (h1 : (↑x : EReal) < y) (hx : (↑x : EReal) ≠ ⊥), (↑x : EReal) + z < y + t
Tactic: lift x to ℝ using ⟨h1.ne_top, hx⟩
Cleared hypotheses: x, h1, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y z t : EReal
h2 : z < t
x : ℝ
h1 : (↑x : EReal) < y
hx : (↑x : EReal) ≠ ⊥
⊢ (↑x : EReal) + z < y + t
have calc : (↑x : EReal) + t ≤ y + t
Tactic: calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t
have inl : ∀ (h' : z ≤ z) (hbot : z ≠ ⊥) (htop : z = ⊤ → z = ⊤ → x = ⊥), x + z < y + z
Tactic: rcases h'.eq_or_lt with (rfl | hlt)
Cleared hypotheses: t, h', hbot, htop
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ x + z < y + t
have inr : ∀ (hlt : z < t), x + z < y + t
Tactic: rcases h'.eq_or_lt with (rfl | hlt)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z
have inl : ∀ (h' : LE.le (α := EReal) ⊤ ⊤) (hbot : Ne (α := EReal) ⊤ ⊥) (htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → x = ⊥),
  x + ⊤ < y + ⊤
Tactic: rcases eq_or_ne z ⊤ with (rfl | hz)
Cleared hypotheses: z, h', hbot, htop
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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 + ⊤
⊢ x + z < y + z
have inl₁ : ∀ (hz : z ≠ ⊤), x + z < y + z
Tactic: rcases eq_or_ne z ⊤ with (rfl | hz)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : x < y
h' : LE.le (α := EReal) ⊤ ⊤
hbot : Ne (α := EReal) ⊤ ⊥
htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤
have inl : ∀ (h : ⊥ < y) (htop : Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊤ ⊤ → Eq (α := EReal) ⊥ ⊥),
  HAdd.hAdd (α := EReal) ⊥ ⊤ < y + ⊤
Tactic: obtain rfl := htop rfl rfl
Cleared hypotheses: x, h, htop
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
have 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)
Tactic: lift z to ℝ using ⟨hz, hbot⟩
Cleared hypotheses: z, h', hbot, htop, hz
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤
have refine : x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤
Tactic: refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤
have bot : ∀ (hx : Ne (α := EReal) ⊥ ⊥), ⊥ + y ≠ ⊤ → Ne (α := EReal) ⊥ ⊤ ∧ y ≠ ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
bot : ∀ (hx : Ne (α := EReal) ⊥ ⊥), ⊥ + y ≠ ⊤ → Ne (α := EReal) ⊥ ⊤ ∧ y ≠ ⊤
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤
have coe : ∀ (a : ℝ) (hx : (↑a : EReal) ≠ ⊥), (↑a : EReal) + y ≠ ⊤ → (↑a : EReal) ≠ ⊤ ∧ y ≠ ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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 ≠ ⊤
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤
have top : ∀ (hx : Ne (α := EReal) ⊤ ⊥), ⊤ + y ≠ ⊤ → Ne (α := EReal) ⊤ ⊤ ∧ y ≠ ⊤
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
y : EReal
hy : y ≠ ⊥
a : ℝ
hx : (↑a : EReal) ≠ ⊥
⊢ (↑a : EReal) + y ≠ ⊤ → (↑a : EReal) ≠ ⊤ ∧ y ≠ ⊤
have hy₁ : ¬y = ⊥
Tactic: simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]
Cleared hypotheses: hy, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
Goal:
y : EReal
hy : y ≠ ⊥
a : ℝ
hx : (↑a : EReal) ≠ ⊥
hy₁ : ¬y = ⊥
⊢ (↑a : EReal) + y ≠ ⊤ → (↑a : EReal) ≠ ⊤ ∧ y ≠ ⊤
have hx₁ : ¬(↑a : EReal) = ⊥
Tactic: simp_all only [ne_eq, not_false_eq_true, top_add_of_ne_bot, not_true_eq_false,
    IsEmpty.forall_iff]
Cleared hypotheses: hy, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
hy : ¬y = ⊥
hx : ¬(↑a : EReal) = ⊥
⊢ ¬(↑a : EReal) + y = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬y = ⊤
have coe : ∀ (hy : ¬Eq (α := EReal) ⊥ ⊥), ¬(↑a : EReal) + ⊥ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊥ ⊤
Tactic: cases y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
hy : ¬y = ⊥
hx : ¬(↑a : EReal) = ⊥
coe : ∀ (hy : ¬Eq (α := EReal) ⊥ ⊥), ¬(↑a : EReal) + ⊥ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊥ ⊤
⊢ ¬(↑a : EReal) + y = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬y = ⊤
have coe₁ : ∀ (a_1 : ℝ) (hy : ¬(↑a_1 : EReal) = ⊥), ¬(↑a : EReal) + (↑a_1 : EReal) = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬(↑a_1 : EReal) = ⊤
Tactic: cases y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) = ⊤
⊢ ¬(↑a : EReal) + y = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬y = ⊤
have coe₂ : ∀ (hy : ¬Eq (α := EReal) ⊤ ⊥), ¬(↑a : EReal) + ⊤ = ⊤ → ¬(↑a : EReal) = ⊤ ∧ ¬Eq (α := EReal) ⊤ ⊤
Tactic: cases y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have top : ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
bot : ⊥ + y ≠ ⊤ ↔ Ne (α := EReal) ⊥ ⊤
coe : ∀ (a : ℝ), (↑a : EReal) + y ≠ ⊤ ↔ (↑a : EReal) ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤
have top : ⊤ + y ≠ ⊤ ↔ Ne (α := EReal) ⊤ ⊤
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ -a ≤ b ↔ -b ≤ a
have rw : -b ≤ - -a ↔ -b ≤ a
Tactic: rw [← neg_le_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : -b ≤ - -a ↔ -b ≤ a
⊢ -a ≤ b ↔ -b ≤ a
have rw₁ : -b ≤ a ↔ -b ≤ a
Tactic: rw [← neg_le_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a ≤ -b ↔ b ≤ -a
have rw : - -b ≤ -a ↔ b ≤ -a
Tactic: rw [← neg_le_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : - -b ≤ -a ↔ b ≤ -a
⊢ a ≤ -b ↔ b ≤ -a
have rw₁ : b ≤ -a ↔ b ≤ -a
Tactic: rw [← neg_le_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ -a < b ↔ -b < a
have rw : -b < - -a ↔ -b < a
Tactic: rw [← neg_lt_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : -b < - -a ↔ -b < a
⊢ -a < b ↔ -b < a
have rw₁ : -b < a ↔ -b < a
Tactic: rw [← neg_lt_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a < -b ↔ b < -a
have rw : - -b < -a ↔ b < -a
Tactic: rw [← neg_lt_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : - -b < -a ↔ b < -a
⊢ a < -b ↔ b < -a
have rw₁ : b < -a ↔ b < -a
Tactic: rw [← neg_lt_neg_iff, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
⊢ -a < 0 ↔ 0 < a
have rw : -0 < a ↔ 0 < a
Tactic: rw [neg_lt_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
rw : -0 < a ↔ 0 < a
⊢ -a < 0 ↔ 0 < a
have rw₁ : 0 < a ↔ 0 < a
Tactic: rw [neg_lt_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
⊢ -a ≤ 0 ↔ 0 ≤ a
have rw : -0 ≤ a ↔ 0 ≤ a
Tactic: rw [EReal.neg_le, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
rw : -0 ≤ a ↔ 0 ≤ a
⊢ -a ≤ 0 ↔ 0 ≤ a
have rw₁ : 0 ≤ a ↔ 0 ≤ a
Tactic: rw [EReal.neg_le, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
⊢ 0 < -a ↔ a < 0
have rw : a < -0 ↔ a < 0
Tactic: rw [lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
rw : a < -0 ↔ a < 0
⊢ 0 < -a ↔ a < 0
have rw₁ : a < 0 ↔ a < 0
Tactic: rw [lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
⊢ 0 ≤ -a ↔ a ≤ 0
have rw : a ≤ -0 ↔ a ≤ 0
Tactic: rw [EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : EReal
rw : a ≤ -0 ↔ a ≤ 0
⊢ 0 ≤ -a ↔ a ≤ 0
have rw₁ : a ≤ 0 ↔ a ≤ 0
Tactic: rw [EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
⊢ -(x + y) = -x - y
have bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊥), -(⊥ + y) = -⊥ - y
Tactic: induction x
Cleared hypotheses: x, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊥), -(⊥ + y) = -⊥ - y
⊢ -(x + y) = -x - y
have coe : ∀ (a : ℝ) (h1 : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊥), -((↑a : EReal) + y) = -(↑a : EReal) - y
Tactic: induction x
Cleared hypotheses: x, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ -(x + y) = -x - y
have top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊥), -(⊤ + y) = -⊤ - y
Tactic: induction x
Cleared hypotheses: x, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h1 : Ne (α := EReal) ⊥ ⊥ ∨ y ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ y ≠ ⊥
⊢ -(⊥ + y) = -⊥ - y
have bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
  -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊥) ⊥
⊢ -(⊥ + y) = -⊥ - y
have bot₁ : ∀ (a : ℝ) (h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥),
  -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -(⊥ + y) = -⊥ - y
have bot₂ : ∀ (h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
  -HAdd.hAdd (α := EReal) ⊥ ⊤ = HSub.hSub (α := EReal) (-⊥) ⊤
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ y ≠ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ y ≠ ⊥
⊢ -((↑a : EReal) + y) = -(↑a : EReal) - y
have coe : ∀ (h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
  -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) - ⊥
⊢ -((↑a : EReal) + y) = -(↑a : EReal) - y
have 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)
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -((↑a : EReal) + y) = -(↑a : EReal) - y
have coe₂ : ∀ (h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
  -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
h1 : Ne (α := EReal) ⊤ ⊥ ∨ y ≠ ⊤
h2 : Ne (α := EReal) ⊤ ⊤ ∨ y ≠ ⊥
⊢ -(⊤ + y) = -⊤ - y
have top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊥ ⊥),
  -HAdd.hAdd (α := EReal) ⊤ ⊥ = HSub.hSub (α := EReal) (-⊤) ⊥
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊤) ⊥
⊢ -(⊤ + y) = -⊤ - y
have top₁ : ∀ (a : ℝ) (h1 : Ne (α := EReal) ⊤ ⊥ ∨ (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ (↑a : EReal) ≠ ⊥),
  -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -(⊤ + y) = -⊤ - y
have top₂ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥ ∨ Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤ ∨ Ne (α := EReal) ⊤ ⊥),
  -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
Tactic: induction y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
bot :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₁ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₂ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
h1 : Ne (α := EReal) ⊥ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
bot :
  ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₁ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₂ : ∀ (h1 h2 : Ne (α := EReal) ⊥ ⊤), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) (-⊥) ⊥
⊢ -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
have bot₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -HAdd.hAdd (α := EReal) ⊥ ⊥ = HSub.hSub (α := EReal) (-⊥) ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
have bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : Ne (α := EReal) ⊥ ⊥ ∨ (↑a : EReal) ≠ ⊤
h2 : Ne (α := EReal) ⊥ ⊤ ∨ (↑a : EReal) ≠ ⊥
bot : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
have bot₁ : ∀ (h1 : Ne (α := EReal) ⊥ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
have bot₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊥ ⊤), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
Tactic: tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
have bot₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊥ + (↑a : EReal)) = -⊥ - (↑a : EReal)
Tactic: tauto
Cleared hypotheses: h1, h2