Theorem: tendsto_inv_iff_tendsto (Ray/Misc/Topology.lean)

State before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
⊢ Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹) ↔ Tendsto f l (𝓝 a)
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.inv₀ a0⟩
State after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto f l (𝓝 a)

State before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
⊢ Tendsto f l (𝓝 a)
Tactic:
have h := h.inv₀ (inv_ne_zero a0)
State after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => (f x)⁻¹⁻¹) l (𝓝 a⁻¹⁻¹)
⊢ Tendsto f l (𝓝 a)

State before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => (f x)⁻¹⁻¹) l (𝓝 a⁻¹⁻¹)
⊢ Tendsto f l (𝓝 a)
Tactic:
field_simp [a0] at h
State after:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => f x) l (𝓝 a)
⊢ Tendsto f l (𝓝 a)

State before:
A B : Type
inst✝ : NontriviallyNormedField B
l : Filter A
f : A → B
a : B
a0 : a ≠ 0
h✝ : Tendsto (fun x => (f x)⁻¹) l (𝓝 a⁻¹)
h : Tendsto (fun x => f x) l (𝓝 a)
⊢ Tendsto f l (𝓝 a)
Tactic:
exact h
State after:
no goals