awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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) ≠ ⊥
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: 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) ≠ ⊥
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: 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) ≠ ⊥
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: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe : ∀ (h1 : (↑a : 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 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₁ : ∀ (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 : (↑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) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₂ : ∀ (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 : (↑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) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₃ : ∀ (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 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊥ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊥ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₂ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) - ⊥
⊢ -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
have coe₃ : ∀ (h1 : Ne (α := EReal) ⊥ ⊤) (h2 : Ne (α := EReal) ⊥ ⊥), -((↑a : EReal) + ⊥) = -(↑a : EReal) - ⊥
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe : ∀ (h1 : (↑a : 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 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₁ : ∀ (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 : (↑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) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₂ : ∀ (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 : (↑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) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₃ : ∀ (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 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ Ne (α := EReal) ⊤ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ Ne (α := EReal) ⊤ ⊥
coe : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₁ : ∀ (h1 : (↑a : EReal) ≠ ⊥) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₂ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : (↑a : EReal) ≠ ⊤), -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
Tactic: try tauto
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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) - ⊤
⊢ -((↑a : EReal) + ⊤) = -(↑a : EReal) - ⊤
have coe₃ : ∀ (h1 : Ne (α := EReal) ⊤ ⊤) (h2 : Ne (α := EReal) ⊤ ⊥), -((↑a : EReal) + ⊤) = -(↑a : 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 top : ∀ (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) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₁ : ∀ (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) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₂ : ∀ (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) ≠ ⊥
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)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₃ : ∀ (h1 : (↑a : 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) ≠ ⊥
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : 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) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₁ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : 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) ≠ ⊥
top : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
top₁ : ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₂ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : Ne (α := EReal) ⊤ ⊤), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : 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) ≠ ⊥
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)
⊢ -(⊤ + (↑a : EReal)) = -⊤ - (↑a : EReal)
have top₃ : ∀ (h1 : (↑a : EReal) ≠ ⊤) (h2 : (↑a : EReal) ≠ ⊥), -(⊤ + (↑a : EReal)) = -⊤ - (↑a : 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) ⊤ ⊥
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top : ∀ (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) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₁ : ∀ (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) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₁ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₂ : ∀ (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) ⊤ ⊥
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) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₃ : ∀ (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 top : ∀ (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) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₁ : ∀ (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) ⊤ ⊥
top :
  ∀ (h1 : Ne (α := EReal) ⊤ ⊥) (h2 : Ne (α := EReal) ⊤ ⊤), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
top₁ : ∀ (h1 h2 : Ne (α := EReal) ⊤ ⊥), -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₂ : ∀ (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) ⊤ ⊥
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) (-⊤) ⊤
⊢ -HAdd.hAdd (α := EReal) ⊤ ⊤ = HSub.hSub (α := EReal) (-⊤) ⊤
have top₃ : ∀ (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 a_1 : ℝ
h1 : (↑a : EReal) ≠ ⊥ ∨ (↑a_1 : EReal) ≠ ⊤
h2 : (↑a : EReal) ≠ ⊤ ∨ (↑a_1 : EReal) ≠ ⊥
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
have coe : -(↑(a + a_1) : EReal) = -(↑a : EReal) - (↑a_1 : EReal)
Tactic: rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
have coe₁ : (↑(-(a + a_1)) : EReal) = -(↑a : EReal) - (↑a_1 : EReal)
Tactic: rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
have coe₂ : (↑(-(a + a_1)) : EReal) = (↑(-a) : EReal) - (↑a_1 : EReal)
Tactic: rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
have coe₃ : (↑(-(a + a_1)) : EReal) = (↑(-a - a_1) : EReal)
Tactic: rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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)
⊢ -((↑a : EReal) + (↑a_1 : EReal)) = -(↑a : EReal) - (↑a_1 : EReal)
have coe₄ : (↑(-a - a_1) : EReal) = (↑(-a - a_1) : EReal)
Tactic: rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']
-- 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 rw : x ≠ ⊥ ∨ -y ≠ ⊤
Tactic: rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
rw : x ≠ ⊥ ∨ -y ≠ ⊤
⊢ -(x - y) = -x + y
have rw₁ : x ≠ ⊤ ∨ -y ≠ ⊥
Tactic: rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ x = -(↑(-x).toENNReal : EReal)
have rw : x = - -x
Tactic: rw [coe_toENNReal H₁.le, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ x = -(↑(-x).toENNReal : EReal)
have rw₁ : x = x
Tactic: rw [coe_toENNReal H₁.le, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive (↑x : EReal)
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-(↑x : EReal))
x : ℝ≥0∞
⊢ recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe (↑x : EReal) = coe x
have suffices : ∀ (y : EReal), (↑x : EReal) = y → recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y ≍ 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)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (hypothesis)
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
⊢ recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y ≍ coe x
have H₁ : 0 ≤ y
Tactic: have H₁ : 0 ≤ y := hy ▸ coe_ennreal_nonneg x
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ recENNReal (motive := fun (x : EReal) ↦ motive x) coe neg_coe y ≍ coe x
have 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)
Tactic: obtain rfl : y.toENNReal = x := by simp [← hy]
Cleared hypotheses: x, hy
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
⊢ x - ⊥ = ⊤
have bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = ⊤
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = ⊤
⊢ x - ⊥ = ⊤
have coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), (↑a : EReal) - ⊥ = ⊤
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : EReal
h : x ≠ ⊥
bot : ∀ (h : Ne (α := EReal) ⊥ ⊥), HSub.hSub (α := EReal) ⊥ ⊥ = ⊤
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ ⊥), (↑a : EReal) - ⊥ = ⊤
⊢ x - ⊥ = ⊤
have top : ∀ (h : Ne (α := EReal) ⊤ ⊥), HSub.hSub (α := EReal) ⊤ ⊥ = ⊤
Tactic: cases x
Cleared hypotheses: x, h