awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
h : -x * y = -(x * y)
neg_left : - -x * y = - -(x * y)
neg_left₁ : x * y = - -(x * y)
⊢ - -x * y = -(-x * y)
have neg_left₂ : x * y = x * y
Tactic: rw [h, neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : ℝ
⊢ -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
have coe_coe : -x * y = -(x * y)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_pos : -⊤ * (↑x : EReal) = -⊤
Tactic: rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
top_pos : -⊤ * (↑x : EReal) = -⊤
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_pos₁ : ⊥ * (↑x : EReal) = ⊥
Tactic: rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
top_pos : -⊤ * (↑x : EReal) = -⊤
top_pos₁ : ⊥ * (↑x : EReal) = ⊥
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_pos₂ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
⊢ -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
have pos_top : -(↑x : EReal) * ⊤ = -⊤
Tactic: rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_top : -(↑x : EReal) * ⊤ = -⊤
⊢ -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
have pos_top₁ : -(↑x : EReal) * ⊤ = ⊥
Tactic: rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_top : -(↑x : EReal) * ⊤ = -⊤
pos_top₁ : -(↑x : EReal) * ⊤ = ⊥
⊢ -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
have pos_top₂ : (↑(-x) : EReal) * ⊤ = ⊥
Tactic: rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_top : -(↑x : EReal) * ⊤ = -⊤
pos_top₁ : -(↑x : EReal) * ⊤ = ⊥
pos_top₂ : (↑(-x) : EReal) * ⊤ = ⊥
⊢ -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
have pos_top₃ : Eq (α := EReal) ⊥ ⊥
Tactic: rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : x < 0
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_neg : -⊤ * (↑x : EReal) = -⊥
Tactic: rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : x < 0
top_neg : -⊤ * (↑x : EReal) = -⊥
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_neg₁ : ⊥ * (↑x : EReal) = -⊥
Tactic: rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : x < 0
top_neg : -⊤ * (↑x : EReal) = -⊥
top_neg₁ : ⊥ * (↑x : EReal) = -⊥
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_neg₂ : Eq (α := EReal) ⊤ (-⊥)
Tactic: rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : x < 0
top_neg : -⊤ * (↑x : EReal) = -⊥
top_neg₁ : ⊥ * (↑x : EReal) = -⊥
top_neg₂ : Eq (α := EReal) ⊤ (-⊥)
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
have top_neg₃ : Eq (α := EReal) ⊤ ⊤
Tactic: rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
⊢ -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)
have pos_bot : -(↑x : EReal) * ⊥ = -⊥
Tactic: rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_bot : -(↑x : EReal) * ⊥ = -⊥
⊢ -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)
have pos_bot₁ : -(↑x : EReal) * ⊥ = ⊤
Tactic: rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_bot : -(↑x : EReal) * ⊥ = -⊥
pos_bot₁ : -(↑x : EReal) * ⊥ = ⊤
⊢ -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)
have pos_bot₂ : (↑(-x) : EReal) * ⊥ = ⊤
Tactic: rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x : ℝ
h : 0 < x
pos_bot : -(↑x : EReal) * ⊥ = -⊥
pos_bot₁ : -(↑x : EReal) * ⊥ = ⊤
pos_bot₂ : (↑(-x) : EReal) * ⊥ = ⊤
⊢ -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)
have pos_bot₃ : Eq (α := EReal) ⊤ ⊤
Tactic: rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ -x * y = -(x * y)
have top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
⊢ -x * y = -(x * y)
have zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
⊢ -x * y = -(x * y)
have zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
⊢ -x * y = -(x * y)
have top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
⊢ -x * y = -(x * y)
have top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
⊢ -x * y = -(x * y)
have neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
⊢ -x * y = -(x * y)
have coe_coe : ∀ (x y : ℝ), -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
coe_coe : ∀ (x y : ℝ), -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
⊢ -x * y = -(x * y)
have top_pos : ∀ (x : ℝ) (h : 0 < x), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
coe_coe : ∀ (x y : ℝ), -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
top_pos : ∀ (x : ℝ) (h : 0 < x), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
⊢ -x * y = -(x * y)
have pos_top : ∀ (x : ℝ) (h : 0 < x), -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
coe_coe : ∀ (x y : ℝ), -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
top_pos : ∀ (x : ℝ) (h : 0 < x), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
pos_top : ∀ (x : ℝ) (h : 0 < x), -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
⊢ -x * y = -(x * y)
have top_neg : ∀ (x : ℝ) (h : x < 0), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
top_zero : HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0
zero_top : HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤
zero_bot : HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥
top_top : HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤
top_bot : HMul.hMul (α := EReal) (-⊤) ⊥ = -HMul.hMul (α := EReal) ⊤ ⊥
neg_left : ∀ {x y : EReal} (h : -x * y = -(x * y)), - -x * y = -(-x * y)
coe_coe : ∀ (x y : ℝ), -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))
top_pos : ∀ (x : ℝ) (h : 0 < x), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
pos_top : ∀ (x : ℝ) (h : 0 < x), -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)
top_neg : ∀ (x : ℝ) (h : x < 0), -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))
⊢ -x * y = -(x * y)
have pos_bot : ∀ (x : ℝ) (h : 0 < x), -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)
Tactic: induction x, y using induction₂_neg_left with
  | top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
  | top_top | top_bot => rfl
  | neg_left h => rw [h, neg_neg, neg_neg]
  | coe_coe => norm_cast; exact neg_mul _ _
  | top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
  | pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]
  | top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
  | pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ x * -y = -(x * y)
have rw : -y * x = -(y * x)
Tactic: rw [x.mul_comm, x.mul_comm]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have nth_rw : a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: nth_rw 1 [← neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₃ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₃ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₄ : 0 < a ∧ b < -0 ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 < -(a * b) ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₁ : 0 < a * -b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₂ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₃ : 0 < a ∧ 0 < -b ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
rw₄ : 0 < a ∧ b < -0 ∨ a < 0 ∧ -0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
have rw₅ : 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Tactic: rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have nth_rw : a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: nth_rw 1 [← neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₃ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₄ : 0 ≤ a ∧ b ≤ -0 ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
rw : 0 ≤ -(a * b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₁ : 0 ≤ a * -b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₂ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₃ : 0 ≤ a ∧ 0 ≤ -b ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
rw₄ : 0 ≤ a ∧ b ≤ -0 ∨ a ≤ 0 ∧ -0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
have rw₅ : 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Tactic: rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]