-- Mathlib/Data/Real/EReal.lean
lemma mul_eq_top (a b : EReal) :
    a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤)

Proof state:
case symm.refine_2.inr.inr.inr
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : 0 < y✝ ∧ x✝ = ⊤
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))

Result:
no goals

Proof state:
case top_neg
x✝ : ℝ
hx : x✝ < 0
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

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

Result:
no goals

Proof state:
case neg_bot
x✝ : ℝ
hx : x✝ < 0
⊢ ↑x✝ * ⊥ = ⊤ ↔ ↑x✝ = ⊥ ∧ ⊥ < 0 ∨ ↑x✝ < 0 ∧ ⊥ = ⊥ ∨ ↑x✝ = ⊤ ∧ 0 < ⊥ ∨ 0 < ↑x✝ ∧ ⊥ = ⊤

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

Result:
no goals

Proof state:
case symm.refine_2.inr.inl
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : y✝ < 0 ∧ x✝ = ⊥
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
exact Or.inl ⟨h.2, h.1⟩

Result:
no goals

Proof state:
case symm.refine_2.inr.inr.inl
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : y✝ = ⊤ ∧ 0 < x✝
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))

Result:
no goals

Proof state:
case coe_coe
x y : ℝ
⊢ ↑x * ↑y = ⊤ ↔ ↑x = ⊥ ∧ ↑y < 0 ∨ ↑x < 0 ∧ ↑y = ⊥ ∨ ↑x = ⊤ ∧ 0 < ↑y ∨ 0 < ↑x ∧ ↑y = ⊤

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 _

Result:
no goals

Proof state:
case top_zero

⊢ ⊤ * 0 = ⊤ ↔ ⊤ = ⊥ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 = ⊥ ∨ ⊤ = ⊤ ∧ 0 < 0 ∨ 0 < ⊤ ∧ 0 = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case symm.refine_2.inl
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : y✝ = ⊥ ∧ x✝ < 0
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
exact Or.inr (Or.inl ⟨h.2, h.1⟩)

Result:
no goals

Proof state:
case bot_bot

⊢ ⊥ * ⊥ = ⊤ ↔ ⊥ = ⊥ ∧ ⊥ < 0 ∨ ⊥ < 0 ∧ ⊥ = ⊥ ∨ ⊥ = ⊤ ∧ 0 < ⊥ ∨ 0 < ⊥ ∧ ⊥ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case pos_bot
x✝ : ℝ
hx : 0 < x✝
⊢ ↑x✝ * ⊥ = ⊤ ↔ ↑x✝ = ⊥ ∧ ⊥ < 0 ∨ ↑x✝ < 0 ∧ ⊥ = ⊥ ∨ ↑x✝ = ⊤ ∧ 0 < ⊥ ∨ 0 < ↑x✝ ∧ ⊥ = ⊤

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

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ ⊤ * ↑x✝ = ⊤ ↔ ⊤ = ⊥ ∧ ↑x✝ < 0 ∨ ⊤ < 0 ∧ ↑x✝ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ↑x✝ ∨ 0 < ⊤ ∧ ↑x✝ = ⊤

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

Result:
no goals

Proof state:
case symm
x✝ y✝ : EReal
h : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤ ↔
    y✝ = ⊥ ∧ x✝ < 0 ∨ y✝ < 0 ∧ x✝ = ⊥ ∨ y✝ = ⊤ ∧ 0 < x✝ ∨ 0 < y✝ ∧ x✝ = ⊤

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;>
cases H with
  | inl h => exact Or.inr (Or.inl ⟨h.2, h.1⟩)
  | inr h => cases h with
    | inl h => exact Or.inl ⟨h.2, h.1⟩
    | inr h => cases h with
      | inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
      | inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))

Result:
no goals

Proof state:
case top_top

⊢ ⊤ * ⊤ = ⊤ ↔ ⊤ = ⊥ ∧ ⊤ < 0 ∨ ⊤ < 0 ∧ ⊤ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ⊤ ∨ 0 < ⊤ ∧ ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
a b : EReal
⊢ a * b = ⊤ ↔ a = ⊥ ∧ b < 0 ∨ a < 0 ∧ b = ⊥ ∨ a = ⊤ ∧ 0 < b ∨ 0 < a ∧ b = ⊤

Tactic:
induction a, b using EReal.induction₂_symm with
| symm h =>
  rw [EReal.mul_comm, h]
  refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩ <;>
  cases H with
    | inl h => exact Or.inr (Or.inl ⟨h.2, h.1⟩)
    | inr h => cases h with
      | inl h => exact Or.inl ⟨h.2, h.1⟩
      | inr h => cases h with
        | inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
        | inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))
| 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

Result:
no goals

Proof state:
case symm.refine_2.inr
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : y✝ < 0 ∧ x✝ = ⊥ ∨ y✝ = ⊤ ∧ 0 < x✝ ∨ 0 < y✝ ∧ x✝ = ⊤
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
cases h with
| inl h => exact Or.inl ⟨h.2, h.1⟩
| inr h => cases h with
| inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
| inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))

Result:
no goals

Proof state:
case 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:
rw [EReal.mul_comm, h]

Result:
case symm
x✝ y✝ : EReal
h : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤ ↔
    y✝ = ⊥ ∧ x✝ < 0 ∨ y✝ < 0 ∧ x✝ = ⊥ ∨ y✝ = ⊤ ∧ 0 < x✝ ∨ 0 < y✝ ∧ x✝ = ⊤

Proof state:
case top_bot

⊢ ⊤ * ⊥ = ⊤ ↔ ⊤ = ⊥ ∧ ⊥ < 0 ∨ ⊤ < 0 ∧ ⊥ = ⊥ ∨ ⊤ = ⊤ ∧ 0 < ⊥ ∨ 0 < ⊤ ∧ ⊥ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case zero_bot

⊢ 0 * ⊥ = ⊤ ↔ 0 = ⊥ ∧ ⊥ < 0 ∨ 0 < 0 ∧ ⊥ = ⊥ ∨ 0 = ⊤ ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case symm.refine_2.inr.inr
x✝ y✝ : EReal
h✝ : x✝ * y✝ = ⊤ ↔ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤
h : y✝ = ⊤ ∧ 0 < x✝ ∨ 0 < y✝ ∧ x✝ = ⊤
⊢ x✝ = ⊥ ∧ y✝ < 0 ∨ x✝ < 0 ∧ y✝ = ⊥ ∨ x✝ = ⊤ ∧ 0 < y✝ ∨ 0 < x✝ ∧ y✝ = ⊤

Tactic:
cases h with
| inl h => exact Or.inr (Or.inr (Or.inr ⟨h.2, h.1⟩))
| inr h => exact Or.inr (Or.inr (Or.inl ⟨h.2, h.1⟩))

Result:
no goals