-- Mathlib/Analysis/Asymptotics/TVS.lean
theorem IsLittleOTVS.add [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    {f₁ f₂ : α → E} {g : α → F} {l : Filter α}
    (h₁ : f₁ =o[𝕜; l] g) (h₂ : f₂ =o[𝕜; l] g) : (f₁ + f₂) =o[𝕜; l] g

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
⊢ (f₁ + f₂) =o[𝕜;l] g

Tactic:
rw [(nhds_basis_balanced 𝕜 E).add_self.isLittleOTVS_iff (basis_sets _)]

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
⊢ ∀ (i : Set E),
    i ∈ 𝓝 0 ∧ Balanced 𝕜 i →
      ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i + id i) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
⊢ ∀ (i : Set E),
    i ∈ 𝓝 0 ∧ Balanced 𝕜 i →
      ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i + id i) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Tactic:
rintro U ⟨hU, hUb⟩

Result:
case intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Tactic:
refine ⟨V, hV, fun ε hε ↦ ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id V) (g x)

Proof state:
case h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id V) (g x)

Tactic:
exact (egauge_add_add_le hUb hUb _ _).trans (max_le hx₁ hx₂)

Result:
no goals

Proof state:
case intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Tactic:
rcases ((h₁.eventually_smallSets U hU).and (h₂.eventually_smallSets U hU)).exists_mem_of_smallSets
  with ⟨V, hV, hVf₁, hVf₂⟩

Result:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id j) (g x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id V) (g x)

Tactic:
filter_upwards [hVf₁ ε hε, hVf₂ ε hε] with x hx₁ hx₂

Result:
case h
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜;l] g
h₂ : f₂ =o[𝕜;l] g
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
V : Set F
hV : V ∈ 𝓝 0
hVf₁ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hVf₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ egauge 𝕜 (id U + id U) ((f₁ + f₂) x) ≤ ↑ε * egauge 𝕜 (id V) (g x)