awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
this : IsAddTorsionFree E
⊢ DiscreteTopology.{u_6} ↥⊥

Tactic:
exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))

Premises used: Subsingleton.discreteTopology
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
inr :
  ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' t) {0}
⊢ DiscreteTopology.{u_6} ↥(AddSubgroup.zmultiples e)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]

Premises used: discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' t) {0}

Tactic:
⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩

Premises used: Norm.norm, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
inr :
  Eq (α := Set ↥(AddSubgroup.zmultiples e))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
    {0}
⊢ ∃ (t : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' t) {0}

Tactic:
refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
inr :
  ∀ (x : E) (hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x),
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹'
          ball 0 ‖e‖)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx) ↔
      Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx)
⊢ Eq (α := Set ↥(AddSubgroup.zmultiples e))
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
    {0}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
E : Type u_6
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
x : E
hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x
inr :
  ∀ (k : ℤ) (hx : Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) (k • e)),
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹'
          ball 0 ‖e‖)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx) ↔
      Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) (k • e) hx)
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e))
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) ⁻¹' ball 0 ‖e‖)
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples e)) {0}
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := AddSubgroup E) (AddSubgroup.zmultiples e) x) x hx)

Tactic:
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx

Premises used: AddSubgroup.mem_zmultiples_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
apply : 2 * r ≤ diam (sphere x r)
⊢ diam (sphere x r) = 2 * r

Tactic:
apply le_antisymm
    (diam_mono sphere_subset_closedBall isBounded_closedBall |>.trans <| diam_closedBall hr)

Premises used: Metric.isBounded_closedBall, Metric.diam_mono, Metric.diam_closedBall, le_antisymm, Metric.sphere_subset_closedBall, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
obtain : ∀ (y : E) (hy : y ≠ 0), 2 * r ≤ diam (sphere x r)
⊢ 2 * r ≤ diam (sphere x r)

Tactic:
obtain ⟨y, hy⟩ := exists_ne (0 : E)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ 2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y)

Tactic:
simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]

Premises used: dist_eq_norm, norm_smul, smul_assoc, mul_assoc, abs_of_nonneg, two_nsmul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
hx : x + r • ‖y‖⁻¹ • y ∈ sphere x r
hy₁ : x - r • ‖y‖⁻¹ • y ∈ sphere x r
⊢ dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)

Tactic:
apply dist_le_diam_of_mem isBounded_sphere

Premises used: Metric.dist_le_diam_of_mem, Metric.isBounded_sphere
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x + r • ‖y‖⁻¹ • y ∈ sphere x r

Tactic:
simp [norm_smul, hy, abs_of_nonneg hr]

Premises used: norm_smul, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
⊢ x - r • ‖y‖⁻¹ • y ∈ sphere x r

Tactic:
simp [norm_smul, hy, abs_of_nonneg hr]

Premises used: norm_smul, abs_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : y ≠ 0
r₁ : 2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y)
r₂ : dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) ≤ diam (sphere x r)
⊢ 2 * r ≤ diam (sphere x r)

Tactic:
calc
    2 * r = dist (x + r • ‖y‖⁻¹ • y) (x - r • ‖y‖⁻¹ • y) := by
      simp [dist_eq_norm, ← two_nsmul, ← smul_assoc, norm_smul, abs_of_nonneg hr, hy, mul_assoc]
    _ ≤ diam (sphere x r) := by
      apply dist_le_diam_of_mem isBounded_sphere <;> simp [norm_smul, hy, abs_of_nonneg hr]

Premises used: Norm.norm, HSub.hSub, Inv.inv, HAdd.hAdd, HSMul.hSMul, Metric.diam, Dist.dist, Metric.sphere
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ diam (closedBall x r) = 2 * r

Tactic:
le_antisymm (diam_closedBall hr) <|
    diam_sphere_eq x hr |>.symm.le.trans <| diam_mono sphere_subset_closedBall isBounded_closedBall

Premises used: Metric.isBounded_closedBall, Metric.diam_mono, Eq.le, Metric.diam_closedBall, le_antisymm, Metric.diam_sphere_eq, Metric.sphere_subset_closedBall, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
refine : ∀ (a : ℝ) (ha : a ≥ 0) (ha' : a < 2) (r' : ℝ) (hr' : r' ≥ 0) (hr'' : r' < r), a * r' ≤ diam (ball x r)
⊢ diam (ball x r) = 2 * r

Tactic:
refine le_antisymm (diam_ball hr) <|
    mul_le_of_forall_lt_of_nonneg (by positivity) diam_nonneg fun a ha ha' r' hr' hr'' ↦ ?_

Premises used: Metric.diam_ball, Metric.diam_nonneg, le_antisymm, mul_le_of_forall_lt_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
ha₁ : 0 ≤ r'
⊢ a * r' ≤ 2 * r'

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
⊢ 2 * r' ≤ diam (ball x r)

Tactic:
simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball

Premises used: Metric.isBounded_ball, Metric.diam_mono, Metric.sphere_subset_ball, Metric.diam_sphere_eq, GE.ge.le
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
E : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
a : ℝ
ha : a ≥ 0
ha' : a < 2
r' : ℝ
hr' : r' ≥ 0
hr'' : r' < r
calc : a * r' ≤ 2 * r'
calc₁ : 2 * r' ≤ diam (ball x r)
⊢ a * r' ≤ diam (ball x r)

Tactic:
calc a * r' ≤ 2 * r' := by gcongr
    _ ≤ _ := by simpa only [← Metric.diam_sphere_eq x hr'.le]
      using diam_mono (sphere_subset_ball hr'') isBounded_ball
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
s : 𝕜
x : E × F
⊢ ‖s • x‖ ≤ ‖s‖ * ‖x‖

Tactic:
simp only [norm_smul, Prod.norm_def, le_rfl]

Premises used: le_rfl, norm_smul, Prod.norm_def
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst_5 : Fintype ι
inst_6 : (i : ι) → SeminormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
simp_rw :
  LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖(a • f) b‖₊)
    (Finset.sup Finset.univ fun (a_1 : ι) ↦ ‖a‖₊ * ‖f a_1‖₊)
⊢ ‖a • f‖ ≤ ‖a‖ * ‖f‖

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_mul, NNReal.coe_le_coe, Pi.nnnorm_def,
      NNReal.mul_finset_sup]

Premises used: NNReal.mul_finset_sup, coe_nnnorm, Pi.nnnorm_def, NNReal.coe_mul, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst_5 : Fintype ι
inst_6 : (i : ι) → SeminormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖(a • f) b‖₊)
    (Finset.sup Finset.univ fun (a_1 : ι) ↦ ‖a‖₊ * ‖f a_1‖₊)

Tactic:
Finset.sup_mono_fun fun _ _ => norm_smul_le a _

Premises used: norm_smul_le, Finset.sup_mono_fun
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F : Type u_4
α : Type u_5
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E_1
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E_1
inst_4 : NormedSpace 𝕜 F
ι : Type u_6
E : ι → Type u_7
inst_5 : Fintype ι
inst_6 : (i : ι) → SeminormedAddCommGroup (E i)
inst_7 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (E i)
a : 𝕜
f : (i : ι) → E i
⊢ LE.le (α := ℝ≥0) (Finset.sup Finset.univ fun (b : ι) ↦ ‖(a • f) b‖₊)
    (Finset.sup Finset.univ fun (a_1 : ι) ↦ ‖a‖₊ * ‖f a_1‖₊)

Tactic:
exact Finset.sup_mono_fun fun _ _ => norm_smul_le a _
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜_1 : Type u_1
𝕜' : Type u_2
E_1 : Type u_3
F_1 : Type u_4
α : Type u_5
F : Type u_6
𝕜 : Type u_7
E : Type u_8
G : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : FunLike F E G
inst_6 : LinearMapClass F 𝕜 E G
f : F
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.induced E G f
a : 𝕜
b : E
⊢ ‖a • b‖ ≤ ‖a‖ * ‖b‖

Tactic:
simpa only [← map_smul f a b] using norm_smul_le a (f b)

Premises used: norm_smul_le, DFunLike.coe, map_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
rcases : ∀ (x : E) (hx : x ≠ 0), ∃ (x : E), c < ‖x‖
⊢ ∃ (x : E), c < ‖x‖

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
rcases : ∀ (r : 𝕜) (hr : c / ‖x‖ < ‖r‖), ∃ (x : E), c < ‖x‖
⊢ ∃ (x : E), c < ‖x‖

Tactic:
rcases NormedField.exists_lt_norm 𝕜 (c / ‖x‖) with ⟨r, hr⟩

Premises used: Norm.norm, HDiv.hDiv, NormedField.exists_lt_norm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
h : c < ‖r • x‖
⊢ ∃ (x : E), c < ‖x‖

Tactic:
use r • x
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
h : 0 < ‖x‖
⊢ c < ‖r • x‖

Tactic:
rwa [norm_smul, ← div_lt_iff₀]

Premises used: norm_smul, div_lt_iff₀
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
h h₁ h₂ h₃ : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ ¬Bornology.IsBounded.{u_3} (α := E) univ

Tactic:
fun h =>
  let ⟨R, hR⟩ := isBounded_iff_forall_norm_le.1 h
  let ⟨x, hx⟩ := NormedSpace.exists_lt_norm 𝕜 E R
  hx.not_ge (hR x trivial)

Premises used: False, trivial, _private.0.NormedSpace.unbounded_univ.match_2, isBounded_iff_forall_norm_le, _private.0.NormedSpace.unbounded_univ.match_1, Iff.mp, LT.lt.not_ge, Not, NormedSpace.exists_lt_norm
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
rw : ¬Bornology.IsBounded.{u_3} (α := E) univ
⊢ (cobounded E).NeBot

Tactic:
rw [neBot_iff, Ne, cobounded_eq_bot_iff, ← isBounded_univ]

Premises used: Filter.neBot_iff, Ne, Bornology.cobounded_eq_bot_iff, Bornology.isBounded_univ
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ ¬Bornology.IsBounded.{u_3} (α := E) univ

Tactic:
NormedSpace.unbounded_univ 𝕜 E

Premises used: NormedSpace.unbounded_univ
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ ¬Bornology.IsBounded.{u_3} (α := E) univ

Tactic:
exact NormedSpace.unbounded_univ 𝕜 E

Premises used: NormedSpace.unbounded_univ
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ (cobounded 𝕜).NeBot

Tactic:
NormedSpace.cobounded_neBot 𝕜 𝕜

Premises used: NormedSpace.cobounded_neBot
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
inst_4 : NormedSpace ℝ E
⊢ (cobounded E).NeBot

Tactic:
NormedSpace.cobounded_neBot ℝ E

Premises used: Real, NormedSpace.cobounded_neBot
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
⊢ Infinite 𝕜

Tactic:
⟨fun _ ↦ NormedSpace.unbounded_univ 𝕜 𝕜 (Set.toFinite _).isBounded⟩

Premises used: Set.univ, Infinite.mk, Set.Finite.isBounded, Set.toFinite, NormedSpace.unbounded_univ
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
pos : ∀ (H : ∃ (c : 𝕜), c ≠ 0 ∧ ‖c‖ ≠ 1), NoncompactSpace E
neg : ∀ (H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1), NoncompactSpace E
⊢ NoncompactSpace E

Tactic:
by_cases! H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∃ (c : 𝕜), c ≠ 0 ∧ ‖c‖ ≠ 1
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.ofNormNeOne H
⊢ NoncompactSpace E

Tactic:
⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩

Premises used: IsCompact.isBounded, NormedSpace.unbounded_univ, NoncompactSpace.mk
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∃ (c : 𝕜), c ≠ 0 ∧ ‖c‖ ≠ 1
this : NontriviallyNormedField 𝕜 := NontriviallyNormedField.ofNormNeOne H
⊢ NoncompactSpace E

Tactic:
exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
neg : ∀ (x : E) (hx : x ≠ 0), NoncompactSpace E
⊢ NoncompactSpace E

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
neg :
  IsClosedEmbedding.{0, u_3} (Y := E) fun (x_1 : ℕ) ↦
    HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x
⊢ NoncompactSpace E

Tactic:
suffices IsClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
⊢ IsClosedEmbedding.{0, u_3} (Y := E) fun (x_1 : ℕ) ↦
    HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x

Tactic:
isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_

Premises used: Iff.mpr, norm_pos_iff, Metric.isClosedEmbedding_of_pairwise_le_dist
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
neg :
  ∀ (k n : ℕ) (hne : k ≠ n),
    (fun (x_1 y : ℕ) ↦
        ‖x‖ ≤
          dist (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x)
            (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) y : 𝕜) x))
      k n
⊢ IsClosedEmbedding.{0, u_3} (Y := E) fun (x_1 : ℕ) ↦
    HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) x_1 : 𝕜) x

Tactic:
refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_

Premises used: Iff.mpr, norm_pos_iff, Metric.isClosedEmbedding_of_pairwise_le_dist
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
neg :
  ‖x‖ ≤
    ‖HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
          ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)‖ *
      ‖x‖
⊢ ‖x‖ ≤
    dist (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜) x)
      (HSMul.hSMul (α := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜) x)

Tactic:
simp only [dist_eq_norm, ← sub_smul, norm_smul]

Premises used: dist_eq_norm, norm_smul, sub_smul
-- Module: Mathlib.Analysis.Normed.Module.Basic
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : Infinite 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : Nontrivial E
inst_4 : NormedSpace 𝕜 E
H : ∀ (c : 𝕜) (_ : c ≠ 0), ‖c‖ = 1
x : E
hx : x ≠ 0
k n : ℕ
hne : k ≠ n
neg :
  HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
      ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜) ≠
    0
⊢ ‖x‖ ≤
    ‖HSub.hSub (α := 𝕜) (β := 𝕜) ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) k : 𝕜)
          ((Infinite.natEmbedding 𝕜 : (a : ℕ) → 𝕜) n : 𝕜)‖ *
      ‖x‖

Tactic:
rw [H, one_mul]

Premises used: one_mul