-- Mathlib/Analysis/Asymptotics/TVS.lean
lemma IsLittleOTVS.tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} (h : g =o[𝕜;l] f) :
    Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => (f x)⁻¹ • g x) x) ≤ ↑ε * egauge 𝕜 V (1 x)

Tactic:
rcases h.smul_left f⁻¹ U hU with ⟨V, hV₀, hV⟩

Result:
case intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
V : Set 𝕜
hV₀ : V ∈ 𝓝 0
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => (f x)⁻¹ • g x) x) ≤ ↑ε * egauge 𝕜 V (1 x)

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
⊢ Tendsto (fun x => (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
rw [← isLittleOTVS_one (𝕜 := 𝕜)]

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
⊢ (fun x => (f x)⁻¹ • g x) =o[𝕜;l] 1

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
⊢ (fun x => (f x)⁻¹ • g x) =o[𝕜;l] 1

Tactic:
intro U hU

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => (f x)⁻¹ • g x) x) ≤ ↑ε * egauge 𝕜 V (1 x)

Proof state:
case intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
V : Set 𝕜
hV₀ : V ∈ 𝓝 0
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
⊢ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x) ≤ ↑ε * egauge 𝕜 V (1 x)

Tactic:
by_cases hx₀ : f x = 0 <;> simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
V : Set 𝕜
hV₀ : V ∈ 𝓝 0
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => (f x)⁻¹ • g x) x) ≤ ↑ε * egauge 𝕜 V (1 x)

Tactic:
refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩

Result:
case intro.intro
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
h : g =o[𝕜;l] f
U : Set E
hU : U ∈ 𝓝 0
V : Set 𝕜
hV₀ : V ∈ 𝓝 0
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U ((fun x => f⁻¹ x • g x) x) ≤ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x)
⊢ ↑ε * egauge 𝕜 V ((fun x => f⁻¹ x • f x) x) ≤ ↑ε * egauge 𝕜 V (1 x)