Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₃ : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ 0
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)

pp: case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

pp: case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

pp: case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

pp: case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

pp: case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

pp: case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)

Tactic:
· simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃
    exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

Goal state after:
case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)

case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)

case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)