awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
⊢ x * ⊤ = ⊤

Tactic:
exact mul_top_of_pos h

Premises used: EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
rw : x * ⊤ = ⊥
⊢ ⊤ * x = ⊥

Tactic:
rw [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
⊢ x * ⊤ = ⊥

Tactic:
mul_top_of_neg h

Premises used: EReal.mul_top_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
⊢ x * ⊤ = ⊥

Tactic:
exact mul_top_of_neg h

Premises used: EReal.mul_top_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ≥0∞
hx : x ≠ 0
⊢ ⊤ * (↑x : EReal) = ⊤

Tactic:
top_mul_of_pos <| coe_ennreal_pos.mpr <| pos_iff_ne_zero.mpr hx

Premises used: Iff.mpr, EReal.top_mul_of_pos, pos_iff_ne_zero, EReal.coe_ennreal_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ≥0∞
hx : x ≠ 0
rw : ⊤ * (↑x : EReal) = ⊤
rw₁ rw₂ : Eq (α := EReal) ⊤ ⊤
⊢ (↑x : EReal) * ⊤ = ⊤

Tactic:
rw [EReal.mul_comm, top_mul_coe_ennreal hx]

Premises used: EReal.top_mul_coe_ennreal, EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ (↑x : EReal) * ⊥ = ⊥

Tactic:
if_pos h

Premises used: if_pos, EReal.mul, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ (↑x : EReal) * ⊥ = ⊤

Tactic:
(if_neg h.not_gt).trans (if_neg h.ne)

Premises used: EReal.mul, LT.lt.not_gt, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ ⊥ * (↑x : EReal) = ⊥

Tactic:
if_pos h

Premises used: if_pos, EReal.mul, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ ⊥ * (↑x : EReal) = ⊤

Tactic:
(if_neg h.not_gt).trans (if_neg h.ne)

Premises used: EReal.mul, LT.lt.not_gt, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
rw : x * ⊥ = ⊥
⊢ ⊥ * x = ⊥

Tactic:
rw [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥

Tactic:
mul_bot_of_pos h

Premises used: EReal.mul_bot_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥

Tactic:
exact mul_bot_of_pos h

Premises used: EReal.mul_bot_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
rw : x * ⊥ = ⊤
⊢ ⊥ * x = ⊤

Tactic:
rw [EReal.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
⊢ x * ⊥ = ⊤

Tactic:
mul_bot_of_neg h

Premises used: EReal.mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : EReal
h : x < 0
⊢ x * ⊥ = ⊤

Tactic:
exact mul_bot_of_neg h

Premises used: EReal.mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ 0).toReal = toReal ⊤ * toReal 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HMul.hMul (α := EReal) 0 ⊥).toReal = toReal 0 * toReal ⊥

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ ⊤).toReal = toReal ⊤ * toReal ⊤

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ (HMul.hMul (α := EReal) ⊤ ⊥).toReal = toReal ⊤ * toReal ⊥

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

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : (x * y).toReal = x.toReal * y.toReal
symm : (y * x).toReal = x.toReal * y.toReal
symm₁ symm₂ symm₃ symm₄ : (x * y).toReal = x.toReal * y.toReal
⊢ (y * x).toReal = y.toReal * x.toReal

Tactic:
rwa [mul_comm, EReal.mul_comm]

Premises used: EReal.mul_comm, mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
coe_coe coe_coe₁ coe_coe₂ coe_coe₃ : (↑(x * y) : EReal).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal
⊢ ((↑x : EReal) * (↑y : EReal)).toReal = (↑x : EReal).toReal * (↑y : EReal).toReal

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal

Tactic:
simp [top_mul_coe_of_pos h]

Premises used: EReal.top_mul_coe_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ (⊤ * (↑x : EReal)).toReal = toReal ⊤ * (↑x : EReal).toReal

Tactic:
simp [top_mul_coe_of_neg h]

Premises used: EReal.top_mul_coe_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
⊢ ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥

Tactic:
simp [coe_mul_bot_of_pos h]

Premises used: EReal.coe_mul_bot_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
⊢ ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥

Tactic:
simp [coe_mul_bot_of_neg h]

Premises used: EReal.coe_mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
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 ⊥
neg_bot : ∀ (x : ℝ) (h : x < 0), ((↑x : EReal) * ⊥).toReal = (↑x : EReal).toReal * toReal ⊥
⊢ (x * y).toReal = x.toReal * y.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]

Premises used: EReal.mul_comm, mul_comm, symm, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ (x * y).toReal = x.toReal * y.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]

Premises used: EReal.mul_comm, mul_comm, symm, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a * b = 0
contrapose! : ∀ (h : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! h
-- Module: Mathlib.Data.EReal.Operations
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
top : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ b ≠ 0), ⊤ * b ≠ 0
⊢ a * b ≠ 0

Tactic:
cases a
-- Module: Mathlib.Data.EReal.Operations
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
bot₂ : ∀ (h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊤ 0), HMul.hMul (α := EReal) ⊥ ⊤ ≠ 0
⊢ ⊥ * b ≠ 0

Tactic:
cases b
-- Module: Mathlib.Data.EReal.Operations
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
coe₂ : ∀ (h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0), (↑a : EReal) * ⊤ ≠ 0
⊢ (↑a : EReal) * b ≠ 0

Tactic:
cases b
-- Module: Mathlib.Data.EReal.Operations
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
top₂ : ∀ (h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊤ 0), HMul.hMul (α := EReal) ⊤ ⊤ ≠ 0
⊢ ⊤ * b ≠ 0

Tactic:
cases b
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊥ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
⊢ ⊥ * (↑a : EReal) ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊤ ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊤ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊥ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊥ ⊤ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ (↑a : EReal) * ⊥ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
h : (↑a : EReal) ≠ 0 ∧ (↑a_1 : EReal) ≠ 0
⊢ (↑a : EReal) * (↑a_1 : EReal) ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
h : (↑a : EReal) ≠ 0 ∧ (↑a_1 : EReal) ≠ 0
⊢ (↑a : EReal) * (↑a_1 : EReal) ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a a_1 : ℝ
h : (↑a : EReal) ≠ 0 ∧ (↑a_1 : EReal) ≠ 0
⊢ (↑a : EReal) * (↑a_1 : EReal) ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ (↑a : EReal) * ⊤ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊥ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊥ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
⊢ ⊤ * (↑a : EReal) ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊤ ≠ 0

Tactic:
simp_all [← EReal.coe_mul]

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊤ ≠ 0

Tactic:
{· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
h : Ne (α := EReal) ⊤ 0 ∧ Ne (α := EReal) ⊤ 0
⊢ HMul.hMul (α := EReal) ⊤ ⊤ ≠ 0

Tactic:
try {· simp_all [← EReal.coe_mul]}

Premises used: EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
bot : ∀ (h : (↑a : EReal) < 0), ⊥ * (↑a : EReal) ≠ 0
bot₁ : ∀ (h : 0 < (↑a : EReal)), ⊥ * (↑a : EReal) ≠ 0
⊢ ⊥ * (↑a : EReal) ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.2 with (h | h)

Premises used: lt_or_gt_of_ne, And.right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
h : (↑a : EReal) < 0
⊢ ⊥ * (↑a : EReal) ≠ 0

Tactic:
simp [EReal.bot_mul_of_neg, EReal.bot_mul_of_pos, h]

Premises used: EReal.bot_mul_of_pos, EReal.bot_mul_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : Ne (α := EReal) ⊥ 0 ∧ (↑a : EReal) ≠ 0
h : 0 < (↑a : EReal)
⊢ ⊥ * (↑a : EReal) ≠ 0

Tactic:
simp [EReal.bot_mul_of_neg, EReal.bot_mul_of_pos, h]

Premises used: EReal.bot_mul_of_pos, EReal.bot_mul_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊥ ≠ 0
coe₁ : ∀ (h : 0 < (↑a : EReal)), (↑a : EReal) * ⊥ ≠ 0
⊢ (↑a : EReal) * ⊥ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.1 with (h | h)

Premises used: lt_or_gt_of_ne, And.left
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
h : (↑a : EReal) < 0
⊢ (↑a : EReal) * ⊥ ≠ 0

Tactic:
simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]

Premises used: EReal.mul_bot_of_pos, EReal.mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊥ 0
h : 0 < (↑a : EReal)
⊢ (↑a : EReal) * ⊥ ≠ 0

Tactic:
simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]

Premises used: EReal.mul_bot_of_pos, EReal.mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
coe : ∀ (h : (↑a : EReal) < 0), (↑a : EReal) * ⊤ ≠ 0
coe₁ : ∀ (h : 0 < (↑a : EReal)), (↑a : EReal) * ⊤ ≠ 0
⊢ (↑a : EReal) * ⊤ ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.1 with (h | h)

Premises used: lt_or_gt_of_ne, And.left
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
h : (↑a : EReal) < 0
⊢ (↑a : EReal) * ⊤ ≠ 0

Tactic:
simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]

Premises used: EReal.mul_top_of_neg, EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : (↑a : EReal) ≠ 0 ∧ Ne (α := EReal) ⊤ 0
h : 0 < (↑a : EReal)
⊢ (↑a : EReal) * ⊤ ≠ 0

Tactic:
simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]

Premises used: EReal.mul_top_of_neg, EReal.mul_top_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
top : ∀ (h : (↑a : EReal) < 0), ⊤ * (↑a : EReal) ≠ 0
top₁ : ∀ (h : 0 < (↑a : EReal)), ⊤ * (↑a : EReal) ≠ 0
⊢ ⊤ * (↑a : EReal) ≠ 0

Tactic:
rcases lt_or_gt_of_ne h.2 with (h | h)

Premises used: lt_or_gt_of_ne, And.right
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
h : (↑a : EReal) < 0
⊢ ⊤ * (↑a : EReal) ≠ 0

Tactic:
simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

Premises used: EReal.top_mul_of_pos, EReal.top_mul_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a : ℝ
h_1 : Ne (α := EReal) ⊤ 0 ∧ (↑a : EReal) ≠ 0
h : 0 < (↑a : EReal)
⊢ ⊤ * (↑a : EReal) ≠ 0

Tactic:
simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]

Premises used: EReal.top_mul_of_pos, EReal.top_mul_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
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:
simp [EReal.mul_comm, h, and_comm]

Premises used: and_comm, EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HMul.hMul (α := EReal) ⊤ ⊤ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊤ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊤ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

Premises used: EReal.top_mul_coe_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HMul.hMul (α := EReal) ⊤ 0 ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 0 ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) 0 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx : x < 0
⊢ 0 < ⊤ * (↑x : EReal) ↔ LT.lt (α := EReal) 0 ⊤ ∧ 0 < (↑x : EReal) ∨ LT.lt (α := EReal) ⊤ 0 ∧ (↑x : EReal) < 0

Tactic:
simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]

Premises used: le_of_lt, EReal.top_mul_coe_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]

Premises used: le_of_lt, EReal.coe_mul_bot_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
⊢ 0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0

Tactic:
simp [← coe_mul, _root_.mul_pos_iff]

Premises used: mul_pos_iff, EReal.coe_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HMul.hMul (α := EReal) 0 ⊥ ↔
    LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) ⊥ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
hx : x < 0
⊢ 0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

Premises used: EReal.coe_mul_bot_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ 0 < HMul.hMul (α := EReal) ⊥ ⊥ ↔
    LT.lt (α := EReal) 0 ⊥ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊥ 0 ∧ LT.lt (α := EReal) ⊥ 0

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
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
top_bot :
  0 < HMul.hMul (α := EReal) ⊤ ⊥ ↔
    LT.lt (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) ⊤ 0 ∧ LT.lt (α := EReal) ⊥ 0
pos_bot :
  ∀ (x : ℝ) (hx : 0 < x),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
coe_coe :
  ∀ (x y : ℝ),
    0 < (↑x : EReal) * (↑y : EReal) ↔ 0 < (↑x : EReal) ∧ 0 < (↑y : EReal) ∨ (↑x : EReal) < 0 ∧ (↑y : EReal) < 0
zero_bot :
  0 < HMul.hMul (α := EReal) 0 ⊥ ↔
    LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ LT.lt (α := EReal) ⊥ 0
neg_bot :
  ∀ (x : ℝ) (hx : x < 0),
    0 < (↑x : EReal) * ⊥ ↔ 0 < (↑x : EReal) ∧ LT.lt (α := EReal) 0 ⊥ ∨ (↑x : EReal) < 0 ∧ LT.lt (α := EReal) ⊥ 0
bot_bot :
  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

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

Premises used: le_of_lt, and_comm, mul_pos_iff, EReal.mul_comm, EReal.coe_mul, symm, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
simp_rw :
  (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]

Premises used: zero_eq_mul, le_iff_lt_or_eq, EReal.mul_pos_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
inl :
  ∀ (h : a < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr :
  ∀ (h : a = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₁ :
  ∀ (h : 0 < a),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy a 0 with (h | h | h)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a < 0
inl :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inl₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inl₂ :
  ∀ (h' : 0 < b),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy b 0 with (h' | h' | h')

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a = 0
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₂ :
  ∀ (h' : 0 < b),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy b 0 with (h' | h' | h')

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : 0 < a
inr :
  ∀ (h' : b < 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₁ :
  ∀ (h' : b = 0),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
inr₂ :
  ∀ (h' : 0 < b),
    (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
      (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy b 0 with (h' | h' | h')

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a < 0
h' : b < 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

Premises used: and_true, true_or, or_true, true_and
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a < 0
h' : b = 0
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
simp only [h, h', true_or, true_and, or_true, and_true]

Premises used: and_true, true_or, or_true, true_and