awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have symm : ∀ {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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have top_top : 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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have top_pos : ∀ (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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have top_zero : 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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
top_zero :
  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 ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have top_neg : ∀ (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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
top_zero :
  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 ⊤
top_neg :
  ∀ (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) = ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have top_bot : 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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
top_zero :
  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 ⊤
top_neg :
  ∀ (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) = ⊤
top_bot :
  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) ⊥ ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have pos_bot : ∀ (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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
top_zero :
  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 ⊤
top_neg :
  ∀ (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) = ⊤
top_bot :
  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) ⊥ ⊤
pos_bot :
  ∀ (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) ⊥ ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have coe_coe : ∀ (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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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 : 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 = ⊤
top_top :
  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) ⊤ ⊤
top_pos :
  ∀ (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) = ⊤
top_zero :
  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 ⊤
top_neg :
  ∀ (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) = ⊤
top_bot :
  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) ⊥ ⊤
pos_bot :
  ∀ (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) ⊥ ⊤
coe_coe :
  ∀ (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) = ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have zero_bot : 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: induction a, b using EReal.induction₂_symm with
  | symm h => grind [EReal.mul_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
  | top_bot => simp
  | pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
  | coe_coe x y =>
    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 _
  | 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
⊢ a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
have 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 ≠ ⊤)
Tactic: rw [ne_eq, mul_eq_top]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ ¬(a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤)
have 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 ≠ ⊤)
Tactic: push +distrib Not
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b = ⊥ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
have 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 = ⊤
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]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
have 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 ≠ ⊤)
Tactic: rw [ne_eq, mul_eq_bot]
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
a b : EReal
⊢ ¬(a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤) ↔
    (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤)
have 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 ≠ ⊤)
Tactic: push +distrib Not
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : 0 ≤ x
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
x y : EReal
hx : 0 ≤ x
bot : ∀ (hx : LE.le (α := EReal) 0 ⊥), (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have coe : ∀ (a : ℝ) (hx : 0 ≤ (↑a : EReal)), ((↑a : EReal) * y).toENNReal = (↑a : EReal).toENNReal * y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
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
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal
have top : ∀ (hx : LE.le (α := EReal) 0 ⊤), (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal
Tactic: induction x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊥
⊢ (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
have bot : (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊥
bot : (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥
⊢ (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
have bot₁ : ∀ (a : ℝ), (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊥
bot : (HMul.hMul (α := EReal) ⊥ ⊥).toENNReal = toENNReal ⊥ * toENNReal ⊥
bot₁ : ∀ (a : ℝ), (⊥ * (↑a : EReal)).toENNReal = toENNReal ⊥ * (↑a : EReal).toENNReal
⊢ (⊥ * y).toENNReal = toENNReal ⊥ * y.toENNReal
have bot₂ : (HMul.hMul (α := EReal) ⊥ ⊤).toENNReal = toENNReal ⊥ * toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
hx : 0 ≤ (↑a : EReal)
⊢ ((↑a : EReal) * y).toENNReal = (↑a : EReal).toENNReal * y.toENNReal
have coe : ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥
⊢ ((↑a : EReal) * y).toENNReal = (↑a : EReal).toENNReal * y.toENNReal
have coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) * (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal * (↑a_1 : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
a : ℝ
hx : 0 ≤ (↑a : EReal)
coe : ((↑a : EReal) * ⊥).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊥
coe₁ : ∀ (a_1 : ℝ), ((↑a : EReal) * (↑a_1 : EReal)).toENNReal = (↑a : EReal).toENNReal * (↑a_1 : EReal).toENNReal
⊢ ((↑a : EReal) * y).toENNReal = (↑a : EReal).toENNReal * y.toENNReal
have coe₂ : ((↑a : EReal) * ⊤).toENNReal = (↑a : EReal).toENNReal * toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊤
⊢ (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal
have top : (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊤
top : (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥
⊢ (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal
have top₁ : ∀ (a : ℝ), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Data.EReal.Operations (goal)
Goal:
y : EReal
hx : LE.le (α := EReal) 0 ⊤
top : (HMul.hMul (α := EReal) ⊤ ⊥).toENNReal = toENNReal ⊤ * toENNReal ⊥
top₁ : ∀ (a : ℝ), (⊤ * (↑a : EReal)).toENNReal = toENNReal ⊤ * (↑a : EReal).toENNReal
⊢ (⊤ * y).toENNReal = toENNReal ⊤ * y.toENNReal
have top₂ : (HMul.hMul (α := EReal) ⊤ ⊤).toENNReal = toENNReal ⊤ * toENNReal ⊤
Tactic: induction y
Cleared hypotheses: y