α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
huv : ∃ φ x, u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => (u x)⁻¹) ~[l] fun x => (v x)⁻¹
rw [isEquivalent_iff_exists_eq_mul] at *
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
huv : ∃ φ x, u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
rcases huv with ⟨φ, hφ, h⟩
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
rw [← inv_one]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ (fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ x, (fun x => (u x)⁻¹) =ᶠ[l] φ * fun x => (v x)⁻¹
refine' ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by norm_num), _⟩
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ (fun x => (u x)⁻¹) =ᶠ[l] (fun x => (φ x)⁻¹) * fun x => (v x)⁻¹
convert h.inv
no goals
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((fun x => (φ x)⁻¹) * fun x => (v x)⁻¹) x✝ = ((φ * v) x✝)⁻¹
simp [mul_comm]
no goals
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ 1 ≠ 0
norm_num