awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hVS : ¬Absorbs 𝕜 (id V) S
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
x : ι → (↑S : Type u_3)
hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • (↑(x x_1) : E) ∉ V
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ε x_3 • (↑(x x_3) : E) ∉ V) x_2} x_1 →
          Membership.mem (γ := Set ι)
            {x_2 : ι |
              Membership.mem (γ := Set ι)
                  {x_3 : ι | (fun (x_4 : ι) ↦ (ε • Subtype.val (p := fun (x : E) ↦ x ∈ S) ∘ x) x_4 ∈ V) x_3} x_2 →
                Membership.mem (γ := Set ι) {x : ι | (fun (x : ι) ↦ False) x} x_2}
            x_1}
      a
h₁ : ∀ (a : ι), ε a • (↑(x a) : E) ∉ V → (ε • Subtype.val (p := fun (x : E) ↦ x ∈ S) ∘ x) a ∈ V → False
⊢ ∀ᶠ (x : ι) in l, False

Tactic:
filter_upwards [hx,
    (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id

Premises used: Iff.mpr, Function.comp, id, Filter.Tendsto.eventually, Filter.eventually_mem_set, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : Tendsto ε l (𝓝[≠] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0

Tactic:
hε self_mem_nhdsWithin

Premises used: Set.Mem, Filter.Eventually, setOf, self_mem_nhdsWithin, Set.preimage, Set.singleton, Not
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst_5 : l.NeBot
hε : Tendsto ε l (𝓝[≠] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0

Tactic:
exact hε self_mem_nhdsWithin

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ ∃ (ε : ℕ → 𝕜), Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0

Tactic:
simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))

Premises used: tendsto_nhdsWithin_iff, Compl.compl, nhdsWithin, Filter.exists_seq_tendsto, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
obtain : ∀ (ε : ℕ → 𝕜) (hε : Tendsto ε atTop (𝓝 0)) (hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0), IsVonNBounded 𝕝 s
⊢ IsVonNBounded 𝕝 s

Tactic:
obtain ⟨ε, hε, hε₀⟩ : ∃ ε : ℕ → 𝕜, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ n in atTop, ε n ≠ 0 := by
    simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))

Premises used: Filter.atTop
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, Ne.{u_7 + 1} (α := 𝕝) ((fun (x : ℕ) ↦ HSMul.hSMul (β := 𝕝) (ε x) 1) n) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
refine :
  ∀ (x : ℕ → E) (hx : ∀ (n : ℕ), x n ∈ s),
    Tendsto (HSMul.hSMul.{u_7, u_6, u_6} (α := ℕ → 𝕝) (fun (x : ℕ) ↦ HSMul.hSMul (β := 𝕝) (ε x) 1) x) atTop (𝓝 0)
⊢ IsVonNBounded 𝕝 s

Tactic:
refine isVonNBounded_of_smul_tendsto_zero (ε := (ε · • 1)) (by simpa) fun x hx ↦ ?_

Premises used: Bornology.isVonNBounded_of_smul_tendsto_zero
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ s
⊢ Tendsto (ε • x) atTop (𝓝 0)

Tactic:
have := h.smul_tendsto_zero (.of_forall hx) hε
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_6
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
𝕝 : Type u_7
inst_3 : NontriviallyNormedField 𝕝
inst_4 : NormedAlgebra 𝕜 𝕝
inst_5 : Module 𝕝 E
inst_6 : TopologicalSpace E
inst_7 : ContinuousSMul 𝕝 E
inst_8 : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ s
this : Tendsto (ε • x) atTop (𝓝 0)
⊢ Tendsto (HSMul.hSMul.{u_7, u_6, u_6} (α := ℕ → 𝕝) (fun (x : ℕ) ↦ HSMul.hSMul (β := 𝕝) (ε x) 1) x) atTop (𝓝 0)

Tactic:
simpa only [Pi.smul_def', smul_one_smul]

Premises used: smul_one_smul, Pi.smul_def'
-- 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 : T1Space E
inst_5 : RegularSpace E
inst_6 : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
rcases :
  ∀ (W : Set E) (hW₁ : Membership.mem (γ := Filter E) (𝓝 0) W) (hW₂ : IsClosed[inst_3] W) (hW₃ : W ⊆ V),
    Absorbs 𝕜 V (closure[inst_3] a)
⊢ Absorbs 𝕜 V (closure[inst_3] a)

Tactic:
rcases exists_mem_nhds_isClosed_subset hV with ⟨W, hW₁, hW₂, hW₃⟩

Premises used: exists_mem_nhds_isClosed_subset
-- 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 : T1Space E
inst_5 : RegularSpace E
inst_6 : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
W : Set E
hW₁ : Membership.mem (γ := Filter E) (𝓝 0) W
hW₂ : IsClosed[inst_3] W
hW₃ : W ⊆ V
⊢ Absorbs 𝕜 W a

Tactic:
specialize ha hW₁
-- 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 : T1Space E
inst_5 : RegularSpace E
inst_6 : ContinuousConstSMul 𝕜 E
a V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
W : Set E
hW₁ : Membership.mem (γ := Filter E) (𝓝 0) W
hW₂ : IsClosed[inst_3] W
hW₃ : W ⊆ V
ha : Absorbs 𝕜 W a
h : ∀ (b : 𝕜) (ha' : a ⊆ b • W), closure[inst_3] a ⊆ b • V
⊢ Absorbs 𝕜 V (closure[inst_3] a)

Tactic:
filter_upwards [ha] with b ha'
-- 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 : T1Space E
inst_5 : RegularSpace E
inst_6 : ContinuousConstSMul 𝕜 E
a V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
W : Set E
hW₁ : Membership.mem (γ := Filter E) (𝓝 0) W
hW₂ : IsClosed[inst_3] W
hW₃ : W ⊆ V
ha : Absorbs 𝕜 W a
b : 𝕜
ha' : a ⊆ b • W
h : closure[inst_3] (b • W) ⊆ b • V
h₁ : b • closure[inst_3] W ⊆ b • V
h₂ : b • W ⊆ b • V
h₃ h₄ : b • V ⊆ b • V
⊢ closure[inst_3] a ⊆ b • V

Tactic:
grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]

Premises used: Iff.mpr, closure_subset_iff_isClosed, closure_smul₀
-- 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 : ContinuousSMul 𝕜 E
x : E
⊢ IsVonNBounded 𝕜 (E := E) {x}

Tactic:
fun _ hV =>
  (absorbent_nhds_zero hV).absorbs

Premises used: Absorbent.absorbs, Bornology.IsVonNBounded, absorbent_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 : ContinuousSMul 𝕜 E
x : E
s : Set E
⊢ IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Tactic:
simp only [← singleton_union, isVonNBounded_union, isVonNBounded_singleton, true_and]

Premises used: Set.singleton_union, Bornology.isVonNBounded_union, Bornology.isVonNBounded_singleton, true_and
-- 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 : ContinuousSMul 𝕜 E
s : Set E
hs : s.Finite
⊢ IsVonNBounded 𝕜 s

Tactic:
fun _ hV ↦
  (absorbent_nhds_zero hV).absorbs_finite hs

Premises used: Bornology.IsVonNBounded, absorbent_nhds_zero, Absorbent.absorbs_finite
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
rw : IsVonNBounded 𝕜 (HVAdd.hVAdd (α := Set E) {x} s)
⊢ IsVonNBounded 𝕜 (x +ᵥ s)

Tactic:
rw [← singleton_vadd]

Premises used: Set.singleton_vadd
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (HVAdd.hVAdd (α := Set E) {x} s)

Tactic:
IsVonNBounded.add (isVonNBounded_singleton x) hs

Premises used: Bornology.IsVonNBounded.add, Bornology.isVonNBounded_singleton
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
hs : IsVonNBounded 𝕜 s
x : E
⊢ IsVonNBounded 𝕜 (HVAdd.hVAdd (α := Set E) {x} s)

Tactic:
exact IsVonNBounded.add (isVonNBounded_singleton x) hs

Premises used: Bornology.IsVonNBounded.add, Bornology.isVonNBounded_singleton
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
x : E
h : IsVonNBounded 𝕜 (x +ᵥ s)
⊢ IsVonNBounded 𝕜 s

Tactic:
simpa using h.vadd (-x)

Premises used: Bornology.IsVonNBounded.vadd, Neg.neg
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hst : IsVonNBounded 𝕜 (s + t)
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 t

Tactic:
let ⟨x, hx⟩ := hs
  (isVonNBounded_vadd x).mp <| hst.subset <| image_subset_image2_right hx

Premises used: Bornology.IsVonNBounded, Bornology.IsVonNBounded.subset, _private.0.Bornology.IsVonNBounded.of_add_right.match_1, Set.image_subset_image2_right, Iff.mp, Bornology.isVonNBounded_vadd
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hst : IsVonNBounded 𝕜 (s + t)
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 s

Tactic:
((add_comm s t).subst hst).of_add_right ht

Premises used: Bornology.IsVonNBounded.of_add_right, Eq.subst, add_comm
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
⟨fun h ↦ ⟨h.of_add_left ht, h.of_add_right hs⟩, and_imp.2 IsVonNBounded.add⟩

Premises used: Iff.mpr, Bornology.IsVonNBounded.of_add_right, and_imp, Bornology.IsVonNBounded.of_add_left, And.intro, Bornology.IsVonNBounded.add, Iff.intro
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
inl :
  IsVonNBounded 𝕜 (∅ + t) ↔
    Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ t = ∅ ∨ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅ ∧ IsVonNBounded 𝕜 t
inr : ∀ (hs : s.Nonempty), IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔
    Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ t = ∅ ∨ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅ ∧ IsVonNBounded 𝕜 t

Tactic:
simp
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : s.Nonempty
inr :
  IsVonNBounded 𝕜 (s + ∅) ↔
    s = ∅ ∨ Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅
inr₁ : ∀ (ht : t.Nonempty), IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔
    s = ∅ ∨ Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
simp
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [hs.ne_empty, ht.ne_empty, isVonNBounded_add_of_nonempty hs ht]

Premises used: Bornology.isVonNBounded_add_of_nonempty, Set.Nonempty.ne_empty
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
inl : IsVonNBounded 𝕜 (HAdd.hAdd (α := Set E) ∅ ∅) ↔ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅
inr : ∀ (hs : s.Nonempty), IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
⊢ IsVonNBounded 𝕜 (HAdd.hAdd (α := Set E) ∅ ∅) ↔ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
simp [isVonNBounded_add_of_nonempty, *]

Premises used: Bornology.isVonNBounded_add_of_nonempty
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
simp [isVonNBounded_add_of_nonempty, *]

Premises used: Bornology.isVonNBounded_add_of_nonempty
-- 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 : ContinuousSMul 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hst : IsVonNBounded 𝕜 (s - t)
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 s

Tactic:
((sub_eq_add_neg s t).subst hst).of_add_left ht.neg

Premises used: sub_eq_add_neg, Eq.subst, Set.Nonempty.neg, Bornology.IsVonNBounded.of_add_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 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : IsTopologicalAddGroup E
s t : Set E
hst : IsVonNBounded 𝕜 (s - t)
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 t

Tactic:
(((sub_eq_add_neg s t).subst hst).of_add_right hs).of_neg

Premises used: Bornology.IsVonNBounded.of_neg, Bornology.IsVonNBounded.of_add_right, sub_eq_add_neg, Eq.subst
-- 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 : ContinuousSMul 𝕜 E
inst_5 : IsTopologicalAddGroup E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [sub_eq_add_neg, isVonNBounded_add_of_nonempty, hs, ht]

Premises used: Bornology.isVonNBounded_add_of_nonempty, sub_eq_add_neg
-- 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 : ContinuousSMul 𝕜 E
inst_5 : IsTopologicalAddGroup E
s t : Set E
⊢ IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [sub_eq_add_neg, isVonNBounded_add]

Premises used: sub_eq_add_neg, Bornology.isVonNBounded_add
-- 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 : ContinuousSMul 𝕜 E
⊢ Eq.{u_3 + 1} (α := Set E) (⋃₀ setOf (IsVonNBounded 𝕜)) univ

Tactic:
Set.eq_univ_iff_forall.mpr fun x =>
    Set.mem_sUnion.mpr ⟨{x}, isVonNBounded_singleton _, Set.mem_singleton _⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.eq_univ_iff_forall, And.intro, Exists.intro, Set.mem_sUnion, Singleton.singleton, Bornology.isVonNBounded_singleton
-- 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 : ContinuousSMul 𝕜 E
s : Set E
⊢ IsBounded s ↔ IsVonNBounded 𝕜 s

Tactic:
isBounded_ofBounded_iff _

Premises used: Bornology.IsVonNBounded, Set.Mem, setOf, Bornology.isBounded_ofBounded_iff
-- 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 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h }
⊢ ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs

Premises used: 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 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
hs : TotallyBounded s
h : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h }
hs₁ : ∀ (U : Set E), Membership.mem (γ := Filter E) (𝓝 0) U → ∃ (t : Set E), t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs

Premises used: 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 : 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 : ∃ (x : 𝕜), 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := h }
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Tendsto (β := E) (fun (x : E × E) ↦ x.1 + x.2) (𝓝 0) (𝓝 0)

Tactic:
have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)
-- 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)
⊢ (SProd.sprod (α := Filter E) (β := Filter E) (𝓝 0) (𝓝 0)).HasBasis
    (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) ↦ id i.1 ×ˢ id i.2

Tactic:
have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
-- 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' :
  (SProd.sprod (α := Filter E) (β := Filter E) (𝓝 0) (𝓝 0)).HasBasis
    (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) ↦ id i.1 ×ˢ id i.2
⊢ 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

Tactic:
simp_rw [← nhds_prod_eq, id] at h'

Premises used: id, nhds_prod_eq