Theorem: tendsto_atInf_iff_tendsto_nhds_zero (Ray/Misc/AtInf.lean)

State before:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ Tendsto f atInf l ↔ Tendsto (fun x => f x⁻¹) (𝓝[≠] 0) l
Tactic:
rw [Filter.HasBasis.tendsto_left_iff atInf_basis, Metric.nhdsWithin_basis_ball.tendsto_left_iff]
State after:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) ↔ ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

State before:
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) ↔ ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
constructor
State after:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) → ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t) → ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t

State before:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t) → ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
intro h t tl
State after:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

State before:
case mp
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
rcases h t tl with ⟨r, _, m⟩
State after:
case mp.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

State before:
case mp.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
by_cases rp : 0 < r
State after:
case pos
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

case neg
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t

State before:
case pos
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
use r⁻¹
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ 0 < r⁻¹ ∧ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ 0 < r⁻¹ ∧ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Tactic:
simp only [rp, inv_pos, true_and_iff]
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 r⁻¹ ∩ {0}ᶜ) t
Tactic:
intro x xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Tactic:
refine m ?_
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : x ∈ ball 0 r⁻¹ ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : ‖x‖ < r⁻¹ ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : 0 < r
x : 𝕜
xs : ‖x‖ < r⁻¹ ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [← lt_inv (norm_pos_iff.mpr xs.2) rp, xs.1, mem_setOf_eq, norm_inv]
State after:
no goals

State before:
case neg
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
Tactic:
use 1
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ 0 < 1 ∧ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ 0 < 1 ∧ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t
Tactic:
simp only [zero_lt_one, true_and_iff]
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
⊢ MapsTo (fun x => f x⁻¹) (ball 0 1 ∩ {0}ᶜ) t
Tactic:
intro x xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ (fun x => f x⁻¹) x ∈ t
Tactic:
refine m ?_
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : x ∈ ball 0 1 ∩ {0}ᶜ
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, mem_compl_iff, mem_singleton_iff] at xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ x⁻¹ ∈ {x | r < ‖x‖}
Tactic:
simp only [mem_setOf_eq, norm_inv]
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ r < ‖x‖⁻¹

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
rp : ¬0 < r
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
⊢ r < ‖x‖⁻¹
Tactic:
simp only [not_lt] at rp
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
rp : r ≤ 0
⊢ r < ‖x‖⁻¹

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
t : Set X
tl : t ∈ l
r : ℝ
left✝ : True
m : MapsTo f {x | r < ‖x‖} t
x : 𝕜
xs : ‖x‖ < 1 ∧ ¬x = 0
rp : r ≤ 0
⊢ r < ‖x‖⁻¹
Tactic:
exact lt_of_le_of_lt rp (inv_pos.mpr (norm_pos_iff.mpr xs.2))
State after:
no goals

State before:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
⊢ (∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t) → ∀ t ∈ l, ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
intro h t tl
State after:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t

State before:
case mpr
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
rcases h t tl with ⟨r, rp, m⟩
State after:
case mpr.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t

State before:
case mpr.intro.intro
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ ∃ i, True ∧ MapsTo f {x | i < ‖x‖} t
Tactic:
use r⁻¹
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ True ∧ MapsTo f {x | r⁻¹ < ‖x‖} t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ True ∧ MapsTo f {x | r⁻¹ < ‖x‖} t
Tactic:
simp only [true_and_iff]
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ MapsTo f {x | r⁻¹ < ‖x‖} t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
⊢ MapsTo f {x | r⁻¹ < ‖x‖} t
Tactic:
intro x xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : x ∈ {x | r⁻¹ < ‖x‖}
⊢ f x ∈ t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : x ∈ {x | r⁻¹ < ‖x‖}
⊢ f x ∈ t
Tactic:
simp only [mem_setOf_eq] at xs
State after:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ f x ∈ t

State before:
case h
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ f x ∈ t
Tactic:
have m := @m x⁻¹ ?_
State after:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : (fun x => f x⁻¹) x⁻¹ ∈ t
⊢ f x ∈ t

case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ x⁻¹ ∈ ball 0 r ∩ {0}ᶜ

State before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ x⁻¹ ∈ ball 0 r ∩ {0}ᶜ
Tactic:
simp only [mem_inter_iff, mem_ball_zero_iff, norm_inv, mem_compl_iff, mem_singleton_iff,
  inv_eq_zero]
State after:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0

State before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Tactic:
have np : 0 < ‖x‖ := _root_.trans (inv_pos.mpr rp) xs
State after:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
np : 0 < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0

State before:
case h.refine_1
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
np : 0 < ‖x‖
⊢ ‖x‖⁻¹ < r ∧ ¬x = 0
Tactic:
simp [inv_lt np rp, xs, norm_pos_iff.mp np]
State after:
no goals

State before:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : (fun x => f x⁻¹) x⁻¹ ∈ t
⊢ f x ∈ t
Tactic:
simp only [inv_inv] at m
State after:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : f x ∈ t
⊢ f x ∈ t

State before:
case h.refine_2
𝕜 X : Type
inst✝ : NontriviallyNormedField 𝕜
l : Filter X
f : 𝕜 → X
h : ∀ t ∈ l, ∃ i, 0 < i ∧ MapsTo (fun x => f x⁻¹) (ball 0 i ∩ {0}ᶜ) t
t : Set X
tl : t ∈ l
r : ℝ
rp : 0 < r
m✝ : MapsTo (fun x => f x⁻¹) (ball 0 r ∩ {0}ᶜ) t
x : 𝕜
xs : r⁻¹ < ‖x‖
m : f x ∈ t
⊢ f x ∈ t
Tactic:
exact m
State after:
no goals