awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ ‖x‖⁻¹ * dist y x * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
have rw : ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
have h₁ : r ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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‖
⊢ ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
have h₂ : r ≤ ‖y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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⁻¹ ≤ ε
have dist : dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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.dist x⁻¹ y⁻¹ ≤ ε
have dist₁ : ‖x‖⁻¹ * Dist.dist y x * ‖y‖⁻¹ ≤ r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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.dist x⁻¹ y⁻¹ ≤ ε
have dist₂ : r⁻¹ * (ε * HPow.hPow (β := ℕ) r 2) * r⁻¹ = ε
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)ᶜ
⊢ UniformContinuous f⁻¹
have simp : ∀ (hf : UniformContinuousOn f Set.univ) (hf₀ : Membership.mem (γ := Filter α) (𝓝 0) (f '' Set.univ)ᶜ),
  UniformContinuousOn f⁻¹ Set.univ
Tactic: simp only [← uniformContinuousOn_univ, ← Set.image_univ] at *
Cleared hypotheses: hf, hf₀
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
have 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) (𝓤 α)
Tactic: rw [tendstoLocallyUniformlyOn_iff_forall_tendsto] at *
Cleared hypotheses: hF, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
have 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) (𝓤 α)
Tactic: rcases basis_sets _ |>.map _ |>.disjoint_iff nhds_basis_ball
    |>.mp (hf x hx) with ⟨U, hUx, r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
⊢ Tendsto (fun (y : ι × X) ↦ (f⁻¹ y.2, F⁻¹ y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
have 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))ᶜ
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 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
⊢ ∀ᶠ (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))ᶜ
have 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))ᶜ
Tactic: filter_upwards [hF x hx (dist_mem_uniformity (half_pos hr₀)), tendsto_snd hUx] with y hy₁ hy₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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
⊢ (f y.2, F y.1 y.2) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ
have this : r ≤ ‖f y.2‖
Tactic: have : r ≤ ‖f y.2‖ := by simp_all [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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‖
have hy₃ : ‖f y.2 - F y.1 y.2‖ < r / 2
Tactic: simp [dist_eq_norm_sub] at hy₁
Cleared hypotheses: hy₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ r / 2 < ‖F y.1 y.2‖
have linarith : ‖F y.1 y.2‖ ≤ r / 2 → 2 / 2 = 1
Tactic: linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ r / 2 < ‖F y.1 y.2‖
have linarith₁ : ‖F y.1 y.2‖ ≤ r / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ r / 2 < ‖F y.1 y.2‖
have linarith₂ : ‖F y.1 y.2‖ ≤ r / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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
⊢ r / 2 < ‖F y.1 y.2‖
have 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
Tactic: linarith [hy₁, norm_sub_norm_le (f y.2) (F y.1 y.2)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
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) ∈ SProd.sprod (α := Set α) (β := Set α) (closedBall 0 (r / 2))ᶜ (closedBall 0 (r / 2))ᶜ
have this₁ : 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)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l
have rw : ∀ (hF : TendstoLocallyUniformlyOn F f l Set.univ) (hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)),
  TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ
Tactic: rw [← tendstoLocallyUniformlyOn_univ] at *
Cleared hypotheses: hF, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
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)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ
have apply : ∀ (x : X), Membership.mem (γ := Set X) Set.univ x → Disjoint (map f (𝓝[Set.univ] x)) (𝓝 0)
Tactic: apply hF.inv₀_of_disjoint
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x
have refine_1 : Membership.mem (γ := Filter α) (𝓝 0) (closedBall x (‖x‖ / 2))ᶜ
Tactic: refine uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
refine_1 : Membership.mem (γ := Filter α) (𝓝 0) (closedBall x (‖x‖ / 2))ᶜ
⊢ ContinuousAt Inv.inv x
have refine_2 : closedBall x (‖x‖ / 2) ∈ 𝓝 x
Tactic: refine uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ Membership.mem (γ := Filter α) (𝓝 0) (closedBall x (‖x‖ / 2))ᶜ
have refine_1 : 0 ∈ (closedBall x (‖x‖ / 2))ᶜ
Tactic: refine Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x
have refine_2 : 0 < ‖x‖ / 2
Tactic: apply Metric.closedBall_mem_nhds
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
s : Set X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ContinuousOn f s
hg : ContinuousOn g s
hg₀ : ∀ x ∈ s, g x ≠ 0
⊢ TendstoLocallyUniformlyOn (F / G) (f / g) l s
have simp : TendstoLocallyUniformlyOn (F * G⁻¹) (f * g⁻¹) l s
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst_1 : TopologicalSpace X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hg₀ : ∀ (x : X), g x ≠ 0
⊢ TendstoLocallyUniformly (F / G) (f / g) l
have simp : TendstoLocallyUniformly (F * G⁻¹) (f * g⁻¹) l
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : m < 0
⊢ Tendsto (fun (x : α) ↦ x ^ m) (𝓝[≠] 0) (cobounded α)
have obtain : ∀ (m : ℤ) (hm : -m < 0), Tendsto (fun (x : α) ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)
Tactic: obtain ⟨m, rfl⟩ := neg_surjective m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ Tendsto (fun (x : α) ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)
have lift : ∀ (m : ℕ) (hm : LT.lt (α := ℤ) (-(↑m : ℤ)) 0),
  Tendsto (fun (x : α) ↦ HPow.hPow (β := ℤ) x (-(↑m : ℤ))) (𝓝[≠] 0) (cobounded α)
Tactic: lift m to ℕ using by lia
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
⊢ DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
have pos : ∀ (H : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1),
  DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
Tactic: by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
pos :
  ∀ (H : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1),
    DiscreteTopology 𝕜 ∨
      Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
⊢ DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
have neg : ∀ (H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1),
  DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
Tactic: by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
have neg : (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨
  Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
Tactic: simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
have neg : ∀ (y : 𝕜), ‖y‖ < 1 → y = 0
Tactic: refine Or.inl ⟨1, zero_lt_one, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∀ (y : 𝕜), ‖y‖ < 1 → y = 0
have neg : ∀ (H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0), ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0
⊢ ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
have neg : ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1
Tactic: refine H.imp ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
inst : NormedField 𝕜
h : BddAbove (α := ℝ) (Set.range fun (k : 𝕜) ↦ ‖k‖)
⊢ DiscreteTopology 𝕜
have refine : ¬Nonempty.{u_4 + 1} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = inst }
Tactic: refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
h : BddAbove (α := ℝ) (Set.range fun (k : 𝕜) ↦ ‖k‖)
⊢ False
have obtain : ∀ (x : ℝ) (h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x), False
Tactic: obtain ⟨x, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
x : ℝ
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x
⊢ False
have obtain : ∀ (k : 𝕜) (hk : x < ‖k‖), False
Tactic: obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n
have refine : ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x → x ≠ 0 ∨ 0 ≤ n
Tactic: refine ⟨?_, continuousAt_zpow₀ _ _⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x → x ≠ 0 ∨ 0 ≤ n
have contrapose! : x = 0 ∧ n < 0 → ¬ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < (↑q : ℝ) ∧ (↑q : ℝ) < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂
have rwa : r₁ < norm (E := ℝ) (↑q : ℝ) ∧ norm (E := ℝ) (↑q : ℝ) < r₂
Tactic: rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < (↑q : ℝ) ∧ (↑q : ℝ) < r₂
rwa : r₁ < norm (E := ℝ) (↑q : ℝ) ∧ norm (E := ℝ) (↑q : ℝ) < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂
have rwa₁ : r₁ < |(↑q : ℝ)| ∧ |(↑q : ℝ)| < r₂
Tactic: rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
inst : NormedField K
⊢ CompleteSpace K ↔ IsComplete.{u_4} (α := K) (closedBall 0 1)
have mp : CompleteSpace K → IsComplete.{u_4} (α := K) (closedBall 0 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
inst : NormedField K
mp : CompleteSpace K → IsComplete.{u_4} (α := K) (closedBall 0 1)
⊢ CompleteSpace K ↔ IsComplete.{u_4} (α := K) (closedBall 0 1)
have mpr : IsComplete.{u_4} (α := K) (closedBall 0 1) → CompleteSpace K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
inst : NormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
⊢ CompleteSpace K
have mpr : DiscreteTopology K → CompleteSpace K
Tactic: rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
K : Type u_4
inst : NormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
mpr : DiscreteTopology K → CompleteSpace K
⊢ CompleteSpace K
have mpr₁ : ∀ (val : NontriviallyNormedField K) (h : IsComplete.{u_4} (α := K) (closedBall 0 1)), CompleteSpace K
Tactic: rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩
Cleared hypotheses: inst, h