awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h : r > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
⊢ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
have h : ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h : ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r
⊢ ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
have h : 1 + max r 0 > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < 1 + max r 0
Tactic: use 1 + max r 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
⊢ (WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p) ↔
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1)
have refine_1 : ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p),
  Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
refine_1 :
  ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p),
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
⊢ (WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p) ↔
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1)
have refine_2 : ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p), IsVonNBounded 𝕜 (p.ball 0 1)
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
refine_1 :
  ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p),
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
refine_2 :
  ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p), IsVonNBounded 𝕜 (p.ball 0 1)
⊢ (WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p) ↔
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1)
have refine_3 : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1) →
  WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
have refine_1 : ∃ (s : Finset (Fin 1)), ∃ r > 0, ball.{u_2, u_6} (𝕜 := 𝕜) (s.sup fun (x : Fin 1) ↦ p) 0 r ⊆ p.ball 0 1
Tactic: apply (h.mem_nhds_iff _ _).2
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
⊢ IsVonNBounded 𝕜 (p.ball 0 1)
have apply : ∀ (i : Fin 1), ∃ r > 0, ∀ x ∈ p.ball 0 1, (p : (a : E) → ℝ) x < r
Tactic: apply h.isVonNBounded_iff_seminorm_bounded.2 (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
⊢ WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
have refine_3 : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
Tactic: apply SeminormFamily.withSeminorms_of_nhds
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
have refine_3 : ∀ (s : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) s ↔
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
⊢ Membership.mem (γ := Filter E) (𝓝 0) s ↔
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
have refine_3 : ∀ (hs : Membership.mem (γ := Filter E) (𝓝 0) s),
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
Tactic: refine ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
refine_3 :
  ∀ (hs : Membership.mem (γ := Filter E) (𝓝 0) s),
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
⊢ Membership.mem (γ := Filter E) (𝓝 0) s ↔
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
have refine_3₁ : ∀
  (hs :
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s),
  Membership.mem (γ := Filter E) (𝓝 0) s
Tactic: refine ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
have refine_3 : ∀ (c : 𝕜) (hc : p.ball 0 1 ⊆ c • s) (c_ne : c ≠ 0),
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
Tactic: obtain ⟨c, hc, c_ne⟩ : ∃ (c : 𝕜), p.ball 0 1 ⊆ c • s ∧ c ≠ 0 :=
      ((h' hs).and (eventually_ne_cobounded 0)).exists
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s
have this : c • p.ball 0 ‖c⁻¹‖ ⊆ c • s
Tactic: have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : c • p.ball 0 ‖c⁻¹‖ ⊆ c • s
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s
have rwa : ∀ (this : p.ball 0 ‖c⁻¹‖ ⊆ s), p.ball 0 ‖c⁻¹‖ ⊆ s
Tactic: rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
have this : p.ball 0 ‖c⁻¹‖ ⊆ s
Tactic: have : p.ball 0 (‖c⁻¹‖) ⊆ s := by
      have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
      rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
have refine_3 : Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
  (p.ball 0 ‖c⁻¹‖)
Tactic: grw [← this]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (p.ball 0 ‖c⁻¹‖)
have refine_3 : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) (p.ball 0 ‖c⁻¹‖)
Tactic: apply FilterBasis.mem_filter_of_mem
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ Membership.mem (γ := Set (Set E)) (SeminormFamily.basisSets.{u_2, u_6, 0} (R := 𝕜) (ι := Fin 1) fun (i : Fin 1) ↦ p)
    (p.ball 0 ‖c⁻¹‖)
have refine_3 : 0 < ‖c⁻¹‖
Tactic: apply SeminormFamily.basisSets_singleton_mem _ 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
⊢ Membership.mem (γ := Filter E) (𝓝 0) s
have refine_3 : ∀ (t : Set E)
  (ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t)
  (ts : t ⊆ s), Membership.mem (γ := Filter E) (𝓝 0) s
Tactic: rcases (FilterBasis.mem_filter_iff _).1 hs with ⟨t, ht, ts⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
⊢ Membership.mem (γ := Filter E) (𝓝 0) s
have refine_3 : Membership.mem (γ := Filter E) (𝓝 0) t
Tactic: grw [← ts]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have refine_3 : ∀ (w : Finset (Fin 1)) (r : ℝ) (r_pos : 0 < r) (hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r),
  Membership.mem (γ := Filter E) (𝓝 0) t
Tactic: rcases (SeminormFamily.basisSets_iff _).1 ht with ⟨w, r, r_pos, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have refine_3 : ∀ (hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup ∅ fun (x : Fin 1) ↦ p) 0 r), Membership.mem (γ := Filter E) (𝓝 0) t
Tactic: rcases eq_or_ne w ∅ with rfl | w_ne
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
refine_3 :
  ∀ (hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup ∅ fun (x : Fin 1) ↦ p) 0 r), Membership.mem (γ := Filter E) (𝓝 0) t
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have refine_3₁ : ∀ (w_ne : w ≠ ∅), Membership.mem (γ := Filter E) (𝓝 0) t
Tactic: rcases eq_or_ne w ∅ with rfl | w_ne
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup ∅ fun (x : Fin 1) ↦ p) 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have hw₁ : t = univ
Tactic: simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, setOf_true] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
⊢ w = Finset.univ
have rcases : ∀ (i : Fin 1) (hi : i ∈ w), w = Finset.univ
Tactic: rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
⊢ w = Finset.univ
have h₁ : ∀ (j : Fin 1), j ∈ w ↔ Membership.mem (γ := Finset (Fin 1)) Finset.univ j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
⊢ t = p.ball 0 r
have this : w = Finset.univ
Tactic: have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have this : t = p.ball 0 r
Tactic: have : t = p.ball 0 r := by
      have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
      simpa only [this, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
        Finset.sup_singleton] using hw
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) t
have refine_3 : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
Tactic: rw [this]