no goals
α : Type u_1
β : Type ?u.123804
γ : Type ?u.123807
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f : Filter α
m : α → ℝ≥0∞
a : ℝ≥0∞
h : Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹)
⊢ Tendsto m f (𝓝 a)
simpa only [inv_inv] using Tendsto.inv h