case mk
α : Type ?u.28673
inst✝ : TopologicalSpace α
x y : EReal
h : (x, y).fst ≠ ⊤ ∨ (x, y).snd ≠ ⊥
h' : (x, y).fst ≠ ⊥ ∨ (x, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (x, y)
α : Type ?u.28673
inst✝ : TopologicalSpace α
p : EReal × EReal
h : p.fst ≠ ⊤ ∨ p.snd ≠ ⊥
h' : p.fst ≠ ⊥ ∨ p.snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) p
rcases p with ⟨x, y⟩
case mk.h_bot.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊥, ⊥).fst ≠ ⊤ ∨ (⊥, ⊥).snd ≠ ⊥
h' : (⊥, ⊥).fst ≠ ⊥ ∨ (⊥, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)

case mk.h_bot.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊥, ↑a✝).fst ≠ ⊤ ∨ (⊥, ↑a✝).snd ≠ ⊥
h' : (⊥, ↑a✝).fst ≠ ⊥ ∨ (⊥, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a✝)

case mk.h_bot.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊥, ⊤).fst ≠ ⊤ ∨ (⊥, ⊤).snd ≠ ⊥
h' : (⊥, ⊤).fst ≠ ⊥ ∨ (⊥, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊤)

case mk.h_real.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊥).fst ≠ ⊤ ∨ (↑a✝, ⊥).snd ≠ ⊥
h' : (↑a✝, ⊥).fst ≠ ⊥ ∨ (↑a✝, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊥)

case mk.h_real.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).fst ≠ ⊤ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊥
h' : (↑a✝¹, ↑a✝).fst ≠ ⊥ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝¹, ↑a✝)

case mk.h_real.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊤).fst ≠ ⊤ ∨ (↑a✝, ⊤).snd ≠ ⊥
h' : (↑a✝, ⊤).fst ≠ ⊥ ∨ (↑a✝, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊤)

case mk.h_top.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊤, ⊥).fst ≠ ⊤ ∨ (⊤, ⊥).snd ≠ ⊥
h' : (⊤, ⊥).fst ≠ ⊥ ∨ (⊤, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊥)

case mk.h_top.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊤, ↑a✝).fst ≠ ⊤ ∨ (⊤, ↑a✝).snd ≠ ⊥
h' : (⊤, ↑a✝).fst ≠ ⊥ ∨ (⊤, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a✝)

case mk.h_top.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊤, ⊤).fst ≠ ⊤ ∨ (⊤, ⊤).snd ≠ ⊥
h' : (⊤, ⊤).fst ≠ ⊥ ∨ (⊤, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
case mk
α : Type ?u.28673
inst✝ : TopologicalSpace α
x y : EReal
h : (x, y).fst ≠ ⊤ ∨ (x, y).snd ≠ ⊥
h' : (x, y).fst ≠ ⊥ ∨ (x, y).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (x, y)
induction x using EReal.rec <;> induction y using EReal.rec
no goals
case mk.h_bot.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊥, ⊥).fst ≠ ⊤ ∨ (⊥, ⊥).snd ≠ ⊥
h' : (⊥, ⊥).fst ≠ ⊥ ∨ (⊥, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊥)
exact continuousAt_add_bot_bot
no goals
case mk.h_bot.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊥, ↑a✝).fst ≠ ⊤ ∨ (⊥, ↑a✝).snd ≠ ⊥
h' : (⊥, ↑a✝).fst ≠ ⊥ ∨ (⊥, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ↑a✝)
exact continuousAt_add_bot_coe _
no goals
case mk.h_bot.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊥, ⊤).fst ≠ ⊤ ∨ (⊥, ⊤).snd ≠ ⊥
h' : (⊥, ⊤).fst ≠ ⊥ ∨ (⊥, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊥, ⊤)
simp at h'
no goals
case mk.h_real.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊥).fst ≠ ⊤ ∨ (↑a✝, ⊥).snd ≠ ⊥
h' : (↑a✝, ⊥).fst ≠ ⊥ ∨ (↑a✝, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊥)
exact continuousAt_add_coe_bot _
no goals
case mk.h_real.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).fst ≠ ⊤ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊥
h' : (↑a✝¹, ↑a✝).fst ≠ ⊥ ∨ (↑a✝¹, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝¹, ↑a✝)
exact continuousAt_add_coe_coe _ _
no goals
case mk.h_real.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (↑a✝, ⊤).fst ≠ ⊤ ∨ (↑a✝, ⊤).snd ≠ ⊥
h' : (↑a✝, ⊤).fst ≠ ⊥ ∨ (↑a✝, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (↑a✝, ⊤)
exact continuousAt_add_coe_top _
no goals
case mk.h_top.h_bot
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊤, ⊥).fst ≠ ⊤ ∨ (⊤, ⊥).snd ≠ ⊥
h' : (⊤, ⊥).fst ≠ ⊥ ∨ (⊤, ⊥).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊥)
simp at h
no goals
case mk.h_top.h_real
α : Type ?u.28673
inst✝ : TopologicalSpace α
a✝ : ℝ
h : (⊤, ↑a✝).fst ≠ ⊤ ∨ (⊤, ↑a✝).snd ≠ ⊥
h' : (⊤, ↑a✝).fst ≠ ⊥ ∨ (⊤, ↑a✝).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ↑a✝)
exact continuousAt_add_top_coe _
no goals
case mk.h_top.h_top
α : Type ?u.28673
inst✝ : TopologicalSpace α
h : (⊤, ⊤).fst ≠ ⊤ ∨ (⊤, ⊤).snd ≠ ⊥
h' : (⊤, ⊤).fst ≠ ⊥ ∨ (⊤, ⊤).snd ≠ ⊤
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
exact continuousAt_add_top_top