awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
R : Type u_4
V : Type u_5
inst_17 : CommRing R
inst_18 : TopologicalSpace R
inst_19 : T2Space R
inst_20 : ContinuousAdd R
inst_21 : ContinuousConstSMul R R
inst_22 : AddCommGroup V
inst_23 : Module R V
inst_24 : TopologicalSpace V
inst_25 : SeparatingDual R V
x x_1 : V
h :
  Eq (α := (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x : (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x_1 : (V →L[R] R) →ₗ[R] R)
hne : ¬x = x_1
f : StrongDual R V
hf : Ne.{u_4 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) x_1 : R)
⊢ False

Tactic:
hf (DFunLike.congr_fun h f)

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Analysis.LocallyConvex.WeakSpace
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
inst_5 : Module ℝ E
inst_6 : IsScalarTower ℝ 𝕜 E
inst_7 : Module ℝ F
inst_8 : IsScalarTower ℝ 𝕜 F
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousSMul 𝕜 E
inst_12 : LocallyConvexSpace ℝ E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
inst_15 : ContinuousSMul 𝕜 F
inst_16 : LocallyConvexSpace ℝ F
R : Type u_4
V : Type u_5
inst_17 : CommRing R
inst_18 : TopologicalSpace R
inst_19 : T2Space R
inst_20 : ContinuousAdd R
inst_21 : ContinuousConstSMul R R
inst_22 : AddCommGroup V
inst_23 : Module R V
inst_24 : TopologicalSpace V
inst_25 : SeparatingDual R V
x x_1 : V
h :
  Eq (α := (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x : (V →L[R] R) →ₗ[R] R)
    ((LinearMap.flip (topDualPairing R V) : (a : V) → (V →L[R] R) →ₗ[R] R) x_1 : (V →L[R] R) →ₗ[R] R)
hne : ¬x = x_1
f : StrongDual R V
hf : Ne.{u_4 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) x_1 : R)
⊢ False

Tactic:
exact hf (DFunLike.congr_fun h f)

Premises used: DFunLike.congr_fun
-- 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
⊢ U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = (i.sup p).ball 0 r

Tactic:
simp only [basisSets, mem_iUnion, exists_prop, mem_singleton_iff]

Premises used: SeminormFamily.basisSets, Set.mem_iUnion, exists_prop, Set.mem_singleton_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 ι
i : Finset ι
r : ℝ
hr : 0 < r
⊢ (i.sup p).ball 0 r ∈ p.basisSets

Tactic:
(basisSets_iff _).mpr ⟨i, _, hr, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, SeminormFamily.basisSets_iff, rfl
-- 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 ι
i : ι
r : ℝ
hr : 0 < r
rw rw₁ : (p i).ball 0 r = (p i).ball 0 r
⊢ (p i).ball 0 r = (Finset.sup {i} p).ball 0 r

Tactic:
rw [Finset.sup_singleton]

Premises used: Finset.sup_singleton
-- 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 ι
rw : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) ⊥ 0 1)
rw₁ : Eq.{u_6 + 1} (α := Set E) univ (ball.{u_1, u_6} (𝕜 := R) 0 0 1)
rw₂ rw₃ : Eq.{u_6 + 1} (α := Set E) univ univ
⊢ univ = (Finset.sup ∅ p).ball 0 1

Tactic:
rw [Finset.sup_empty, Seminorm.bot_eq_zero, ball_zero' _ one_pos]

Premises used: Seminorm.bot_eq_zero, Finset.sup_empty, Seminorm.ball_zero', one_pos
-- 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 ι
⊢ p.basisSets.Nonempty

Tactic:
nonempty_def.mpr ⟨univ, basisSets_univ_mem _⟩

Premises used: Iff.mpr, Set.univ, SeminormFamily.basisSets_univ_mem, Set.nonempty_def, Exists.intro
-- 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 ι
⊢ p.basisSets.Nonempty

Tactic:
refine nonempty_def.mpr ⟨univ, basisSets_univ_mem _⟩

Premises used: Iff.mpr, Set.univ, SeminormFamily.basisSets_univ_mem, Set.nonempty_def, Exists.intro
-- 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 V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

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 V : Set E
hU_1 : U ∈ p.basisSets
hV : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
rcases : ∀ (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂) (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩

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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
h : ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
use ((s ∪ t).sup p).ball 0 (min r₁ r₂)

Premises used: Seminorm.ball, Finset.sup, Union.union, OfNat.ofNat, Min.min
-- 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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V

Tactic:
⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩

Premises used: Iff.mpr, And.intro, Union.union, SeminormFamily.basisSets_mem, lt_min_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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
h : ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V

Tactic:
refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, 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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
h :
  Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
    ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)
⊢ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V

Tactic:
rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]

Premises used: Iff.mpr, And.intro, Seminorm.ball_finset_sup_eq_iInter, lt_min_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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
    ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)

Tactic:
Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

Premises used: Set.iInter₂_mono', Seminorm.ball_mono, Finset.subset_union_left, min_le_left, Set.subset_inter, min_le_right, Exists.intro, Finset.subset_union_right
-- 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 V : Set E
hU_1 : U ∈ p.basisSets
hV_1 : V ∈ p.basisSets
s : Finset ι
r₁ : ℝ
hr₁ : 0 < r₁
hU : U = (s.sup p).ball 0 r₁
t : Finset ι
r₂ : ℝ
hr₂ : 0 < r₂
hV : V = (t.sup p).ball 0 r₂
⊢ Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
    ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)

Tactic:
exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

Premises used: Set.iInter₂_mono', Finset.subset_union_left, Set.subset_inter, Exists.intro, Finset.subset_union_right
-- 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 V : Set E
hU : U ∈ p.basisSets
hV : V ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
rcases₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ∃ z ∈ p.basisSets, z ⊆ U ∩ V
h :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂),
    ((s ∪ t).sup p).ball 0 (min r₁ r₂) ∈ p.basisSets ∧ ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
h₁ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂), ((s ∪ t).sup p).ball 0 (min r₁ r₂) ⊆ U ∩ V
h₂ :
  ∀ (s : Finset ι) (r₁ : ℝ) (hr₁ : 0 < r₁) (hU : U = (s.sup p).ball 0 r₁) (t : Finset ι) (r₂ : ℝ) (hr₂ : 0 < r₂)
    (hV : V = (t.sup p).ball 0 r₂),
    Subset.{u_6} (α := Set E) (⋂ i ∈ s ∪ t, (p i).ball 0 (min r₁ r₂))
      ((⋂ i ∈ s, (p i).ball 0 r₁) ∩ ⋂ i ∈ t, (p i).ball 0 r₂)
⊢ ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Tactic:
classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

Premises used: Set.iInter₂_mono', Finset.subset_union_left, Set.subset_inter, Exists.intro, Iff.mp, Finset.subset_union_right, 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 : U ∈ p.basisSets
rcases : ∀ (ι' : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (ι'.sup p).ball 0 r), 0 ∈ U
⊢ 0 ∈ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨ι', 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
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
rw : 0 < r
⊢ 0 ∈ U

Tactic:
rw [hU, mem_ball_zero, map_zero]

Premises used: Seminorm.mem_ball_zero, map_zero
-- 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
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 < r

Tactic:
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
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 < r

Tactic:
exact 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 : U ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r), ∃ V ∈ p.basisSets, V + V ⊆ U
⊢ ∃ V ∈ p.basisSets, V + V ⊆ 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
h : (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

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

Premises used: HDiv.hDiv, Seminorm.ball, Finset.sup, 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
⊢ (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩

Premises used: And.intro, div_pos, zero_lt_two, 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
h : (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
⊢ (s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩
-- 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
⊢ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_

Premises used: Set.Subset.trans, HDiv.hDiv, Seminorm.ball_add_ball_subset, Finset.sup, 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
h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U
⊢ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U

Tactic:
refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_

Premises used: Set.Subset.trans, HDiv.hDiv, Seminorm.ball_add_ball_subset, Finset.sup, 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
h : (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
h₁ : (s.sup p).ball 0 (r / 2 + r / 2) ⊆ (s.sup p).ball 0 r
h₂ h₃ : (s.sup p).ball 0 r ⊆ (s.sup p).ball 0 r
⊢ (s.sup p).ball (HAdd.hAdd (α := E) 0 0) (r / 2 + r / 2) ⊆ U

Tactic:
rw [hU, add_zero, add_halves]

Premises used: add_halves, add_zero
-- 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 : ℝ), 0 < r → ∀ (hU : U = (s.sup p).ball 0 r), ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U

Tactic:
rcases p.basisSets_iff.mp hU' with ⟨s, r, _, 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' : U ∈ p.basisSets
s : Finset ι
r : ℝ
left : 0 < r
hU : U = (s.sup p).ball 0 r
rw : ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun (x : E) ↦ -x) ⁻¹' U

Tactic:
rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]

Premises used: Seminorm.neg_ball, Set.neg_preimage, Finset.sup, neg_zero
-- 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
s : Finset ι
r : ℝ
left : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r

Tactic:
⟨U, hU', Eq.subset hU⟩

Premises used: Eq.subset, And.intro, Exists.intro
-- 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
s : Finset ι
r : ℝ
left : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V ⊆ (s.sup p).ball 0 r

Tactic:
exact ⟨U, hU', Eq.subset hU⟩
-- 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 : U ∈ p.basisSets
rcases : ∀ (s : Finset ι) (r : ℝ) (hr : 0 < r) (hU : U = (s.sup p).ball 0 r), ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ 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 ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
rw : Membership.mem (γ := Filter R) (𝓝 0) {x : R | x • v ∈ (s.sup p).ball 0 r}
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U

Tactic:
rw [hU, Filter.eventually_iff]

Premises used: Filter.eventually_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 ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
simp_rw : Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | x • v ∈ (s.sup p).ball 0 r}

Tactic:
simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]

Premises used: Seminorm.mem_ball_zero, SeminormClass.map_smul_eq_mul, 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 ι
v : E
U : Set E
hU_1 : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
pos :
  ∀ (h : LT.lt (α := ℝ) (0 : ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ)),
    Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
neg :
  ∀ (h : LE.le (α := ℝ) ((s.sup p : (a : E) → ℝ) v : ℝ) (0 : ℝ)),
    Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}

Tactic:
by_cases! h : 0 < (s.sup p) v

Premises used: Finset.sup, DFunLike.coe
-- 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 : ℝ)
pos : Membership.mem (γ := Filter R) (𝓝 0) {x : R | ‖x‖ < HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)}
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | HMul.hMul (β := ℝ) ‖x‖ ((s.sup p : (a : E) → ℝ) v : ℝ) < r}

Tactic:
simp_rw [(lt_div_iff₀ h).symm]

Premises used: lt_div_iff₀, Iff.symm
-- 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 : ℝ)
pos : Membership.mem (γ := Filter R) (𝓝 0) (Metric.ball 0 (HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)))
⊢ Membership.mem (γ := Filter R) (𝓝 0) {x : R | ‖x‖ < HDiv.hDiv (β := ℝ) r ((s.sup p : (a : E) → ℝ) v : ℝ)}

Tactic:
rw [← _root_.ball_zero_eq]

Premises used: ball_zero_eq
-- 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:
Metric.ball_mem_nhds 0 (div_pos hr h)

Premises used: Set.Mem, Metric.ball_mem_nhds, div_pos, OfNat.ofNat