awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) (Metric.ball 0 (HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)))

Tactic:
exact Metric.ball_mem_nhds 0 (div_pos hr h)

Premises used: Metric.ball_mem_nhds, div_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)
neg : Membership.mem (γ := Filter R) (𝓝 0) {x : R | True}
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}

Tactic:
simp_rw [le_antisymm h (apply_nonneg _ v), mul_zero, hr]

Premises used: MulZeroClass.mul_zero, le_antisymm, NonnegHomClass.apply_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | True}

Tactic:
IsOpen.mem_nhds isOpen_univ (mem_univ 0)

Premises used: isOpen_univ, IsOpen.mem_nhds, Set.mem_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | True}

Tactic:
exact IsOpen.mem_nhds isOpen_univ (mem_univ 0)

Premises used: isOpen_univ, IsOpen.mem_nhds, Set.mem_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU : U ∈ p.basisSets
rcases :
  ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r),
    ∃ (V : Set R),
      Membership.mem (γ := Filter R) (𝓝 0) V ∧
        ∃ (W : Set E),
          Membership.mem (γ := Set (Set E))
              (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
            V • W ⊆ U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Premises used: Iff.mp, SeminormFamily.basisSets_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩

Premises used: Iff.mpr, Metric.ball, Metric.ball_mem_nhds, Real.sqrt_pos, And.intro, Exists.intro, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
refine :
  ∃ (W : Set E),
    Membership.mem (γ := Set (Set E))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
      HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) W ⊆ U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set E),
        Membership.mem (γ := Set (Set E))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ (W : Set E),
    Membership.mem (γ := Set (Set E))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
      HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) W ⊆ U

Tactic:
⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩

Premises used: Iff.mpr, Real.sqrt_pos, Seminorm.ball, And.intro, Exists.intro, Real.sqrt, Finset.sup, OfNat.ofNat, SeminormFamily.basisSets_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
refine : HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) ((s.sup p).ball 0 √r) ⊆ U
⊢ ∃ (W : Set E),
    Membership.mem (γ := Set (Set E))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
      HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) W ⊆ U

Tactic:
refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) ((s.sup p).ball 0 √r) ⊆ U

Tactic:
Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_

Premises used: Set.Subset.trans, Seminorm.ball_smul_ball, Real.sqrt, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
refine : (s.sup p).ball 0 (√r * √r) ⊆ U
⊢ HSMul.hSMul.{u_1, u_6, u_6} (α := Set R) (Metric.ball 0 √r) ((s.sup p).ball 0 √r) ⊆ U

Tactic:
refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_

Premises used: Set.Subset.trans, Seminorm.ball_smul_ball, Real.sqrt, Finset.sup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
R : Type u_1
E : Type u_6
ι : Type u_9
inst : SeminormedRing R
inst_1 : AddCommGroup E
inst_2 : Module R E
p : SeminormFamily R E ι
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
rw : (s.sup p).ball 0 (√r * √r) ⊆ (s.sup p).ball 0 r
rw₁ rw₂ : (s.sup p).ball 0 r ⊆ (s.sup p).ball 0 r
⊢ (s.sup p).ball 0 (√r * √r) ⊆ U

Tactic:
rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

Premises used: le_of_lt, Real.mul_self_sqrt
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU : U ∈ p.basisSets
rcases :
  ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r),
    ∃ (V : Set F),
      Membership.mem (γ := Set (Set F))
          (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
        V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Premises used: Iff.mp, SeminormFamily.basisSets_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
rw :
  ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' U

Tactic:
rw [hU]
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
pos :
  ∀ (h : x ≠ 0),
    ∃ (V : Set F),
      Membership.mem (γ := Set (Set F))
          (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
        V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
neg :
  ∀ (h : ¬x ≠ 0),
    ∃ (V : Set F),
      Membership.mem (γ := Set (Set F))
          (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
        V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
by_cases h : x ≠ 0
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
pos :
  ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (s.sup p).ball 0 (r / ‖x‖)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]

Premises used: smul_zero, Seminorm.smul_ball_preimage, Finset.sup, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
h₁ :
  Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      ((s.sup p).ball 0 (r / ‖x‖)) ∧
    (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (s.sup p).ball 0 (r / ‖x‖)

Tactic:
use (s.sup p).ball 0 (r / ‖x‖)

Premises used: Norm.norm, HDiv.hDiv, Seminorm.ball, Finset.sup, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      ((s.sup p).ball 0 (r / ‖x‖)) ∧
    (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)

Tactic:
⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩

Premises used: Iff.mpr, norm_pos_iff, Set.Subset.rfl, And.intro, div_pos, SeminormFamily.basisSets_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ Membership.mem (γ := Set (Set F)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      ((s.sup p).ball 0 (r / ‖x‖)) ∧
    (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)

Tactic:
exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩

Premises used: Seminorm.ball, And.intro, Exists.intro, Finset.sup, OfNat.ofNat, SeminormFamily.basisSets_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
neg : (s.sup p).ball 0 r ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r
⊢ ∃ (V : Set F),
    Membership.mem (γ := Set (Set F))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
refine ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬x ≠ 0
⊢ (s.sup p).ball 0 r ⊆ (fun (y : F) ↦ x • y) ⁻¹' (s.sup p).ball 0 r

Tactic:
simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
    preimage_const_of_mem, zero_smul]

Premises used: Seminorm.mem_ball_zero, Set.subset_def, map_zero, not_ne_iff, imp_true_iff, zero_smul, Iff.mp, Set.mem_univ, Set.preimage_const_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
⊢ Eq.{u_7 + 1} (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))

Tactic:
le_antisymm (le_iInf fun i => ?_) ?_

Premises used: le_iInf, le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
refine_1 :
  ∀ (i : ι),
    LE.le (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      (comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
refine_2 :
  LE.le.{u_7} (α := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ Eq.{u_7 + 1} (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))

Tactic:
refine le_antisymm (le_iInf fun i => ?_) ?_

Premises used: le_iInf, le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
refine_1 :
  ∀ (i' : ℝ),
    0 < i' →
      ∃ (i_1 : Set F),
        Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
          id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 i')
⊢ LE.le (α := Filter F) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]

Premises used: AddGroupFilterBasis.toFilterBasis, FilterBasis.hasBasis, Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ ∃ (i_1 : Set F),
    Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
      id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)

Tactic:
⟨(p i).ball 0 ε, ?_, ?_⟩

Premises used: Seminorm.ball, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
refine_1 :
  Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) ((p i).ball 0 ε)
refine_1₁ : id ((p i).ball 0 ε) ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
⊢ ∃ (i_1 : Set F),
    Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i_1 ∧
      id i_1 ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)

Tactic:
refine ⟨(p i).ball 0 ε, ?_, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
refine_1 :
  Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)
    ((Finset.sup {i} p).ball 0 ε)
⊢ Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) ((p i).ball 0 ε)

Tactic:
rw [← (Finset.sup_singleton : _ = p i)]

Premises used: Finset.sup_singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)
    ((Finset.sup {i} p).ball 0 ε)

Tactic:
p.basisSets_mem {i} hε

Premises used: SeminormFamily.basisSets, Set.Mem, iSup, Singleton.singleton, SeminormFamily.basisSets_mem, Set.iUnion
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
⊢ Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)
    ((Finset.sup {i} p).ball 0 ε)

Tactic:
exact p.basisSets_mem {i} hε

Premises used: Singleton.singleton, SeminormFamily.basisSets_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
i : ι
ε : ℝ
hε : 0 < ε
refine_1 : (p i).ball 0 ε ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)
refine_1₁ refine_1₂ :
  Subset (α := Set F) (preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε))
    (preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε))
⊢ id ((p i).ball 0 ε) ⊆ preimage (β := ℝ) (⇑(p i) : (a : F) → ℝ) (Metric.ball 0 ε)

Tactic:
rw [id, (p i).ball_zero_eq_preimage_ball]

Premises used: Seminorm.ball_zero_eq_preimage_ball, id
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
refine_2 :
  ∀ (i' : Set F),
    Membership.mem (γ := FilterBasis F) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) i' →
      Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id i')
⊢ LE.le.{u_7} (α := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0))
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]

Premises used: AddGroupFilterBasis.toFilterBasis, FilterBasis.hasBasis, Filter.HasBasis.ge_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
U : Set F
hU : U ∈ p.basisSets
refine_2 :
  ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : (s.sup p).ball 0 r ∈ p.basisSets),
    Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id ((s.sup p).ball 0 r))
⊢ Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id U)

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩

Premises used: Iff.mp, SeminormFamily.basisSets_iff, rfl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
refine_2 :
  ∀ i ∈ s, Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) ((p i).ball 0 r)
⊢ Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) (id ((s.sup p).ball 0 r))

Tactic:
rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]

Premises used: id, Finset.iInter_mem_sets, Seminorm.ball_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ ∀ i ∈ s, Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) ((p i).ball 0 r)

Tactic:
fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

Premises used: Seminorm.ball_zero_eq_preimage_ball, Metric.ball, Filter.mem_iInf_of_mem, Eq.subset, Metric.ball_mem_nhds, And.intro, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ ∀ i ∈ s, Membership.mem (γ := Filter F) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : F) → ℝ) (𝓝 0)) ((p i).ball 0 r)

Tactic:
exact fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩