awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
⊢ (x * y).toReal = x.toReal * y.toReal
have top_zero : (HMul.hMul (α := EReal) ⊤ 0).toReal = toReal ⊤ * toReal 0
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
⊢ (x * y).toReal = x.toReal * y.toReal
have zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
⊢ (x * y).toReal = x.toReal * y.toReal
have top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
⊢ (x * y).toReal = x.toReal * y.toReal
have top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
⊢ (x * y).toReal = x.toReal * y.toReal
have bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
⊢ (x * y).toReal = x.toReal * y.toReal
have symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
⊢ (x * y).toReal = x.toReal * y.toReal
have coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
⊢ (x * y).toReal = x.toReal * y.toReal
have top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
⊢ (x * y).toReal = x.toReal * y.toReal
have top_neg : ∀ (x : ℝ) (h : x < 0), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
top_neg : ∀ (x : ℝ) (h : x < 0), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
⊢ (x * y).toReal = x.toReal * y.toReal
have pos_bot : ∀ (x : ℝ) (h : 0 < x), ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg 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).toReal = toReal ⊤ * toReal 0
zero_bot : (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥
top_top : (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤
top_bot : (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥
bot_bot : (HMul.hMul (α := EReal) ⊥ ⊥).toReal = toReal ⊥ * toReal ⊥
symm : ∀ {x y : EReal} (h : (x * y).toReal = x.toReal * y.toReal), (y * x).toReal = y.toReal * x.toReal
coe_coe : ∀ (x y : ℝ), ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
top_pos : ∀ (x : ℝ) (h : 0 < x), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
top_neg : ∀ (x : ℝ) (h : x < 0), (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal
pos_bot : ∀ (x : ℝ) (h : 0 < x), ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥
⊢ (x * y).toReal = x.toReal * y.toReal
have neg_bot : ∀ (x : ℝ) (h : x < 0), ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥
Tactic: induction x, y using induction₂_symm with
  | top_zero | zero_bot | top_top | top_bot | bot_bot => simp
  | symm h => rwa [mul_comm, EReal.mul_comm]
  | coe_coe => norm_cast
  | top_pos _ h => simp [top_mul_coe_of_pos h]
  | top_neg _ h => simp [top_mul_coe_of_neg h]
  | pos_bot _ h => simp [coe_mul_bot_of_pos h]
  | neg_bot _ h => simp [coe_mul_bot_of_neg h]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a * b = 0
⊢ a = 0 ∨ b = 0
have contrapose! : ∀ (h : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0
have bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0), ⊥ * b ≠ 0
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a ≠ 0 ∧ b ≠ 0
bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0), ⊥ * b ≠ 0
⊢ a * b ≠ 0
have coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ 0 ∧ b ≠ 0), (↑a : EReal) * b ≠ 0
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
h : a ≠ 0 ∧ b ≠ 0
bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0), ⊥ * b ≠ 0
coe : ∀ (a : ℝ) (h : (↑a : EReal) ≠ 0 ∧ b ≠ 0), (↑a : EReal) * b ≠ 0
⊢ a * b ≠ 0
have top : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ b ≠ 0), ⊤ * b ≠ 0
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0
⊢ ⊥ * b ≠ 0
have bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0
bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0
⊢ ⊥ * b ≠ 0
have bot₁ : ∀ (a : ℝ) (h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0), ⊥ * (↑a : EReal) ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊥ 0 ∧ b ≠ 0
bot : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0
bot₁ : ∀ (a : ℝ) (h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0), ⊥ * (↑a : EReal) ≠ 0
⊢ ⊥ * b ≠ 0
have bot₂ : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊤ 0), HMul.hMul (α := EReal) ⊥ ⊤ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ b ≠ 0
⊢ (↑a : EReal) * b ≠ 0
have coe : ∀ (h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0), (↑a : EReal) * ⊥ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ b ≠ 0
coe : ∀ (h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0), (↑a : EReal) * ⊥ ≠ 0
⊢ (↑a : EReal) * b ≠ 0
have coe₁ : ∀ (a_1 : ℝ) (h : (↑a : EReal) ≠ 0 ∧ (↑a_1 : EReal) ≠ 0), (↑a : EReal) * (↑a_1 : EReal) ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ b ≠ 0
coe : ∀ (h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0), (↑a : EReal) * ⊥ ≠ 0
coe₁ : ∀ (a_1 : ℝ) (h : (↑a : EReal) ≠ 0 ∧ (↑a_1 : EReal) ≠ 0), (↑a : EReal) * (↑a_1 : EReal) ≠ 0
⊢ (↑a : EReal) * b ≠ 0
have coe₂ : ∀ (h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0), (↑a : EReal) * ⊤ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊤ 0 ∧ b ≠ 0
⊢ ⊤ * b ≠ 0
have top : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊤ 0 ∧ b ≠ 0
top : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0
⊢ ⊤ * b ≠ 0
have top₁ : ∀ (a : ℝ) (h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0), ⊤ * (↑a : EReal) ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
b : EReal
h : Ne (α := EReal) ⊤ 0 ∧ b ≠ 0
top : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0), HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0
top₁ : ∀ (a : ℝ) (h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0), ⊤ * (↑a : EReal) ≠ 0
⊢ ⊤ * b ≠ 0
have top₂ : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊤ 0), HMul.hMul (α := EReal) ⊤ ⊤ ≠ 0
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
⊢ ⊥ * (↑a : EReal) ≠ 0
have bot : ∀ (h : (↑a : EReal) < 0), ⊥ * (↑a : EReal) ≠ 0
Tactic: rcases lt_or_gt_of_ne h.2 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
bot : ∀ (h : (↑a : EReal) < 0), ⊥ * (↑a : EReal) ≠ 0
⊢ ⊥ * (↑a : EReal) ≠ 0
have bot₁ : ∀ (h : 0 < (↑a : EReal)), ⊥ * (↑a : EReal) ≠ 0
Tactic: rcases lt_or_gt_of_ne h.2 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ (↑a : EReal) * ⊥ ≠ 0
have coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊥ ≠ 0
Tactic: rcases lt_or_gt_of_ne h.1 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊥ ≠ 0
⊢ (↑a : EReal) * ⊥ ≠ 0
have coe₁ : ∀ (h : 0 < (↑a : EReal)), (↑a : EReal) * ⊥ ≠ 0
Tactic: rcases lt_or_gt_of_ne h.1 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ (↑a : EReal) * ⊤ ≠ 0
have coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊤ ≠ 0
Tactic: rcases lt_or_gt_of_ne h.1 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊤ ≠ 0
⊢ (↑a : EReal) * ⊤ ≠ 0
have coe₁ : ∀ (h : 0 < (↑a : EReal)), (↑a : EReal) * ⊤ ≠ 0
Tactic: rcases lt_or_gt_of_ne h.1 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
⊢ ⊤ * (↑a : EReal) ≠ 0
have top : ∀ (h : (↑a : EReal) < 0), ⊤ * (↑a : EReal) ≠ 0
Tactic: rcases lt_or_gt_of_ne h.2 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a : ℝ
h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
top : ∀ (h : (↑a : EReal) < 0), ⊤ * (↑a : EReal) ≠ 0
⊢ ⊤ * (↑a : EReal) ≠ 0
have top₁ : ∀ (h : 0 < (↑a : EReal)), ⊤ * (↑a : EReal) ≠ 0
Tactic: rcases lt_or_gt_of_ne h.2 with (h | h)
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have top_top : 0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
  LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have top_pos : ∀ (x : ℝ) (hx : 0 < x),
  0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have top_zero : 0 < HMul.hMul (α := EReal) ⊤ 0 ↔
  LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have top_neg : ∀ (x : ℝ) (hx : x < 0),
  0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
symm : ∀ {x y : EReal} (h : 0 < x * y ↔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0), 0 < y * x ↔ 0 < y ∧ 0 < x ∨ y < 0 ∧ x < 0
top_top :
  0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0
top_pos :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
top_zero :
  0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0
top_neg :
  ∀ (x : ℝ) (hx : x < 0),
    0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
have top_bot : 0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
  LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
Tactic: induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp
Cleared hypotheses: a, b