awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : a < 0
h' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ 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:
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
-- 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' : 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)

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 : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ 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)

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 : 0 < a
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 : 0 < a
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)

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' : 0 < b
inl : (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁ : (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₃ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₄ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₅ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₆ : 0 < a → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₇ : b < 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₈ : a = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₉ : b = 0 → (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0
inl₁₀ : 0 < a → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₁ : b < 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₂ : a = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₃ : b = 0 → ¬(0 < a ∨ 0 = a) → b < 0 ∨ b = 0
inl₁₄ : 0 < a → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₁₅ : 0 = a → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₁₆ : b < 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₁₇ : b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₁₈ : 0 < a → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₁₉ : 0 = a → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂₀ : b < 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂₁ : b = 0 → (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0
inl₂₂ : 0 < a → ¬(0 < a ∨ b < 0) → a = 0 ∨ b = 0
inl₂₃ : 0 = a → ¬(0 < a ∨ b < 0) → a = 0 ∨ b = 0
inl₂₄ : b < 0 → ¬(0 < a ∨ b < 0) → a = 0 ∨ b = 0
inl₂₅ : b = 0 → ¬(0 < a ∨ b < 0) → a = 0 ∨ b = 0
inl₂₆ : 0 < a → ¬0 < a → ¬0 = a → b < 0 ∨ b = 0
inl₂₇ inl₂₈ : b < 0 → ¬0 < a → ¬0 = a → b < 0 ∨ b = 0
inl₂₉ : b < 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₃₀ inl₃₁ : a = 0 → ¬0 < a → ¬0 = a → b < 0 ∨ b = 0
inl₃₂ : a = 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₃₃ inl₃₄ : b = 0 → ¬0 < a → ¬0 = a → b < 0 ∨ b = 0
inl₃₅ : b = 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₃₆ : 0 < a → ¬0 < a → ¬b < 0 → a = 0 ∨ b = 0
inl₃₇ inl₃₈ : 0 = a → ¬0 < a → ¬b < 0 → a = 0 ∨ b = 0
inl₃₉ : 0 = a → ¬0 < a → ¬b < 0 → ¬a = 0 → b = 0
inl₄₀ : b < 0 → ¬0 < a → ¬b < 0 → a = 0 ∨ b = 0
inl₄₁ inl₄₂ : b = 0 → ¬0 < a → ¬b < 0 → a = 0 ∨ b = 0
inl₄₃ : b = 0 → ¬0 < a → ¬b < 0 → ¬a = 0 → b = 0
inl₄₄ : b < 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₄₅ inl₄₆ inl₄₇ : a = 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₄₈ inl₄₉ inl₅₀ : 0 = a → ¬0 < a → ¬b < 0 → ¬a = 0 → b = 0
inl₅₁ inl₅₂ inl₅₃ : a = 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₅₄ inl₅₅ inl₅₆ : 0 = a → ¬0 < a → ¬b < 0 → ¬a = 0 → b = 0
inl₅₇ inl₅₈ : a = 0 → ¬0 < a → ¬0 = a → ¬b < 0 → b = 0
inl₅₉ inl₆₀ : 0 = a → ¬0 < a → ¬b < 0 → ¬a = 0 → b = 0
⊢ (0 < a ∨ b < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < a ∨ 0 = a) ∨ b < 0 ∨ b = 0

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
h : 0 < a
h' : b < 0
inr : (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁ : (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₃ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₄ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₅ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₆ : 0 < b → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₇ : a < 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₈ : a = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₉ : b = 0 → (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0
inr₁₀ : 0 < b → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₁ : a < 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₂ : a = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₃ : b = 0 → ¬(0 < b ∨ 0 = b) → a < 0 ∨ a = 0
inr₁₄ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₅ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₆ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₇ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₈ : 0 < b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₁₉ : 0 = b → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₀ : a < 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₁ : a = 0 → (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0
inr₂₂ : 0 < b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₃ : 0 = b → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₄ : a < 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₅ : a = 0 → ¬(0 < b ∨ a < 0) → a = 0 ∨ b = 0
inr₂₆ : 0 < b → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₇ inr₂₈ : a < 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₂₉ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₀ inr₃₁ : a = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₂ : a = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₃ inr₃₄ : b = 0 → ¬0 < b → ¬0 = b → a < 0 ∨ a = 0
inr₃₅ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₃₆ : 0 < b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₇ inr₃₈ : 0 = b → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₃₉ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₄₀ : a < 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₄₁ inr₄₂ : a = 0 → ¬0 < b → ¬a < 0 → a = 0 ∨ b = 0
inr₄₃ : a = 0 → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₄₄ : a < 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₄₅ inr₄₆ inr₄₇ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₄₈ inr₄₉ inr₅₀ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₅₁ : a = 0 → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₅₂ inr₅₃ inr₅₄ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₅₅ inr₅₆ inr₅₇ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
inr₅₈ inr₅₉ : b = 0 → ¬0 < b → ¬0 = b → ¬a < 0 → a = 0
inr₆₀ inr₆₁ : 0 = b → ¬0 < b → ¬a < 0 → ¬a = 0 → b = 0
⊢ (0 < b ∨ a < 0) ∨ a = 0 ∨ b = 0 ↔ (0 < b ∨ 0 = b) ∨ a < 0 ∨ a = 0

Tactic:
tauto
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
mul_nonneg_iff.mpr <| .inl ⟨ha, hb⟩

Premises used: Iff.mpr, EReal.mul_nonneg_iff, And.intro, Or.inl
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
mul_pos_iff.mpr (Or.inl ⟨ha, hb⟩)

Premises used: Iff.mpr, And.intro, Or.inl, EReal.mul_pos_iff
-- Module: Mathlib.Data.EReal.Operations
Goal:
P : EReal → EReal → Prop
neg_left : ∀ {x y : EReal}, P x y → P (-x) y
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ (↑x : EReal)
top_bot : P ⊤ ⊥
zero_top : P 0 ⊤
zero_bot : P 0 ⊥
pos_top : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P (↑x : EReal) ⊥
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
⊢ ∀ (x y : EReal), P x y

Tactic:
have : ∀ y, (∀ x : ℝ, 0 < x → P x y) → ∀ x : ℝ, x < 0 → P x y := fun _ h x hx =>
    neg_neg (x : EReal) ▸ neg_left <| h _ (neg_pos_of_neg hx)
  @induction₂ P top_top top_pos top_zero top_neg top_bot pos_top pos_bot zero_top
    coe_coe zero_bot (this _ pos_top) (this _ pos_bot) (neg_left top_top)
    (fun x hx => neg_left <| top_pos x hx) (neg_left top_zero)
    (fun x hx => neg_left <| top_neg x hx) (neg_left top_bot)

Premises used: Bot.bot, EReal.induction₂, Top.top
-- Module: Mathlib.Data.EReal.Operations
Goal:
P : EReal → EReal → Prop
symm : ∀ {x y : EReal}, P x y → P y x
neg_left : ∀ {x y : EReal}, P x y → P (-x) y
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ (↑x : EReal)
top_zero : P ⊤ 0
coe_coe : ∀ (x y : ℝ), P (↑x : EReal) (↑y : EReal)
⊢ ∀ (x y : EReal), P x y

Tactic:
have neg_right : ∀ {x y}, P x y → P x (-y) := fun h => symm <| neg_left <| symm h
  have : ∀ x, (∀ y : ℝ, 0 < y → P x y) → ∀ y : ℝ, y < 0 → P x y := fun _ h y hy =>
    neg_neg (y : EReal) ▸ neg_right (h _ (neg_pos_of_neg hy))
  @induction₂_neg_left P neg_left top_top top_pos top_zero (this _ top_pos) (neg_right top_top)
    (symm top_zero) (symm <| neg_left top_zero) (fun x hx => symm <| top_pos x hx)
    (fun x hx => symm <| neg_left <| top_pos x hx) coe_coe

Premises used: Eq.rec, neg_pos_of_neg, neg_neg, EReal.induction₂_neg_left, Top.top, Neg.neg, Real.toEReal
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) (-⊤) 0 = -HMul.hMul (α := EReal) ⊤ 0

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) (-0) ⊤ = -HMul.hMul (α := EReal) 0 ⊤

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) (-0) ⊥ = -HMul.hMul (α := EReal) 0 ⊥

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, neg_zero
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) (-⊤) ⊤ = -HMul.hMul (α := EReal) ⊤ ⊤

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

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : -x * y = -(x * y)
neg_left : - -x * y = - -(x * y)
neg_left₁ : x * y = - -(x * y)
neg_left₂ neg_left₃ : x * y = x * y
⊢ - -x * y = -(-x * y)

Tactic:
rw [h, neg_neg, neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
coe_coe : -x * y = -(x * y)
⊢ -(↑x : EReal) * (↑y : EReal) = -((↑x : EReal) * (↑y : EReal))

Tactic:
norm_cast
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
⊢ -x * y = -(x * y)

Tactic:
neg_mul _ _

Premises used: neg_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
⊢ -x * y = -(x * y)

Tactic:
exact neg_mul _ _

Premises used: neg_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
top_pos : -⊤ * (↑x : EReal) = -⊤
top_pos₁ : ⊥ * (↑x : EReal) = ⊥
top_pos₂ top_pos₃ : Eq (α := EReal) ⊥ ⊥
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))

Tactic:
rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]

Premises used: EReal.bot_mul_coe_of_pos, EReal.top_mul_coe_of_pos, EReal.neg_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
pos_top : -(↑x : EReal) * ⊤ = -⊤
pos_top₁ : -(↑x : EReal) * ⊤ = ⊥
pos_top₂ : (↑(-x) : EReal) * ⊤ = ⊥
pos_top₃ pos_top₄ : Eq (α := EReal) ⊥ ⊥
⊢ -(↑x : EReal) * ⊤ = -((↑x : EReal) * ⊤)

Tactic:
rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
    coe_mul_top_of_neg (neg_neg_of_pos h)]

Premises used: EReal.coe_neg, EReal.coe_mul_top_of_pos, neg_neg_of_pos, EReal.neg_top, EReal.coe_mul_top_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : x < 0
top_neg : -⊤ * (↑x : EReal) = -⊥
top_neg₁ : ⊥ * (↑x : EReal) = -⊥
top_neg₂ : Eq (α := EReal) ⊤ (-⊥)
top_neg₃ top_neg₄ : Eq (α := EReal) ⊤ ⊤
⊢ -⊤ * (↑x : EReal) = -(⊤ * (↑x : EReal))

Tactic:
rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]

Premises used: EReal.bot_mul_coe_of_neg, EReal.neg_top, EReal.neg_bot, EReal.top_mul_coe_of_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x : ℝ
h : 0 < x
pos_bot : -(↑x : EReal) * ⊥ = -⊥
pos_bot₁ : -(↑x : EReal) * ⊥ = ⊤
pos_bot₂ : (↑(-x) : EReal) * ⊥ = ⊤
pos_bot₃ pos_bot₄ : Eq (α := EReal) ⊤ ⊤
⊢ -(↑x : EReal) * ⊥ = -((↑x : EReal) * ⊥)

Tactic:
rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
    coe_mul_bot_of_neg (neg_neg_of_pos h)]

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

Premises used: EReal.coe_neg, MulZeroClass.zero_mul, neg_neg, MulZeroClass.mul_zero, neg_mul, neg_zero, EReal.neg_top, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ -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)]

Premises used: EReal.coe_neg, MulZeroClass.zero_mul, neg_neg, MulZeroClass.mul_zero, neg_mul, neg_zero, EReal.neg_top, EReal.neg_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
rw : -y * x = -(y * x)
⊢ x * -y = -(x * y)

Tactic:
rw [x.mul_comm, x.mul_comm]

Premises used: EReal.mul_comm
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ -y * x = -(y * x)

Tactic:
y.neg_mul x

Premises used: EReal.neg_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
⊢ -y * x = -(y * x)

Tactic:
exact y.neg_mul x

Premises used: EReal.neg_mul
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
nth_rw : a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
nth_rw 1 [← neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Data.EReal.Operations
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
rw₅ 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

Tactic:
rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

Premises used: EReal.neg_lt_comm, EReal.lt_neg_comm, EReal.mul_pos_iff, neg_zero, mul_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
nth_rw : a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
nth_rw 1 [← neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Data.EReal.Operations
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
rw₅ 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

Tactic:
rw [EReal.le_neg, ← mul_neg, mul_nonneg_iff, EReal.neg_le, EReal.le_neg, neg_zero]

Premises used: EReal.mul_nonneg_iff, EReal.le_neg, EReal.neg_le, neg_zero, mul_neg
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
h : x * y = ⊤ ↔ x = ⊥ ∧ y < 0 ∨ x < 0 ∧ y = ⊥ ∨ x = ⊤ ∧ 0 < y ∨ 0 < x ∧ y = ⊤
⊢ y * x = ⊤ ↔ y = ⊥ ∧ x < 0 ∨ y < 0 ∧ x = ⊥ ∨ y = ⊤ ∧ 0 < x ∨ 0 < y ∧ x = ⊤

Tactic:
grind [EReal.mul_comm]

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

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

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

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

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

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

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

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

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

Premises used: LT.lt.le, EReal.coe_mul_bot_of_pos
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : ℝ
⊢ (↑x : EReal) * (↑y : EReal) = ⊤ ↔
    (↑x : EReal) = ⊥ ∧ (↑y : EReal) < 0 ∨
      (↑x : EReal) < 0 ∧ (↑y : EReal) = ⊥ ∨ (↑x : EReal) = ⊤ ∧ 0 < (↑y : EReal) ∨ 0 < (↑x : EReal) ∧ (↑y : EReal) = ⊤

Tactic:
simpa only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top,
      EReal.coe_pos, or_self, iff_false, EReal.coe_mul] using EReal.coe_ne_top _

Premises used: iff_false, false_and, EReal.coe_ne_bot, EReal.coe_neg', EReal.coe_pos, EReal.coe_mul, or_self, EReal.coe_ne_top, and_false
-- Module: Mathlib.Data.EReal.Operations
Goal:
⊢ HMul.hMul (α := EReal) 0 ⊥ = ⊤ ↔
    Eq (α := EReal) 0 ⊥ ∧ LT.lt (α := EReal) ⊥ 0 ∨
      LT.lt (α := EReal) 0 0 ∧ Eq (α := EReal) ⊥ ⊥ ∨
        Eq (α := EReal) 0 ⊤ ∧ LT.lt (α := EReal) 0 ⊥ ∨ LT.lt (α := EReal) 0 0 ∧ Eq (α := EReal) ⊥ ⊤

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

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

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

Tactic:
simp
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw :
  ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_top]

Premises used: ne_eq, EReal.mul_eq_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
push :
  (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
⊢ ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
push +distrib Not

Premises used: Not
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
⊢ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw :
  a = ⊤ ∧ b < 0 ∨ 0 < a ∧ b = ⊥ ∨ a = ⊥ ∧ 0 < b ∨ a < 0 ∧ b = ⊤ ↔
    a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
⊢ a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff,
    neg_lt_comm, lt_neg_comm, neg_zero]

Premises used: EReal.neg_lt_comm, EReal.neg_eq_top_iff, EReal.neg_eq_bot_iff, EReal.lt_neg_comm, EReal.neg_mul, neg_zero, EReal.mul_eq_top
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
rw :
  ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rw [ne_eq, mul_eq_bot]

Premises used: ne_eq, EReal.mul_eq_bot
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
push :
  (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
push +distrib Not

Premises used: Not
-- Module: Mathlib.Data.EReal.Operations
Goal:
a b : EReal
⊢ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)

Tactic:
rfl
-- Module: Mathlib.Data.EReal.Operations
Goal:
x y : EReal
hx : 0 ≤ x
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), ((↑a : EReal) * y).toENNReal = (↑a : EReal).toENNReal * y.toENNReal
top : ∀ (hx : LE.le (α := EReal) 0 ⊤), (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
induction x