-- 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.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)

Tactic:
filter_upwards [hV ε hε, hW 1 one_ne_zero] with a hfga hgka

Result:
case h
α : 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 𝕜 U (f a) ≤ ↑ε * egauge 𝕜 W (k a)

Proof state:
case h
α : 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:
gcongr

Result:
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)

Proof state:
α : 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 ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (k x)

Tactic:
obtain ⟨V, hV0, hV⟩ := hfg U hU

Result:
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)

Proof state:
α : 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
⊢ f =o[𝕜;l] k

Tactic:
intros U hU

Result:
α : 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 ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (k x)

Proof state:
case h
α : 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 𝕜 U (f a) ≤ ↑ε * egauge 𝕜 W (k a)

Tactic:
refine hfga.trans ?_

Result:
case h
α : 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)