awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h_1 : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
h : comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
refine (comp_mono f (finset_sup_le_sum q s')).trans ?_

Premises used: Seminorm.comp_mono, LE.le.trans, Seminorm.finset_sup_le_sum
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h_1 : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
h : ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
simp_rw [← pullback_apply, map_sum, pullback_apply]

Premises used: Seminorm.pullback_apply, map_sum
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
(Finset.sum_le_sum hs).trans ?_

Premises used: Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h_1 : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
h : ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
refine (Finset.sum_le_sum hs).trans ?_

Premises used: Finset.sum_le_sum, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h_1 : s'.Nonempty
fₛ : (i : ι') → Finset ι
fC : (i : ι') → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
h : s'.card • s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
h₁ h₂ : s'.card • s'.sup fC • (s'.biUnion fₛ).sup p ≤ s'.card • s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
rw [Finset.sum_const, smul_assoc]

Premises used: smul_assoc, Finset.sum_const
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : SeminormedRing 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
hf : IsBounded p q f
s' : Finset ι'
inl : ∃ (C : ℝ≥0) (s : Finset ι), (Finset.sup ∅ q).comp f ≤ C • s.sup p
inr inr₁ : s'.Nonempty → ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
inr₂ :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p),
      ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p
h :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p),
      (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
h₁ :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p)
      (hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p),
      (s'.sup q).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
h₂ :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p)
      (hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p),
      comp (∑ i ∈ s', q i) f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
h₃ :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p)
      (hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p),
      ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
h₄ :
  s'.Nonempty →
    ∀ (fₛ : (i : ι') → Finset ι) (fC : (i : ι') → ℝ≥0) (hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p)
      (hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p),
      ∑ i ∈ s', s'.sup fC • (s'.biUnion fₛ).sup p ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
⊢ ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

Tactic:
classical
  obtain rfl | _ := s'.eq_empty_or_nonempty
  · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
  choose fₛ fC hf using hf
  use s'.card • s'.sup fC, Finset.biUnion s' fₛ
  have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p := by
    intro i hi
    refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))
    exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
  refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
  simp_rw [← pullback_apply, map_sum, pullback_apply]
  refine (Finset.sum_le_sum hs).trans ?_
  rw [Finset.sum_const, smul_assoc]

Premises used: smul_assoc, Seminorm.pullback_apply, map_sum, Finset.card, Seminorm.comp_mono, LE.le.trans, Seminorm.finset_sup_le_sum, rfl, Finset.eq_empty_or_nonempty, Finset.sum_const
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
⊢ t = p.moduleFilterBasis.topology

Tactic:
hp.1

Premises used: WithSeminorms.topology_eq_withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : PolynormableSpace 𝕜 E
⊢ WithSeminorms.{u_2, u_6, u_6} (𝕜 := 𝕜) (E := E) (ι :=
    { p : Seminorm 𝕜 E // Continuous[inst_3, _] (⇑p : (a : E) → ℝ) })
    fun (p : { p : Seminorm 𝕜 E // Continuous[inst_3, _] (⇑p : (a : E) → ℝ) }) ↦ (↑p : Seminorm 𝕜 E)

Tactic:
PolynormableSpace.withSeminorms'

Premises used: PolynormableSpace.withSeminorms'
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
rw : IsTopologicalAddGroup E
⊢ IsTopologicalAddGroup E

Tactic:
rw [hp.withSeminorms_eq]

Premises used: WithSeminorms.withSeminorms_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
AddGroupFilterBasis.isTopologicalAddGroup _

Premises used: AddGroupFilterBasis.isTopologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
exact AddGroupFilterBasis.isTopologicalAddGroup _

Premises used: AddGroupFilterBasis.isTopologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
rw : ContinuousSMul 𝕜 E
⊢ ContinuousSMul 𝕜 E

Tactic:
rw [hp.withSeminorms_eq]

Premises used: WithSeminorms.withSeminorms_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ContinuousSMul 𝕜 E

Tactic:
ModuleFilterBasis.continuousSMul _

Premises used: ModuleFilterBasis.continuousSMul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ContinuousSMul 𝕜 E

Tactic:
exact ModuleFilterBasis.continuousSMul _

Premises used: ModuleFilterBasis.continuousSMul
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
rw : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
rw [congr_fun (congr_arg (@nhds E) hp.1) 0]

Premises used: nhds, WithSeminorms.topology_eq_withSeminorms, congr_arg, congr_fun, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
AddGroupFilterBasis.nhds_zero_hasBasis _

Premises used: SeminormFamily.basisSets, Set.Mem, iSup, AddGroupFilterBasis.nhds_zero_hasBasis, Set.iUnion
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id

Tactic:
exact AddGroupFilterBasis.nhds_zero_hasBasis _

Premises used: AddGroupFilterBasis.nhds_zero_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (𝓝 0) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦
    (sr.1.sup p).ball 0 sr.2

Tactic:
⟨fun V => ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
refine :
  ∀ (V : Set E), Membership.mem (γ := Filter E) (𝓝 0) V ↔ ∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (𝓝 0) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦
    (sr.1.sup p).ball 0 sr.2

Tactic:
refine ⟨fun V => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
V : Set E
simp :
  (∃ (i : Set E), (∃ (i_1 : Finset ι) (r : ℝ), 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ i ⊆ V) ↔
    ∃ (a : Finset ι) (b : ℝ), 0 < b ∧ (a.sup p).ball 0 b ⊆ V
⊢ Membership.mem (γ := Filter E) (𝓝 0) V ↔ ∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V

Tactic:
simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists, id_eq]

Premises used: Filter.HasBasis.mem_iff, Prod.exists, WithSeminorms.hasBasis, SeminormFamily.basisSets_iff, id_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
V : Set E
⊢ (∃ (i : Set E), (∃ (i_1 : Finset ι) (r : ℝ), 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ i ⊆ V) ↔
    ∃ (a : Finset ι) (b : ℝ), 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Tactic:
grind
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
⊢ IsTopologicalAddGroup E

Tactic:
have : IsTopologicalAddGroup E := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
rw :
  HasBasis.{u_6, u_9 + 1} (α := E) (Filter.map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2)
    fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2
⊢ (𝓝 x).HasBasis (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2) fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2

Tactic:
rw [← map_add_left_nhds_zero]

Premises used: map_add_left_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (Filter.map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2)
    fun (i : Finset ι × ℝ) ↦ (fun (x_1 : E) ↦ x + x_1) '' (i.1.sup p).ball 0 i.2

Tactic:
hp.hasBasis_zero_ball.map (x + ·)

Premises used: Filter.HasBasis.map, HAdd.hAdd, WithSeminorms.hasBasis_zero_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
h :
  Eq (α := Finset ι × ℝ → Set E) (fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2) fun (i : Finset ι × ℝ) ↦
    (fun (x_1 : E) ↦ x + x_1) '' (i.1.sup p).ball 0 i.2
⊢ HasBasis.{u_6, u_9 + 1} (α := E) (Filter.map (fun (x_1 : E) ↦ x + x_1) (𝓝 0)) (fun (sr : Finset ι × ℝ) ↦ 0 < sr.2)
    fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2

Tactic:
convert! hp.hasBasis_zero_ball.map (x + ·) using 1

Premises used: Filter.HasBasis.map, HAdd.hAdd, WithSeminorms.hasBasis_zero_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
h : ∀ (sr : Finset ι × ℝ), (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
⊢ Eq (α := Finset ι × ℝ → Set E) (fun (sr : Finset ι × ℝ) ↦ (sr.1.sup p).ball x sr.2) fun (i : Finset ι × ℝ) ↦
    (fun (x_1 : E) ↦ x + x_1) '' (i.1.sup p).ball 0 i.2

Tactic:
ext sr : 1
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball (HVAdd.hVAdd (β := E) x 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2

Tactic:
have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
    Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this_1 : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (HVAdd.hVAdd (β := E) x 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
h :
  ∀ (this : (sr.1.sup p).ball (x + 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2),
    (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
h₁ h₂ h₃ h₄ :
  ∀ (this : (sr.1.sup p).ball x sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2),
    (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun (x_1 : E) ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2

Tactic:
rwa [vadd_eq_add, add_zero] at this

Premises used: vadd_eq_add, add_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
U : Set E
rw : (∃ (i : Finset ι × ℝ), 0 < i.2 ∧ (i.1.sup p).ball x i.2 ⊆ U) ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
rw₁ rw₂ :
  (∃ (a : Finset ι) (b : ℝ), 0 < (a, b).2 ∧ ((a, b).1.sup p).ball x (a, b).2 ⊆ U) ↔
    ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U
⊢ U ∈ 𝓝 x ↔ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U

Tactic:
rw [hp.hasBasis_ball.mem_iff, Prod.exists]

Premises used: Filter.HasBasis.mem_iff, Prod.exists, WithSeminorms.hasBasis_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
simp_rw : IsOpen[inst_3] U ↔ ∀ x ∈ U, U ∈ 𝓝 x
⊢ IsOpen[inst_3] U ↔ ∀ x ∈ U, ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ U

Tactic:
simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]

Premises used: WithSeminorms.mem_nhds_iff, isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ IsTopologicalAddGroup E

Tactic:
have := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
⊢ T1Space E

Tactic:
IsTopologicalAddGroup.t1Space _ ?_

Premises used: IsTopologicalAddGroup.t1Space
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
refine : IsClosed[inst_3] {0}
⊢ T1Space E

Tactic:
refine IsTopologicalAddGroup.t1Space _ ?_

Premises used: IsTopologicalAddGroup.t1Space
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
rw : ∀ (x : E), Membership.mem (γ := Set E) {0}ᶜ x → ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
⊢ IsClosed[inst_3] {0}

Tactic:
rw [← isOpen_compl_iff, hp.isOpen_iff_mem_balls]

Premises used: WithSeminorms.isOpen_iff_mem_balls, isOpen_compl_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
obtain :
  ∀ (i : ι) (pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)),
    ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ
⊢ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ

Tactic:
obtain ⟨i, pi_nonzero⟩ := h x hx
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ GT.gt (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
refine : 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)
⊢ ∃ (s : Finset ι), ∃ r > 0, (s.sup p).ball x r ⊆ {0}ᶜ

Tactic:
refine ⟨{i}, p i x, by positivity, subset_compl_singleton_iff.mpr ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : 0 ∉ (p i).ball x ((p i : (a : E) → ℝ) x)
rw₁ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (0 - x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₂ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) (-x) : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₃ : ¬LT.lt (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
rw₄ rw₅ : LE.le (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) ((p i : (a : E) → ℝ) x : ℝ)
⊢ 0 ∉ (Finset.sup {i} p).ball x ((p i : (a : E) → ℝ) x)

Tactic:
rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]

Premises used: Finset.sup_singleton, AddGroupSeminormClass.map_neg_eq_map, not_lt, Seminorm.mem_ball, zero_sub
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
⊢ ∀ ⦃x y : E⦄, x ⤳ y → x = y

Tactic:
have := ((t1Space_TFAE E).out 0 9).mp (inferInstance : T1Space E)