awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddZeroClass E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set E
hVo : IsOpen[inst_2] V
hV : 0 ∈ V
hVU : V + V ⊆ U
⊢ Absorbs 𝕜 U (s + t)

Tactic:
exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

Premises used: Absorbs.mono_left, Absorbs.add, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
rw : Absorbs 𝕜 (- -U) (-s)
⊢ Absorbs 𝕜 U (-s)

Tactic:
rw [← neg_neg U]

Premises used: neg_neg
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Absorbs 𝕜 (- -U) (-s)

Tactic:
(hs <| neg_mem_nhds_zero _ hU).neg_neg

Premises used: neg_mem_nhds_zero, Absorbs.neg_neg
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Absorbs 𝕜 (- -U) (-s)

Tactic:
exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

Premises used: neg_mem_nhds_zero, Absorbs.neg_neg
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s : Set E
⊢ IsVonNBounded 𝕜 (-s) ↔ IsVonNBounded 𝕜 s

Tactic:
⟨fun h ↦ neg_neg s ▸ h.neg, fun h ↦ h.neg⟩

Premises used: Bornology.IsVonNBounded.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
rw : IsVonNBounded 𝕜 (s + -t)
⊢ IsVonNBounded 𝕜 (s - t)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + -t)

Tactic:
hs.add ht.neg

Premises used: Bornology.IsVonNBounded.neg, Bornology.IsVonNBounded.add
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Premises used: Bornology.IsVonNBounded.neg, Bornology.IsVonNBounded.add
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t t' : TopologicalSpace E
h : t ≤ t'
s : Set E
hs : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 s

Tactic:
fun _ hV =>
  hs <| (le_iff_nhds t t').mp h 0 hV

Premises used: Bornology.IsVonNBounded, le_iff_nhds, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
rw : IsVonNBounded 𝕜 S ↔ ∀ (t : Set E), Membership.mem (γ := Filter E) (𝓝 0) t → ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t
⊢ IsVonNBounded 𝕜 S ↔ Tendsto.{u_6, u_7} (β := Set E) (fun (x : 𝕜) ↦ x • S) (𝓝 0) (smallSets (𝓝 0))

Tactic:
rw [tendsto_smallSets_iff]

Premises used: Filter.tendsto_smallSets_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ ∀ (t : Set E), Membership.mem (γ := Filter E) (𝓝 0) t → ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t

Tactic:
forall₂_congr fun V hV ↦ ?_

Premises used: Bornology.IsVonNBounded, forall₂_congr
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
refine : ∀ (V : Set E) (hV : Membership.mem (γ := Filter E) (𝓝 0) V), Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V
⊢ IsVonNBounded 𝕜 S ↔ ∀ (t : Set E), Membership.mem (γ := Filter E) (𝓝 0) t → ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t

Tactic:
refine forall₂_congr fun V hV ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V

Tactic:
simp only [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV), mapsTo_iff_image_subset,
    image_smul]

Premises used: Set.image_smul, Set.mapsTo_iff_image_subset, mem_of_mem_nhds, absorbs_iff_eventually_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ absorbing 𝕜 S ≤ 𝓝 0

Tactic:
.rfl

Premises used: Bornology.IsVonNBounded, Set.Mem, Filter.Eventually, Iff.rfl, setOf, Absorbs
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
rw :
  Eq.{u_7 + 1} (α := Filter 𝕜₂)
    (𝓝[range.{u_7, u_6 + 1} (ι := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂)] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₁ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝[univ] (σ : (a : 𝕜₁) → 𝕜₂) 0 : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₂ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝 ((σ : (a : 𝕜₁) → 𝕜₂) 0) : Filter 𝕜₂) (𝓝 0 : Filter 𝕜₂)
rw₃ rw₄ : Eq.{u_7 + 1} (α := Filter 𝕜₂) (𝓝 0) (𝓝 0)
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)

Tactic:
rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]

Premises used: nhdsWithin_univ, map_zero, RingHom.isometry, Isometry.isEmbedding, Function.Surjective.range_eq, RingHom.surjective, Topology.IsEmbedding.map_nhds_eq
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
⊢ Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)

Tactic:
have : map σ (𝓝 0) = 𝓝 0 := by
    rw [σ.isometry.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
⊢ Tendsto.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F) (𝓝 0) (𝓝 0)

Tactic:
have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
hs : IsVonNBounded 𝕜₁ s
f : E →SL[σ] F
this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
hf₀ : Tendsto.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F) (𝓝 0) (𝓝 0)
simp :
  ∀ (hs : Tendsto.{u_6, u_3} (β := Set E) (fun (x : 𝕜₁) ↦ x • s) (𝓝 0) (smallSets (𝓝 0))),
    Tendsto.{u_6, u_4} (α := 𝕜₁) (β := Set F)
      ((fun (x : 𝕜₂) ↦ HSMul.hSMul (β := Set F) x ((⇑f : (a : E) → F) '' s)) ∘ (⇑σ : (a : 𝕜₁) → 𝕜₂)) (𝓝 0)
      (smallSets (𝓝 0))
⊢ IsVonNBounded.{u_7, u_4} 𝕜₂ (E := F) ((⇑f : (a : E) → F) '' s)

Tactic:
simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢

Premises used: Bornology.isVonNBounded_iff_tendsto_smallSets_nhds, Filter.tendsto_map'_iff
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
E : Type u_3
F : Type u_4
𝕜₁ : Type u_6
𝕜₂ : Type u_7
inst : NormedDivisionRing 𝕜₁
inst_1 : NormedDivisionRing 𝕜₂
inst_2 : AddCommGroup E
inst_3 : Module 𝕜₁ E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
inst_6 : TopologicalSpace E
inst_7 : TopologicalSpace F
σ : 𝕜₁ →+* 𝕜₂
inst_8 : RingHomSurjective σ
inst_9 : RingHomIsometric σ
s : Set E
f : E →SL[σ] F
this : Eq.{u_7 + 1} (α := Filter 𝕜₂) (map.{u_6, u_7} (α := 𝕜₁) (⇑σ : (a : 𝕜₁) → 𝕜₂) (𝓝 0)) (𝓝 0)
hf₀ : Tendsto.{u_3, u_4} (α := E) (β := F) (⇑f : (a : E) → F) (𝓝 0) (𝓝 0)
hs : Tendsto.{u_6, u_3} (β := Set E) (fun (x : 𝕜₁) ↦ x • s) (𝓝 0) (smallSets (𝓝 0))
⊢ Tendsto.{u_6, u_4} (α := 𝕜₁) (β := Set F)
    ((fun (x : 𝕜₂) ↦ HSMul.hSMul (β := Set F) x ((⇑f : (a : E) → F) '' s)) ∘ (⇑σ : (a : 𝕜₁) → 𝕜₂)) (𝓝 0)
    (smallSets (𝓝 0))

Tactic:
simpa only [comp_def, image_smul_setₛₗ] using hf₀.image_smallSets.comp hs

Premises used: image_smul_setₛₗ, Filter.Tendsto.image_smallSets, Function.comp_def, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.LocallyConvex.Bounded
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
ε : ι → 𝕜
x : ι → E
l : Filter ι
hS : IsVonNBounded 𝕜 S
hxS : ∀ᶠ (n : ι) in l, x n ∈ S
hε : Tendsto ε l (𝓝 0)
⊢ Tendsto (ε • x) l (𝓝 0)

Tactic:
(hS.tendsto_smallSets_nhds.comp hε).of_smallSets <| hxS.mono fun _ ↦ smul_mem_smul_set

Premises used: Bornology.IsVonNBounded.tendsto_smallSets_nhds, Filter.Eventually.mono, Filter.Tendsto.of_smallSets, Filter.Tendsto.comp, Set.smul_mem_smul_set
-- 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)
rw : ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S
⊢ IsVonNBounded 𝕜 S

Tactic:
rw [(nhds_basis_balanced 𝕜 E).isVonNBounded_iff]

Premises used: nhds_basis_balanced, Filter.HasBasis.isVonNBounded_iff
-- 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)
by_contra! :
  ∀ (V : Set E) (hVS : ¬Absorbs 𝕜 (id V) S) (hV : Membership.mem (γ := Filter E) (𝓝 0) V) (hVb : Balanced 𝕜 V), False
⊢ ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S

Tactic:
by_contra! ⟨V, ⟨hV, hVb⟩, hVS⟩
-- 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
h : ∀ (n : ι) (hn : ε n ≠ 0), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
⊢ ∀ᶠ (n : ι) in l, ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
filter_upwards [hε] with n hn
-- 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
n : ι
hn : ε n ≠ 0
h :
  ∀ (hVS : ¬∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → S ⊆ c • id V) (hV : Membership.mem (γ := Filter E) (𝓝 0) V)
    (hVb : Balanced 𝕜 V) (n : ι) (hn : ε n ≠ 0), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
rw [absorbs_iff_norm] at hVS

Premises used: absorbs_iff_norm
-- 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 : ¬∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → S ⊆ c • id V
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
⊢ ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V

Tactic:
push Not at hVS

Premises used: 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ε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
h : ∀ (a : 𝕜) (haε : ‖(ε n)⁻¹‖ ≤ ‖a‖) (haS : ¬S ⊆ a • id V), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩

Premises used: Norm.norm, Inv.inv
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
h : ∀ (x : E) (hxS : x ∈ S) (hx : x ∉ a • id V), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩

Premises used: Set.not_subset, Iff.mp
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
⟨⟨x, hxS⟩, fun hnx => ?_⟩

Premises used: Subtype.mk, Exists.intro
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
h : ∀ (hnx : ε n • (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ V), False
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
hnx : ε n • (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ V
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ (ε n)⁻¹ • V

Tactic:
rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx

Premises used: Set.mem_inv_smul_set_iff₀
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
hnx : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ (ε n)⁻¹ • V
⊢ False

Tactic:
hx (hVb.smul_mono haε hnx)

Premises used: Balanced.smul_mono
-- 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
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
hnx : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ (ε n)⁻¹ • V
⊢ False

Tactic:
exact hx (hVb.smul_mono haε hnx)

Premises used: Balanced.smul_mono
-- 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
⊢ ∀ᶠ (n : ι) in l, ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V

Tactic:
have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V := by
    filter_upwards [hε] with n hn
    rw [absorbs_iff_norm] at hVS
    push Not at hVS
    rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩
    rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
    refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
    rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
    exact hx (hVb.smul_mono haε hnx)
-- 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
rcases : ∀ (x : ι → (↑S : Type u_3)) (hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • (↑(x x_1) : E) ∉ V), False
⊢ False

Tactic:
rcases this.choice with ⟨x, hx⟩

Premises used: Filter.Eventually.choice
-- 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
⊢ False

Tactic:
Filter.frequently_false l (Filter.Eventually.frequently ?_)

Premises used: Filter.frequently_false, Filter.Eventually.frequently
-- 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
refine : ∀ᶠ (x : ι) in l, False
⊢ False

Tactic:
refine Filter.frequently_false l (Filter.Eventually.frequently ?_)

Premises used: Filter.frequently_false, Filter.Eventually.frequently
-- 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
⊢ ∀ (a : ι), ε a • (↑(x a) : E) ∉ V → (ε • Subtype.val (p := fun (x : E) ↦ x ∈ S) ∘ x) a ∈ V → False

Tactic:
fun n => id

Premises used: Set.Mem, id, Not