awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
rcases :
  ∀ (x : Set E × Set E)
    (hx :
      (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2)
    (h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U), Absorbs 𝕜 U s
⊢ Absorbs 𝕜 U s

Tactic:
rcases h.basis_left h' U hU with ⟨x, hx, h''⟩

Premises used: Filter.Tendsto.basis_left
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
rcases : ∀ (t : Set E) (ht : t.Finite) (hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2), Absorbs 𝕜 U s
⊢ Absorbs 𝕜 U s

Tactic:
rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩

Premises used: And.right, And.left, Prod.snd
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ Absorbs 𝕜 U s

Tactic:
Absorbs.mono_right ?_ hs

Premises used: Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
refine : Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)
⊢ Absorbs 𝕜 U s

Tactic:
refine Absorbs.mono_right ?_ hs

Premises used: Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
rw : ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)
⊢ Absorbs 𝕜 U (⋃ y ∈ t, y +ᵥ x.2)

Tactic:
rw [ht.absorbs_biUnion]

Premises used: Set.Finite.absorbs_biUnion
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
⊢ x.1 + x.2 ⊆ U

Tactic:
have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)

Tactic:
fun y _ => Absorbs.mono_left ?_ hx_fstsnd

Premises used: Absorbs.mono_left
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
refine : ∀ y ∈ t, Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)
⊢ ∀ i ∈ t, Absorbs 𝕜 U (i +ᵥ x.2)

Tactic:
refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd

Premises used: Absorbs.mono_left
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
y : E
h_2 : y ∈ t
⊢ Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)

Tactic:
(absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self

Premises used: absorbent_nhds_zero, Balanced.absorbs_self, And.right, And.left, Absorbent.vadd_absorbs
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs_1 : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h_1 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h_1 }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
h' :
  HasBasis (α := E × E) (𝓝 (0, 0))
    (fun (i : Set E × Set E) ↦
      (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter E) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2)
    fun (i : Set E × Set E) ↦ i.1 ×ˢ i.2
x : Set E × Set E
hx :
  (Membership.mem (γ := Filter E) (𝓝 0) x.1 ∧ Balanced 𝕜 x.1) ∧
    Membership.mem (γ := Filter E) (𝓝 0) x.2 ∧ Balanced 𝕜 x.2
h'' : MapsTo (fun (x : E × E) ↦ x.1 + x.2) (x.1 ×ˢ x.2) U
t : Set E
ht : t.Finite
hs : s ⊆ ⋃ y ∈ t, y +ᵥ x.2
hx_fstsnd : x.1 + x.2 ⊆ U
y : E
h_2 : y ∈ t
⊢ Absorbs 𝕜 (x.1 + x.2) (y +ᵥ x.2)

Tactic:
exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self

Premises used: absorbent_nhds_zero, Balanced.absorbs_self, And.right, And.left, Absorbent.vadd_absorbs
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ (x : 𝕜), 1 < ‖x‖
⊢ ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) univ x → ∀ ⦃y : 𝕜⦄, Membership.mem (γ := Set 𝕜) univ y → dist x y ≤ 1

Tactic:
simp_all [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ (x : 𝕜), 1 < ‖x‖
⊢ BoundedSpace 𝕜

Tactic:
haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ (x : 𝕜), 1 < ‖x‖
this : BoundedSpace 𝕜
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
Bornology.IsVonNBounded.of_boundedSpace

Premises used: Bornology.IsVonNBounded.of_boundedSpace
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ¬∃ (x : 𝕜), 1 < ‖x‖
this : BoundedSpace 𝕜
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact Bornology.IsVonNBounded.of_boundedSpace

Premises used: Bornology.IsVonNBounded.of_boundedSpace
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
if : ∀ (h : ∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
if₁ : ∀ (h : ¬∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
if₂ : ∀ (h : ∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
if₃ if₄ : ∀ (h : ¬∃ (x : 𝕜), 1 < ‖x‖), Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
if h : ∃ x : 𝕜, 1 < ‖x‖ then
    letI : NontriviallyNormedField 𝕜 := ⟨h⟩
    rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
    intro U hU
    have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)
    have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
    simp_rw [← nhds_prod_eq, id] at h'
    rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
    rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
    refine Absorbs.mono_right ?_ hs
    rw [ht.absorbs_biUnion]
    have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
    refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
    exact (absorbent_nhds_zero hx.1.1).vadd_absorbs hx.2.2.absorbs_self
  else
    haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
    exact Bornology.IsVonNBounded.of_boundedSpace

Premises used: id, nhds_prod_eq, Bornology.IsVonNBounded.of_boundedSpace, Absorbs.mono_right, totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : IsCompact s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace E
  haveI := isUniformAddGroup_of_addCommGroup (G := E)
  hs.totallyBounded.isVonNBounded 𝕜

Premises used: IsCompact.totallyBounded, TotallyBounded.isVonNBounded
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul 𝕜 E
f : ℕ → E
x : E
hf : Tendsto f atTop (𝓝 x)
⊢ Bornology.IsVonNBounded 𝕜 (range f)

Tactic:
letI := IsTopologicalAddGroup.rightUniformSpace E
  haveI := isUniformAddGroup_of_addCommGroup (G := E)
  hf.cauchySeq.totallyBounded_range.isVonNBounded 𝕜

Premises used: TotallyBounded.isVonNBounded, Filter.Tendsto.cauchySeq, CauchySeq.totallyBounded_range
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ Absorbs 𝕜 V s

Tactic:
(h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_

Premises used: AntilipschitzWith.tendsto_cobounded, Absorbs.restrict_scalars
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
refine : AntilipschitzWith.{u_1, u_2} (β := 𝕜') (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜') x 1
⊢ Absorbs 𝕜 V s

Tactic:
refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_

Premises used: AntilipschitzWith.tendsto_cobounded, Absorbs.restrict_scalars
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ AntilipschitzWith.{u_1, u_2} (β := 𝕜') (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜') x 1

Tactic:
AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_

Premises used: AntilipschitzWith.of_le_mul_nndist
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
refine :
  ∀ (x y : 𝕜),
    nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
⊢ AntilipschitzWith.{u_1, u_2} (β := 𝕜') (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ fun (x : 𝕜) ↦ HSMul.hSMul (β := 𝕜') x 1

Tactic:
refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_

Premises used: AntilipschitzWith.of_le_mul_nndist
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Nontrivial 𝕜'
inst_4 : Zero E
inst_5 : TopologicalSpace E
inst_6 : SMul 𝕜 E
inst_7 : MulAction 𝕜' E
inst_8 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
x y : 𝕜
rw : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)
rw₁ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') x 1 - HSMul.hSMul (β := 𝕜') y 1‖₊
rw₂ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * ‖HSMul.hSMul (β := 𝕜') (x - y) 1‖₊
rw₃ : ‖x - y‖₊ ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * (‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1)
rw₄ : ‖x - y‖₊ ≤ ‖x - y‖₊ * nnnorm.{u_2} (E := 𝕜') 1 / nnnorm.{u_2} (E := 𝕜') 1
rw₅ rw₆ : ‖x - y‖₊ ≤ ‖x - y‖₊
⊢ nndist x y ≤ (nnnorm.{u_2} (E := 𝕜') 1)⁻¹ * nndist (HSMul.hSMul (β := 𝕜') x 1) (HSMul.hSMul (β := 𝕜') y 1)

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]

Premises used: Iff.mpr, nnnorm_smul, nnnorm_ne_zero_iff, sub_smul, mul_div_cancel_right₀, nndist_eq_nnnorm, div_eq_inv_mul, one_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : NormedRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : Zero E
inst_4 : TopologicalSpace E
inst_5 : SMul 𝕜 E
inst_6 : MulActionWithZero 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
⊢ IsVonNBounded 𝕜 s

Tactic:
match subsingleton_or_nontrivial 𝕜' with
  | .inl _ =>
    have : Subsingleton E := MulActionWithZero.subsingleton 𝕜' E
    IsVonNBounded.of_subsingleton
  | .inr _ =>
    h.restrict_scalars_of_nontrivial _

Premises used: _private.0.Bornology.IsVonNBounded.restrict_scalars.match_1, Bornology.IsVonNBounded, Bornology.IsVonNBounded.restrict_scalars_of_nontrivial, MulActionWithZero.subsingleton, subsingleton_or_nontrivial, Bornology.IsVonNBounded.of_subsingleton
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
rcases : ∀ (r : ℝ) (hr : s ⊆ Metric.ball 0 r), Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
rcases h.subset_ball 0 with ⟨r, hr⟩

Premises used: Bornology.IsBounded.subset_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
rw : ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
rw [Metric.nhds_basis_ball.isVonNBounded_iff]

Premises used: Filter.HasBasis.isVonNBounded_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Metric.ball 0 r
rw :
  ∀ (hr : s ⊆ Seminorm.ball (normSeminorm 𝕜 E) 0 r) (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) s
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Metric.ball 0 i) s

Tactic:
rw [← ball_normSeminorm 𝕜 E] at hr ⊢

Premises used: ball_normSeminorm
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Seminorm.ball (normSeminorm 𝕜 E) 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) s

Tactic:
fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

Premises used: Seminorm.ball_zero_absorbs_ball_zero, normSeminorm, Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
r : ℝ
hr : s ⊆ Seminorm.ball (normSeminorm 𝕜 E) 0 r
⊢ ∀ (i : ℝ), 0 < i → Absorbs 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 i) s

Tactic:
exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

Premises used: Seminorm.ball_zero_absorbs_ball_zero, normSeminorm, Absorbs.mono_right
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Bornology.IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (Metric.ball 0 r)

Tactic:
isVonNBounded_of_isBounded _ Metric.isBounded_ball

Premises used: Metric.isBounded_ball, NormedSpace.isVonNBounded_of_isBounded