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