-- Mathlib/Analysis/Asymptotics/TVS.lean
theorem IsLittleOTVS.trans {k : α → G} (hfg : f =o[𝕜;l] g) (hgk : g =o[𝕜;l] k) : f =o[𝕜;l] k

Proof state:
case intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜;l] g
hgk : g =o[𝕜;l] k
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV0 : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (k x)

Tactic:
obtain ⟨W, hW0, hW⟩ := hgk V hV0

Result:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜;l] g
hgk : g =o[𝕜;l] k
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV0 : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW0 : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (k x)

Proof state:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜;l] g
hgk : g =o[𝕜;l] k
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV0 : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW0 : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (k x)

Tactic:
refine ⟨W, hW0, fun ε hε => ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜;l] g
hgk : g =o[𝕜;l] k
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV0 : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW0 : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)

Proof state:
case h.bc
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜;l] g
hgk : g =o[𝕜;l] k
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV0 : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
W : Set G
hW0 : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
a : α
hfga : egauge 𝕜 U (f a) ≤ ↑ε * egauge 𝕜 V (g a)
hgka : egauge 𝕜 V (g a) ≤ ↑1 * egauge 𝕜 W (k a)
⊢ egauge 𝕜 V (g a) ≤ egauge 𝕜 W (k a)

Tactic:
simpa using hgka

Result:
no goals