α : Type ?u.21891
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.fst + a.snd
α : Type ?u.21891
inst✝ : TopologicalSpace α
⊢ ContinuousAt (fun p => p.fst + p.snd) (⊤, ⊤)
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]
α : Type ?u.21891
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.fst ∧ ↑r < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
α : Type ?u.21891
inst✝ : TopologicalSpace α
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.fst + a.snd
refine fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
  (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_
no goals
α : Type ?u.21891
inst✝ : TopologicalSpace α
r : ℝ
x✝ : EReal × EReal
h : ↑0 < x✝.fst ∧ ↑r < x✝.snd
⊢ ↑r < x✝.fst + x✝.snd
simpa only [coe_zero, zero_add] using add_lt_add h.1 h.2