[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
⊢ Continuous fun p => p.fst + p.snd
[PROOFSTEP]
refine' continuous_iff_continuousAt.2 _
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
⊢ ∀ (x : G × G), ContinuousAt (fun p => p.fst + p.snd) x
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b : G
⊢ ContinuousAt (fun p => p.fst + p.snd) (a, b)
[PROOFSTEP]
refine' LinearOrderedAddCommGroup.tendsto_nhds.2 fun ε ε0 => _
[GOAL]
case mk
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩ | ⟨_h₁, h₂⟩)
[GOAL]
case mk.inl.intro.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
filter_upwards [(eventually_abs_sub_lt a δ0).prod_nhds (eventually_abs_sub_lt b (sub_pos.2 δε))]
[GOAL]
case h
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
⊢ ∀ (a_1 : G × G), |a_1.fst - a| < δ ∧ |a_1.snd - b| < ε - δ → |a_1.fst + a_1.snd - (a + b)| < ε
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
x y : G
hx : |x - a| < δ
hy : |y - b| < ε - δ
⊢ |(x, y).fst + (x, y).snd - (a + b)| < ε
[PROOFSTEP]
rw [add_sub_add_comm]
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
x y : G
hx : |x - a| < δ
hy : |y - b| < ε - δ
⊢ |(x, y).fst - a + ((x, y).snd - b)| < ε
[PROOFSTEP]
calc
  |x - a + (y - b)| ≤ |x - a| + |y - b| := abs_add _ _
  _ < δ + (ε - δ) := (add_lt_add hx hy)
  _ = ε := add_sub_cancel'_right _ _
[GOAL]
case mk.inr.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
have hε : ∀ {x y}, |x - y| < ε → x = y := by
  intro x y h
  simpa [sub_eq_zero] using h₂ _ h
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
⊢ ∀ {x y : G}, |x - y| < ε → x = y
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
x y : G
h : |x - y| < ε
⊢ x = y
[PROOFSTEP]
simpa [sub_eq_zero] using h₂ _ h
[GOAL]
case mk.inr.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
filter_upwards [(eventually_abs_sub_lt a ε0).prod_nhds (eventually_abs_sub_lt b ε0)]
[GOAL]
case h
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
⊢ ∀ (a_1 : G × G), |a_1.fst - a| < ε ∧ |a_1.snd - b| < ε → |a_1.fst + a_1.snd - (a + b)| < ε
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
x y : G
hx : |x - a| < ε
hy : |y - b| < ε
⊢ |(x, y).fst + (x, y).snd - (a + b)| < ε
[PROOFSTEP]
simpa [hε hx, hε hy]
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a ε : G
ε0 : ε > 0
x : G
hx : |x - a| < ε
⊢ |-x - (fun a => -a) a| < ε
[PROOFSTEP]
rwa [neg_sub_neg, abs_sub_comm]
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
⊢ Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)
[PROOFSTEP]
refine' ⟨fun h => (abs_zero : |(0 : G)| = 0) ▸ h.abs, fun h => _⟩
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun a => -|f a|) l (𝓝 0) := (neg_zero : -(0 : G) = 0) ▸ h.neg
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -|f a|) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
exact tendsto_of_tendsto_of_tendsto_of_le_of_le this h (fun x => neg_abs_le_self <| f x) fun x => le_abs_self <| f x
