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