-- 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) = ⊤
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) ⊥ ⊤
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤
have neg_bot : ∀ (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: 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