awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Krasner
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
c : L
hc : IsConjRoot K x c
hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)‖

Tactic:
simpa [norm_iL, ← map_sub] using kr c hc (fun h ↦ (iff_false_intro hne).mp (congrArg iL h))

Premises used: map_sub, congrArg, iff_false_intro, Iff.mp, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ map (fun (x : α) ↦ a * x) (cobounded α) = cobounded α

Tactic:
DilationEquiv.map_cobounded (DilationEquiv.mulLeft a ha)

Premises used: DilationEquiv.map_cobounded, DilationEquiv.mulLeft
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ map (fun (x : α) ↦ x * a) (cobounded α) = cobounded α

Tactic:
DilationEquiv.map_cobounded (DilationEquiv.mulRight a ha)

Premises used: DilationEquiv.map_cobounded, DilationEquiv.mulRight
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto (fun (x : α) ↦ a * x) (cobounded α) (cobounded α)

Tactic:
(map_mul_left_cobounded ha).le

Premises used: Filter.map_mul_left_cobounded, Eq.le, Filter.Tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto (fun (x : α) ↦ x * a) (cobounded α) (cobounded α)

Tactic:
(map_mul_right_cobounded ha).le

Premises used: Filter.map_mul_right_cobounded, Eq.le, Filter.Tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
rw : Eq.{u_1 + 1} (α := Filter α) (comap Inv.inv (comap norm atTop)) (comap norm (comap Inv.inv atTop))
⊢ (cobounded α)⁻¹ = 𝓝[≠] 0

Tactic:
rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀,
    ← Filter.comap_inv]

Premises used: inv_atTop₀, comap_norm_nhdsGT_zero, comap_norm_atTop, Filter.comap_inv
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ Eq.{u_1 + 1} (α := Filter α) (comap Inv.inv (comap norm atTop)) (comap norm (comap Inv.inv atTop))

Tactic:
simp only [comap_comap, Function.comp_def, norm_inv]

Premises used: norm_inv, Function.comp_def, Filter.comap_comap
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
rw : (cobounded α)⁻¹⁻¹ = cobounded α
rw₁ rw₂ : cobounded α = cobounded α
⊢ (𝓝[≠] 0)⁻¹ = cobounded α

Tactic:
rw [← inv_cobounded₀, inv_inv]

Premises used: Filter.inv_cobounded₀, inv_inv
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ Tendsto Inv.inv (cobounded α) (𝓝[≠] 0)

Tactic:
inv_cobounded₀.le

Premises used: Set.Mem, Filter.inv_cobounded₀, Eq.le, Filter.Tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ Tendsto Inv.inv (cobounded α) (𝓝 0)

Tactic:
tendsto_inv₀_cobounded'.mono_right inf_le_left

Premises used: inf_le_left, Filter.Tendsto.mono_right, Filter.tendsto_inv₀_cobounded'
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ Tendsto Inv.inv (𝓝[≠] 0) (cobounded α)

Tactic:
inv_nhdsNE_zero.le

Premises used: Filter.inv_nhdsNE_zero, Set.Mem, Eq.le, Filter.Tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
rw : ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
⊢ UniformContinuousOn Inv.inv s

Tactic:
rw [Metric.uniformContinuousOn_iff_le]

Premises used: Metric.uniformContinuousOn_iff_le
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
rcases :
  ∀ (r : ℝ) (hr₀ : 0 < r) (hr : {y : α | ‖y‖ < r} ⊆ sᶜ), ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp hs with ⟨r, hr₀, hr⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp, NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : {y : α | ‖y‖ < r} ⊆ sᶜ
⊢ s ⊆ {a : α | r ≤ ‖a‖}

Tactic:
simp only [Set.subset_compl_comm (t := s), Set.compl_setOf, not_lt] at hr

Premises used: Set.subset_compl_comm, not_lt, Set.compl_setOf
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
⊢ ∀ x ∈ s, x ≠ 0

Tactic:
have hs₀ : ∀ x ∈ s, x ≠ 0 := fun x hx ↦ norm_pos_iff.mp <| hr₀.trans_le (hr hx)
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
⊢ ε * HPow.hPow (β := ℕ) r 2 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
refine : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2), dist x⁻¹ y⁻¹ ≤ ε
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
refine ⟨ε * r ^ 2, by positivity, fun x hx y hy hxy ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y x * ‖y‖⁻¹

Tactic:
simp [dist_eq_norm, inv_sub_inv' (hs₀ x hx) (hs₀ y hy)]

Premises used: dist_eq_norm, inv_sub_inv'
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
rw : ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
⊢ ‖x‖⁻¹ * dist y x * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
h₁ : r ≤ ‖x‖
h₂ : r ≤ ‖y‖
⊢ ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ r ≤ ‖x‖

Tactic:
hr ‹_›

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ r ≤ ‖x‖

Tactic:
exact hr ‹_›
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ r ≤ ‖y‖

Tactic:
hr ‹_›

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ r ≤ ‖y‖

Tactic:
exact hr ‹_›
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
⊢ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹ = ε

Tactic:
field_simp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : Dist.dist x y ≤ ε * HPow.hPow (β := ℕ) r 2
dist : Dist.dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * Dist.dist y x * ‖y‖⁻¹
dist₁ : ‖x‖⁻¹ * Dist.dist y x * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
dist₂ : r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹ = ε
⊢ Dist.dist x⁻¹ y⁻¹ ≤ ε

Tactic:
calc
    dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y x * ‖y‖⁻¹ := by
      simp [dist_eq_norm, inv_sub_inv' (hs₀ x hx) (hs₀ y hy)]
    _ ≤ r⁻¹ * (ε * r ^ 2) * r⁻¹ := by
      rw [dist_comm]
      gcongr <;> exact hr ‹_›
    _ = ε := by field_simp

Premises used: HMul.hMul, Inv.inv, HPow.hPow, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
inst_1 : UniformSpace X
f : X → α
s : Set X
hf : UniformContinuousOn f s
hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (f '' s)ᶜ
⊢ UniformContinuousOn f⁻¹ s

Tactic:
uniformContinuousOn_inv₀ hf₀ |>.comp hf (Set.mapsTo_image f s)

Premises used: Set.mapsTo_image, UniformContinuousOn.comp, uniformContinuousOn_inv₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
inst_1 : UniformSpace X
f : X → α
hf : UniformContinuous f
hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (Set.range f)ᶜ
simp :
  ∀ (hf : UniformContinuousOn f Set.univ) (hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (f '' Set.univ)ᶜ),
    UniformContinuousOn f⁻¹ Set.univ
⊢ UniformContinuous f⁻¹

Tactic:
simp only [← uniformContinuousOn_univ, ← Set.image_univ] at *

Premises used: Set.image_univ, uniformContinuousOn_univ
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
inst_1 : UniformSpace X
f : X → α
hf : UniformContinuousOn f Set.univ
hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (f '' Set.univ)ᶜ
⊢ UniformContinuousOn f⁻¹ Set.univ

Tactic:
hf.inv₀ hf₀

Premises used: UniformContinuousOn.inv₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
inst_1 : UniformSpace X
f : X → α
hf : UniformContinuousOn f Set.univ
hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (f '' Set.univ)ᶜ
⊢ UniformContinuousOn f⁻¹ Set.univ

Tactic:
exact hf.inv₀ hf₀

Premises used: UniformContinuousOn.inv₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
rw :
  ∀ (hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α))
    (hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)),
    ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *

Premises used: tendstoLocallyUniformlyOn_iff_forall_tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
rcases :
  ∀ (U : Set X) (hUx : U ∈ 𝓝[s] x) (r : ℝ) (hr₀ : 0 < r) (hr : Disjoint (f '' id U) (ball 0 r)),
    Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
⊢ Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)

Tactic:
rcases basis_sets _ |>.map _ |>.disjoint_iff nhds_basis_ball
    |>.mp (hf x hx) with ⟨U, hUx, r, hr₀, hr⟩

Premises used: Filter.HasBasis.map, Filter.HasBasis.disjoint_iff, Filter.basis_sets, Iff.mp, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
⊢ Membership.mem (γ := Filter α) (𝓝 0) (closedBall 0 (r / 2))ᶜᶜ

Tactic:
simp [closedBall_mem_nhds, hr₀]

Premises used: Metric.closedBall_mem_nhds
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
refine :
  ∀ᶠ (a : ι × X) in l ×ˢ 𝓝[s] x,
    (f a.2, F a.1 a.2) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ
⊢ Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)

Tactic:
refine Tendsto.comp (uniformContinuousOn_inv₀ (s := (closedBall (0 : α) (r / 2))ᶜ)
    (by simp [closedBall_mem_nhds, hr₀])) <| tendsto_inf.mpr ⟨hF x hx, tendsto_principal.mpr ?_⟩

Premises used: Iff.mpr, Filter.tendsto_inf, Filter.tendsto_principal, And.intro, uniformContinuousOn_inv₀, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
h :
  ∀ (y : ι × X)
    (hy₁ :
      Membership.mem (γ := Set (ι × X))
        (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y)
    (hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y),
    (f y.2, F y.1 y.2) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ
⊢ ∀ᶠ (a : ι × X) in l ×ˢ 𝓝[s] x,
    (f a.2, F a.1 a.2) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ

Tactic:
filter_upwards [hF x hx (dist_mem_uniformity (half_pos hr₀)), tendsto_snd hUx] with y hy₁ hy₂

Premises used: half_pos, Filter.tendsto_snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ :
  Membership.mem (γ := Set (ι × X))
    (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
⊢ r ≤ ‖f y.2‖

Tactic:
simp_all [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ :
  Membership.mem (γ := Set (ι × X))
    (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
⊢ r ≤ ‖f y.2‖

Tactic:
have : r ≤ ‖f y.2‖ := by simp_all [Set.disjoint_left]
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ :
  Membership.mem (γ := Set (ι × X))
    (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
this : r ≤ ‖f y.2‖
⊢ ‖f y.2 - F y.1 y.2‖ < r / 2

Tactic:
simp [dist_eq_norm_sub] at hy₁

Premises used: dist_eq_norm_sub
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
this : r ≤ ‖f y.2‖
hy₁ : ‖f y.2 - F y.1 y.2‖ < r / 2
linarith : ‖F y.1 y.2‖ ≤ r / 2 → 2 / 2 = 1
linarith₁ : ‖F y.1 y.2‖ ≤ r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖F y.1 y.2‖ ≤ r / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ‖F y.1 y.2‖ ≤ r / 2 → 2 / 2 = 1
linarith₄ : ‖F y.1 y.2‖ ≤ r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ‖F y.1 y.2‖ ≤ r / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : ‖F y.1 y.2‖ ≤ r / 2 → 2 / 2 = 1
linarith₇ : ‖F y.1 y.2‖ ≤ r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : ‖F y.1 y.2‖ ≤ r / 2 → GT.gt (α := ℝ) 2 0
linarith₉ :
  ‖F y.1 y.2‖ ≤ r / 2 →
    2 * (r - ‖f y.2‖) + (2 * ‖f y.2 - F y.1 y.2‖ - 1 * r) + (2 * ‖F y.1 y.2‖ - 1 * r) +
        2 * (‖f y.2‖ - ‖F y.1 y.2‖ - ‖f y.2 - F y.1 y.2‖) =
      0
linarith₁₀ linarith₁₁ : ‖F y.1 y.2‖ ≤ r / 2 → GT.gt (α := ℝ) 2 0
⊢ r / 2 < ‖F y.1 y.2‖

Tactic:
linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]

Premises used: Prod.fst, norm_sub_norm_le, Prod.snd
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ :
  Membership.mem (γ := Set (ι × X))
    (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
this : r ≤ ‖f y.2‖
⊢ r / 2 < ‖F y.1 y.2‖

Tactic:
have : r / 2 < ‖F y.1 y.2‖ := by
    simp [dist_eq_norm_sub] at hy₁
    linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ :
  Membership.mem (γ := Set (ι × X))
    (Set.preimage (β := α × α) (fun (y : ι × X) ↦ (f y.2, F y.1 y.2)) {p : α × α | dist p.1 p.2 < r / 2}) y
hy₂ : Membership.mem (γ := Set (ι × X)) (Prod.snd ⁻¹' U) y
this_1 : r ≤ ‖f y.2‖
this : r / 2 < ‖F y.1 y.2‖
⊢ (f y.2, F y.1 y.2) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ

Tactic:
simp_all [(half_lt_self hr₀).trans_le]

Premises used: half_lt_self, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
rw :
  ∀ (hF : TendstoLocallyUniformlyOn F f l Set.univ) (hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)),
    TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
rw [← tendstoLocallyUniformlyOn_univ] at *

Premises used: tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
apply : ∀ (x : X), Membership.mem (γ := Set X) Set.univ x → Disjoint (map f (𝓝[Set.univ] x)) (𝓝 0)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ

Tactic:
apply hF.inv₀_of_disjoint

Premises used: TendstoLocallyUniformlyOn.inv₀_of_disjoint
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ ∀ (x : X), Membership.mem (γ := Set X) Set.univ x → Disjoint (map f (𝓝[Set.univ] x)) (𝓝 0)

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hf : ContinuousOn f s
hf₀ : ∀ x ∈ s, f x ≠ 0
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s

Tactic:
hF.inv₀_of_disjoint fun x hx ↦ disjoint_nhds_nhds.2 (hf₀ x hx) |>.mono_left (hf x hx)

Premises used: Iff.mpr, Disjoint.mono_left, TendstoLocallyUniformlyOn.inv₀_of_disjoint, disjoint_nhds_nhds
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf₀ : ∀ (x : X), f x ≠ 0
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
hF.inv₀_of_disjoint fun x ↦ disjoint_nhds_nhds.2 (hf₀ x) |>.mono_left (hf.tendsto x)

Premises used: Iff.mpr, Continuous.tendsto, Disjoint.mono_left, TendstoLocallyUniformly.inv₀_of_disjoint, disjoint_nhds_nhds