-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_of_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot]
    (hε : ∀ᶠ n in l, ε n ≠ 0) {S : Set E}
    (H : ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)) : IsVonNBounded 𝕜 S

Proof state:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
⊢ ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V

Tactic:
filter_upwards [hε] with n hn

Result:
case h
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
⊢ ∃ x, ε n • ↑x ∉ V

Proof state:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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 : ↑⟨x, hxS⟩ ∈ (ε n)⁻¹ • V
⊢ False

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

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V
x : ι → ↑S
hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • ↑(x x_1) ∉ V
⊢ ∀ᶠ (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

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V
⊢ False

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

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
this : ∀ᶠ (n : ι) in l, ∃ x, ε n • ↑x ∉ V
x : ι → ↑S
hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • ↑(x x_1) ∉ V
⊢ False

Proof state:
case h.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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, ε n • ↑x ∉ V

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

Result:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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, ε n • ↑x ∉ V

Proof state:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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, ε n • ↑x ∉ V

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

Result:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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 • ↑⟨x, hxS⟩ ∈ V
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
⊢ ∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕜 i → Absorbs 𝕜 (id i) S

Tactic:
by_contra! H'

Result:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
H' : ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i) ∧ ¬Absorbs 𝕜 (id i) S
⊢ False

Proof state:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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 • ↑⟨x, hxS⟩ ∈ V
⊢ False

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

Result:
case h.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : 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 : V ∈ 𝓝 0
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 : ↑⟨x, hxS⟩ ∈ (ε n)⁻¹ • V
⊢ False