-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_mul {p : EReal × EReal} (h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥)
    (h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤) (h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0) (h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) p

Proof state:
case mk.h_top.h_real
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✝)

Tactic:
simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄

Result:
case mk.h_top.h_real
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a✝)

Proof state:
case mk.h_real.h_bot
a✝ : ℝ
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
h₁ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (↑a✝, ⊥)

Tactic:
exact continuousAt_mul_symm2 (continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₁))

Result:
no goals

Proof state:
case mk.h_real.h_top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
h₂ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (↑a✝, ⊤)

Tactic:
exact continuousAt_mul_swap (continuousAt_mul_top_ne_zero h₂)

Result:
no goals

Proof state:
case mk.h_top.h_real
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a✝)

Tactic:
exact continuousAt_mul_top_ne_zero h₄

Result:
no goals

Proof state:
p : EReal × EReal
h₁ : p.1 ≠ 0 ∨ p.2 ≠ ⊥
h₂ : p.1 ≠ 0 ∨ p.2 ≠ ⊤
h₃ : p.1 ≠ ⊥ ∨ p.2 ≠ 0
h₄ : p.1 ≠ ⊤ ∨ p.2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) p

Tactic:
rcases p with ⟨x, y⟩

Result:
case mk
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (x, y)

Proof state:
case mk.h_top.h_bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ⊥)

Tactic:
exact continuousAt_mul_symm2 continuousAt_mul_top_top

Result:
no goals

Proof state:
case mk.h_real.h_real
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✝)

Tactic:
exact continuousAt_mul_coe_coe _ _

Result:
no goals

Proof state:
case mk
x y : EReal
h₁ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊥
h₂ : (x, y).1 ≠ 0 ∨ (x, y).2 ≠ ⊤
h₃ : (x, y).1 ≠ ⊥ ∨ (x, y).2 ≠ 0
h₄ : (x, y).1 ≠ ⊤ ∨ (x, y).2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (x, y)

Tactic:
induction x <;> induction y

Result:
case mk.h_bot.h_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 mk.h_bot.h_real
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 mk.h_bot.h_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 mk.h_real.h_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 mk.h_real.h_real
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 mk.h_real.h_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 mk.h_top.h_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 mk.h_top.h_real
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 mk.h_top.h_top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ⊤)

Proof state:
case mk.h_real.h_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✝, ⊥)

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁

Result:
case mk.h_real.h_bot
a✝ : ℝ
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
h₁ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (↑a✝, ⊥)

Proof state:
case mk.h_bot.h_bot
h₁ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊥
h₂ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊤
h₃ : (⊥, ⊥).1 ≠ ⊥ ∨ (⊥, ⊥).2 ≠ 0
h₄ : (⊥, ⊥).1 ≠ ⊤ ∨ (⊥, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊥, ⊥)

Tactic:
exact continuousAt_mul_symm3 continuousAt_mul_top_top

Result:
no goals

Proof state:
case mk.h_real.h_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✝, ⊤)

Tactic:
simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂

Result:
case mk.h_real.h_top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
h₂ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (↑a✝, ⊤)

Proof state:
case mk.h_bot.h_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:
exact EReal.neg_top ▸ continuousAt_mul_symm1 continuousAt_mul_top_top

Result:
no goals

Proof state:
case mk.h_bot.h_real
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
h₃ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊥, ↑a✝)

Tactic:
exact continuousAt_mul_symm1 (continuousAt_mul_top_ne_zero h₃)

Result:
no goals

Proof state:
case mk.h_top.h_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:
exact continuousAt_mul_top_top

Result:
no goals

Proof state:
case mk.h_bot.h_real
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✝)

Tactic:
simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₃

Result:
case mk.h_bot.h_real
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
h₃ : ¬a✝ = 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊥, ↑a✝)