awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
have 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
Tactic: rw [absorbs_iff_norm] at hVS
Cleared hypotheses: hVS, hV, hVb, n, hn
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
have hVS₁ : ∀ (r : ℝ), ∃ (c : 𝕜), r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
Tactic: push Not at hVS
Cleared hypotheses: hVS
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
have h : ∀ (a : 𝕜) (haε : ‖(ε n)⁻¹‖ ≤ ‖a‖) (haS : ¬S ⊆ a • id V), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
Tactic: rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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 : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
have h : ∀ (x : E) (hxS : x ∈ S) (hx : x ∉ a • id V), ∃ (x : (↑S : Type u_3)), ε n • (↑x : E) ∉ V
Tactic: rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
have h : ∀ (hnx : ε n • (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ V), False
Tactic: refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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
⊢ False
have hnx₁ : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hxS) : E) ∈ (ε n)⁻¹ • V
Tactic: rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
Cleared hypotheses: hnx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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
⊢ False
have this : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ False
have rcases : ∀ (x : ι → (↑S : Type u_3)) (hx : ∀ᶠ (x_1 : ι) in l, ε x_1 • (↑(x x_1) : E) ∉ V), False
Tactic: rcases this.choice with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
have refine : ∀ᶠ (x : ι) in l, False
Tactic: refine Filter.frequently_false l (Filter.Eventually.frequently ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ ∀ᶠ (x : ι) in l, False
have 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
Tactic: filter_upwards [hx,
    (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ ∀ᶠ (x : ι) in l, False
have h₁ : ∀ (a : ι), ε a • (↑(x a) : E) ∉ V → (ε • Subtype.val (p := fun (x : E) ↦ x ∈ S) ∘ x) a ∈ V → False
Tactic: filter_upwards [hx,
    (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕝 s
have obtain : ∀ (ε : ℕ → 𝕜) (hε : Tendsto ε atTop (𝓝 0)) (hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0), 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 : 𝕜))
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕝 s
have 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)
Tactic: refine isVonNBounded_of_smul_tendsto_zero (ε := (ε · • 1)) (by simpa) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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 (HSMul.hSMul.{u_7, u_6, u_6} (α := ℕ → 𝕝) (fun (x : ℕ) ↦ HSMul.hSMul (β := 𝕝) (ε x) 1) x) atTop (𝓝 0)
have this : Tendsto (ε • x) atTop (𝓝 0)
Tactic: have := h.smul_tendsto_zero (.of_forall hx) hε
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ Absorbs 𝕜 V (closure[inst_3] a)
have 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)
Tactic: rcases exists_mem_nhds_isClosed_subset hV with ⟨W, hW₁, hW₂, hW₃⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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 𝕜 V (closure[inst_3] a)
have ha₁ : Absorbs 𝕜 W a
Tactic: specialize ha hW₁
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ Absorbs 𝕜 V (closure[inst_3] a)
have h : ∀ (b : 𝕜) (ha' : a ⊆ b • W), closure[inst_3] a ⊆ b • V
Tactic: filter_upwards [ha] with b ha'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ closure[inst_3] a ⊆ b • V
have h : closure[inst_3] (b • W) ⊆ b • V
Tactic: grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ closure[inst_3] a ⊆ b • V
have h₁ : b • closure[inst_3] W ⊆ b • V
Tactic: grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ closure[inst_3] a ⊆ b • V
have h₂ : b • W ⊆ b • V
Tactic: grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ closure[inst_3] a ⊆ b • V
have h₃ : b • V ⊆ b • V
Tactic: grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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 𝕜 (x +ᵥ s)
have rw : IsVonNBounded 𝕜 (HVAdd.hVAdd (α := Set E) {x} s)
Tactic: rw [← singleton_vadd]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
have inl : IsVonNBounded 𝕜 (∅ + t) ↔
  Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ t = ∅ ∨ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅ ∧ IsVonNBounded 𝕜 t
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
have inr : ∀ (hs : s.Nonempty), IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
have inr : IsVonNBounded 𝕜 (s + ∅) ↔
  s = ∅ ∨ Eq.{u_3 + 1} (α := Set E) ∅ ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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) ∅
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
have inr₁ : ∀ (ht : t.Nonempty), IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
have inl : IsVonNBounded 𝕜 (HAdd.hAdd (α := Set E) ∅ ∅) ↔ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
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) ∅
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
have inr : ∀ (hs : s.Nonempty), IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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 }
⊢ Bornology.IsVonNBounded 𝕜 s
have hs₁ : ∀ (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
Cleared hypotheses: hs, h, this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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
⊢ Absorbs 𝕜 U s
have h₁ : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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)
⊢ Absorbs 𝕜 U s
have 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
Tactic: have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
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
⊢ Absorbs 𝕜 U s
have 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
Tactic: simp_rw [← nhds_prod_eq, id] at h'
Cleared hypotheses: h'