-- Mathlib/Analysis/Asymptotics/TVS.lean
theorem isLittleOTVS_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    f₁ =o[𝕜;l] g₁ ↔ 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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g₁ x)) ↔
    ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g₂ x)

Tactic:
refine forall₂_congr fun U hU => exists_congr fun V => and_congr_right fun hV =>
  forall₂_congr fun ε hε => Filter.eventually_congr ?_

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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g₁ x) ↔ egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ egauge 𝕜 U (f₁ a✝) ≤ ↑ε * egauge 𝕜 V (g₁ a✝) ↔ egauge 𝕜 U (f₂ a✝) ≤ ↑ε * egauge 𝕜 V (g₂ a✝)

Tactic:
rw [e₁, e₂]

Result:
no goals

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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[𝕜;l] g₁ ↔ f₂ =o[𝕜;l] g₂

Tactic:
simp only [IsLittleOTVS]

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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g₁ x)) ↔
    ∀ U ∈ 𝓝 0, ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 U (f₁ x) ≤ ↑ε * egauge 𝕜 V (g₁ x) ↔ egauge 𝕜 U (f₂ x) ≤ ↑ε * egauge 𝕜 V (g₂ x)

Tactic:
filter_upwards [hf, hg] with _ e₁ e₂

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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
ε : ℝ≥0
hε : ε ≠ 0
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ egauge 𝕜 U (f₁ a✝) ≤ ↑ε * egauge 𝕜 V (g₁ a✝) ↔ egauge 𝕜 U (f₂ a✝) ≤ ↑ε * egauge 𝕜 V (g₂ a✝)