awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_

Premises used: UniformContinuousOn.continuousOn, uniformContinuousOn_inv₀, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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))ᶜ
refine_2 : closedBall x (‖x‖ / 2) ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x

Tactic:
refine uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_

Premises used: UniformContinuousOn.continuousOn, uniformContinuousOn_inv₀, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ Membership.mem (γ := Filter α) (𝓝 0) (closedBall x (‖x‖ / 2))ᶜ

Tactic:
Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
refine_1 : 0 ∈ (closedBall x (‖x‖ / 2))ᶜ
⊢ Membership.mem (γ := Filter α) (𝓝 0) (closedBall x (‖x‖ / 2))ᶜ

Tactic:
refine Metric.isClosed_closedBall.isOpen_compl.mem_nhds ?_

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ 0 ∈ (closedBall x (‖x‖ / 2))ᶜ

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
refine_2 : 0 < ‖x‖ / 2
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x

Tactic:
apply Metric.closedBall_mem_nhds

Premises used: Metric.closedBall_mem_nhds
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ 0 < ‖x‖ / 2

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 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
simp : TendstoLocallyUniformlyOn (F * G⁻¹) (f * g⁻¹) l s
⊢ TendstoLocallyUniformlyOn (F / G) (f / g) l s

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_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 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

Tactic:
hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

Premises used: TendstoLocallyUniformlyOn.inv₀, ContinuousOn.inv₀, TendstoLocallyUniformlyOn.mul₀
-- 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 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

Tactic:
exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

Premises used: TendstoLocallyUniformlyOn.inv₀, ContinuousOn.inv₀, TendstoLocallyUniformlyOn.mul₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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
simp : TendstoLocallyUniformly (F * G⁻¹) (f * g⁻¹) l
⊢ TendstoLocallyUniformly (F / G) (f / g) l

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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

Tactic:
hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

Premises used: TendstoLocallyUniformly.inv₀, TendstoLocallyUniformly.mul₀, Continuous.inv₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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

Tactic:
exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

Premises used: TendstoLocallyUniformly.inv₀, TendstoLocallyUniformly.mul₀, Continuous.inv₀
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop

Tactic:
tendsto_norm_cobounded_atTop.comp tendsto_inv₀_nhdsNE_zero

Premises used: tendsto_norm_cobounded_atTop, Filter.Tendsto.comp, Filter.tendsto_inv₀_nhdsNE_zero
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : m < 0
obtain : ∀ (m : ℤ) (hm : -m < 0), Tendsto (fun (x : α) ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)
⊢ Tendsto (fun (x : α) ↦ x ^ m) (𝓝[≠] 0) (cobounded α)

Tactic:
obtain ⟨m, rfl⟩ := neg_surjective m

Premises used: neg_surjective, rfl
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ 0 ≤ m

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : -m < 0
lift :
  ∀ (m : ℕ) (hm : LT.lt (α := ℤ) (-(↑m : ℤ)) 0),
    Tendsto (fun (x : α) ↦ HPow.hPow (β := ℤ) x (-(↑m : ℤ))) (𝓝[≠] 0) (cobounded α)
⊢ Tendsto (fun (x : α) ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)

Tactic:
lift m to ℕ using by lia
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℕ
hm : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
⊢ m ≠ 0

Tactic:
lia
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℕ
hm : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
⊢ Tendsto (fun (x : α) ↦ HPow.hPow (β := ℤ) x (-(↑m : ℤ))) (𝓝[≠] 0) (cobounded α)

Tactic:
simpa [Function.comp_def] using
    (tendsto_pow_cobounded_cobounded (by lia)).comp tendsto_inv₀_nhdsNE_zero

Premises used: Function.comp_def, Filter.Tendsto.comp, Filter.tendsto_inv₀_nhdsNE_zero, tendsto_pow_cobounded_cobounded
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : NormedDivisionRing α
m : ℤ
hm : m < 0
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop

Tactic:
tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_cobounded hm)

Premises used: tendsto_zpow_nhdsNE_zero_cobounded, tendsto_norm_cobounded_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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 }
neg :
  ∀ (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 }

Tactic:
by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }

Tactic:
Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩

Premises used: Nonempty.intro, Subtype.mk, NontriviallyNormedField.ofNormNeOne, Or.inr, rfl
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }

Tactic:
exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩

Premises used: Or.inr
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
neg :
  (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }
⊢ DiscreteTopology 𝕜 ∨
    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]

Premises used: dist_eq_norm, sub_zero, discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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 }

Tactic:
Or.inl ⟨1, zero_lt_one, ?_⟩

Premises used: zero_lt_one, And.intro, Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
neg : ∀ (y : 𝕜), ‖y‖ < 1 → y = 0
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨
    Nonempty.{max 1 (u_4 + 1)} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = h }

Tactic:
refine Or.inl ⟨1, zero_lt_one, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
neg : ∀ (H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0), ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∀ (y : 𝕜), ‖y‖ < 1 → y = 0

Tactic:
contrapose! H
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0
⊢ ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1

Tactic:
H.imp ?_

Premises used: Exists.imp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0
neg : ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1
⊢ ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1

Tactic:
refine H.imp ?_

Premises used: Exists.imp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ (y : 𝕜), ‖y‖ < 1 ∧ y ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1

Tactic:
simp +contextual [ne_of_lt]

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NormedField 𝕜
h : BddAbove (α := ℝ) (Set.range fun (k : 𝕜) ↦ ‖k‖)
⊢ DiscreteTopology 𝕜

Tactic:
(NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_

Premises used: NormedField.discreteTopology_or_nontriviallyNormedField, Or.resolve_right
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NormedField 𝕜
h : BddAbove (α := ℝ) (Set.range fun (k : 𝕜) ↦ ‖k‖)
refine : ¬Nonempty.{u_4 + 1} { h' : NontriviallyNormedField 𝕜 // NontriviallyNormedField.toNormedField = inst }
⊢ DiscreteTopology 𝕜

Tactic:
refine (NormedField.discreteTopology_or_nontriviallyNormedField _).resolve_right ?_

Premises used: NormedField.discreteTopology_or_nontriviallyNormedField, Or.resolve_right
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
h : BddAbove (α := ℝ) (Set.range fun (k : 𝕜) ↦ ‖k‖)
obtain : ∀ (x : ℝ) (h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x), False
⊢ False

Tactic:
obtain ⟨x, h⟩ := h
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
x : ℝ
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x
obtain : ∀ (k : 𝕜) (hk : x < ‖k‖), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ := NormedField.exists_lt_norm 𝕜 x

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
x : ℝ
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x
k : 𝕜
hk : x < ‖k‖
⊢ False

Tactic:
hk.not_ge (h (Set.mem_range_self k))

Premises used: Set.mem_range_self, LT.lt.not_ge
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
val : NontriviallyNormedField 𝕜
x : ℝ
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (k : 𝕜) ↦ ‖k‖)) x
k : 𝕜
hk : x < ‖k‖
⊢ False

Tactic:
exact hk.not_ge (h (Set.mem_range_self k))

Premises used: Set.mem_range_self, LT.lt.not_ge
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
inst : DenselyNormedField α
⊢ DenseRange.{0, u_1} (α := α) nnnorm

Tactic:
dense_of_exists_between fun _ _ hr =>
    let ⟨x, h⟩ := exists_lt_nnnorm_lt α hr
    ⟨‖x‖₊, ⟨x, rfl⟩, h⟩

Premises used: NormedField.exists_lt_nnnorm_lt, NNNorm.nnnorm, Membership.mem, Exists, And, And.intro, Exists.intro, DenseRange, Set.range, _private.0.NormedField.denseRange_nnnorm.match_1, Set.Ioo, dense_of_exists_between, rfl
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
⟨?_, continuousAt_zpow₀ _ _⟩

Premises used: continuousAt_zpow₀, Iff.intro
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
refine : ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x → x ≠ 0 ∨ 0 ≤ n
⊢ ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
refine ⟨?_, continuousAt_zpow₀ _ _⟩
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
contrapose! : x = 0 ∧ n < 0 → ¬ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x
⊢ ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) x → x ≠ 0 ∨ 0 ≤ n

Tactic:
contrapose!
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) 0
⊢ False

Tactic:
(hc.tendsto.mono_left nhdsWithin_le_nhds).not_tendsto (Metric.disjoint_nhds_cobounded _)
    (tendsto_zpow_nhdsNE_zero_cobounded hm)

Premises used: tendsto_zpow_nhdsNE_zero_cobounded, Metric.disjoint_nhds_cobounded, Filter.Tendsto.not_tendsto, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
n : ℤ
hm : n < 0
hc : ContinuousAt (Y := 𝕜) (fun (x : 𝕜) ↦ x ^ n) 0
⊢ False

Tactic:
exact (hc.tendsto.mono_left nhdsWithin_le_nhds).not_tendsto (Metric.disjoint_nhds_cobounded _)
    (tendsto_zpow_nhdsNE_zero_cobounded hm)

Premises used: tendsto_zpow_nhdsNE_zero_cobounded, Metric.disjoint_nhds_cobounded, Filter.Tendsto.not_tendsto, nhdsWithin_le_nhds, ContinuousAt.tendsto, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ x ≠ 0

Tactic:
simpa using NormedField.continuousAt_zpow (n := -1) (x := x)

Premises used: NormedField.continuousAt_zpow
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
a b : ℚ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp only [norm, Rat.cast_mul, abs_mul]

Premises used: Norm.norm, Rat.cast_mul, abs_mul
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
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₂
rwa₁ : r₁ < |(↑q : ℝ)| ∧ |(↑q : ℝ)| < r₂
rwa₂ rwa₃ rwa₄ rwa₅ : r₁ < (↑q : ℝ) ∧ (↑q : ℝ) < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂

Tactic:
rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]

Premises used: Rat.norm_cast_real, And.left, abs_of_pos, LE.le.trans_lt, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
inst : NormedField K
mp : CompleteSpace K → IsComplete.{u_4} (α := K) (closedBall 0 1)
mpr : IsComplete.{u_4} (α := K) (closedBall 0 1) → CompleteSpace K
⊢ CompleteSpace K ↔ IsComplete.{u_4} (α := K) (closedBall 0 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
inst : NormedField K
h : CompleteSpace K
⊢ IsComplete.{u_4} (α := K) (closedBall 0 1)

Tactic:
Metric.isClosed_closedBall.isComplete

Premises used: Metric.isClosed_closedBall, IsClosed.isComplete
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
inst : NormedField K
h : CompleteSpace K
⊢ IsComplete.{u_4} (α := K) (closedBall 0 1)

Tactic:
exact Metric.isClosed_closedBall.isComplete

Premises used: Metric.isClosed_closedBall, IsClosed.isComplete
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
inst : NormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
mpr : DiscreteTopology K → CompleteSpace K
mpr₁ : ∀ (val : NontriviallyNormedField K) (h : IsComplete.{u_4} (α := K) (closedBall 0 1)), CompleteSpace K
⊢ CompleteSpace K

Tactic:
rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _ | ⟨_, rfl⟩

Premises used: NormedField.discreteTopology_or_nontriviallyNormedField, rfl
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
inst : NormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
h_1 : DiscreteTopology K
mpr : IsComplete.{u_4} (α := K) Set.univ
mpr₁ mpr₂ mpr₃ mpr₄ : IsComplete.{u_4} (α := K) (closedBall 0 1)
⊢ CompleteSpace K

Tactic:
rwa [completeSpace_iff_isComplete_univ,
         ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]

Premises used: completeSpace_iff_isComplete_univ, NormedDivisionRing.unitClosedBall_eq_univ_of_discrete
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
⊢ CompleteSpace K

Tactic:
Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
mpr : ∀ (u : ℕ → K) (hu : CauchySeq u), ∃ (a : K), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace K

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
mpr :
  ∀ (k : ℝ) (hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k),
    ∃ (a : K), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨k, hk⟩ := hu.norm_bddAbove

Premises used: CauchySeq.norm_bddAbove
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖) ‖u 0‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
⊢ 0 ≤ k

Tactic:
have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
mpr : ∀ (x : K) (hx : k < ‖x‖), ∃ (a : K), Tendsto u atTop (𝓝 a)
⊢ ∃ (a : K), Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k

Premises used: NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
⊢ CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)

Tactic:
have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
n : ℕ
simp : ‖u n‖ / ‖x‖ ≤ 1
⊢ Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)

Tactic:
simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]

Premises used: norm_div, Function.comp_apply, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
n : ℕ
rw : ‖u n‖ ≤ ‖x‖
⊢ ‖u n‖ / ‖x‖ ≤ 1

Tactic:
rw [div_le_one (kpos.trans_lt hx)]

Premises used: div_le_one, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
n : ℕ
⊢ Membership.mem (γ := Set ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖) ‖u n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
n : ℕ
⊢ ‖u n‖ ≤ ‖x‖

Tactic:
exact hx.le.trans' (hk (by simp))

Premises used: LT.lt.le, LE.le.trans'
-- Module: Mathlib.Analysis.Normed.Field.Lemmas
Goal:
K : Type u_4
val : NontriviallyNormedField K
h : IsComplete.{u_4} (α := K) (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (n : ℕ) ↦ ‖u n‖)) k
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq (α := K) ((fun (x_1 : K) ↦ x_1 / x) ∘ u)
⊢ ∀ (n : ℕ), Membership.mem (γ := Set K) (closedBall 0 1) (((fun (x_1 : K) ↦ x_1 / x) ∘ u) n)

Tactic:
have hb : ∀ n, ((· / x) ∘ u) n ∈ Metric.closedBall 0 1 := by
    intro
    simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]
    rw [div_le_one (kpos.trans_lt hx)]
    exact hx.le.trans' (hk (by simp))