awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
S : Set E
hS : Convex ℝ S
x : (↑S : Type u_2)
s : Set (↑S : Type u_2)
hs : s ∈ 𝓝 x
t : Set E
ht : t ∈ 𝓝 (↑x : E) ∧ Subtype.val (p := fun (x : E) ↦ x ∈ S) ⁻¹' t ⊆ s
t' : Set E
ht' : (t' ∈ 𝓝 (↑x : E) ∧ Convex ℝ t') ∧ id t' ⊆ t
⊢ IsPathConnected (S ∩ t')

Tactic:
exact (hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩

Premises used: Convex.isPathConnected, mem_of_mem_nhds, Convex.inter, And.right, And.left, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) id

Tactic:
(LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis
    (fun s hs =>
      ⟨interior s, ⟨mem_interior_iff_mem_nhds.mpr hs.1, isOpen_interior, hs.2.interior⟩,
        interior_subset⟩)
    fun s hs => ⟨s, ⟨hs.2.1.mem_nhds hs.1, hs.2.2⟩, subset_rfl⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, LocallyConvexSpace.convex_basis_zero, isOpen_interior, Convex.interior, And.right, And.left, And.intro, IsOpen.mem_nhds, interior, Exists.intro, Filter.HasBasis.to_hasBasis, subset_rfl
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ IsUniformAddGroup E

Tactic:
haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ HasBasis (α := E × E) (comap (β := E) (fun (x : E × E) ↦ x.2 - x.1) (𝓝 0))
    (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦ (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i

Tactic:
have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  HasBasis (α := E × E) (comap (β := E) (fun (x : E × E) ↦ x.2 - x.1) (𝓝 0))
    (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦ (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
⊢ (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i

Tactic:
rw [← uniformity_eq_comap_nhds_zero] at this

Premises used: uniformity_eq_comap_nhds_zero
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
rcases :
  ∀ (V : Set E)
    (hV :
      Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
        (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V)))
    (hV0 : 0 ∈ V) (hVopen : IsOpen[inst_5] V) (hVconvex : Convex 𝕜 V),
    ∃ (u : Set E) (v : Set E),
      IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
⊢ ∃ (u : Set E) (v : Set E),
    IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩

Premises used: Disjoint.exists_uniform_thickening_of_basis
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
⊢ ∃ (u : Set E) (v : Set E),
    IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
    subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩

Premises used: Set.subset_add_left, Convex.add, IsOpen.add_left, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
refine : Disjoint (s + V) (t + V)
⊢ ∃ (u : Set E) (v : Set E),
    IsOpen[inst_5] u ∧ IsOpen[inst_5] v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
refine ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex,
    subset_add_left _ hV0, subset_add_left _ hV0, ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
simp_rw : Disjoint.{u_2} (α := Set E) (⋃ a ∈ s, (fun (x : E) ↦ -a + x) ⁻¹' V) (⋃ a ∈ t, (fun (x : E) ↦ -a + x) ⁻¹' V)
⊢ Disjoint (s + V) (t + V)

Tactic:
simp_rw [← iUnion_add_left_image, image_add_left]

Premises used: Set.image_add_left, Set.iUnion_add_left_image
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
    (⋃ x ∈ t, UniformSpace.ball x ((fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
⊢ Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
    (⋃ x ∈ t, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)

Tactic:
simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV

Premises used: sub_eq_neg_add, Set.preimage_comp, UniformSpace.ball
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
    (⋃ x ∈ t, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
⊢ Disjoint.{u_2} (α := Set E) (⋃ a ∈ s, (fun (x : E) ↦ -a + x) ⁻¹' V) (⋃ a ∈ t, (fun (x : E) ↦ -a + x) ⁻¹' V)

Tactic:
hV
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed[inst_5] t
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this :
  (uniformity E).HasBasis (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_5] s ∧ Convex 𝕜 s) fun (i : Set E) ↦
    (fun (x : E × E) ↦ x.2 - x.1) ⁻¹' id i
V : Set E
hV0 : 0 ∈ V
hVopen : IsOpen[inst_5] V
hVconvex : Convex 𝕜 V
hV :
  Disjoint.{u_2} (α := Set E) (⋃ x ∈ s, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
    (⋃ x ∈ t, (fun (x : E × E) ↦ -x.1 + x.2) ∘ Prod.mk x ⁻¹' id V)
⊢ Disjoint.{u_2} (α := Set E) (⋃ a ∈ s, (fun (x : E) ↦ -a + x) ⁻¹' V) (⋃ a ∈ t, (fun (x : E) ↦ -a + x) ⁻¹' V)

Tactic:
exact hV
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
inst_8 : LocallyConvexSpace 𝕜 E
s : Set E
x : E
hx : x ∉ s
hsconv : Convex 𝕜 s
hsclosed : IsClosed[inst_5] s
⊢ ∃ (U : Set E) (V : Set E),
    IsOpen[inst_5] U ∧ IsOpen[inst_5] V ∧ Convex 𝕜 U ∧ Convex 𝕜 V ∧ x ∈ U ∧ s ⊆ V ∧ Disjoint U V

Tactic:
simpa [*] using Disjoint.exists_open_convexes (s := {x}) (t := s) (𝕜 := 𝕜)

Premises used: Disjoint.exists_open_convexes
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E

Tactic:
.ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
      (fun x => fun If : Set ts × (ts → Set E) =>
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
      (fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2

Premises used: Set.iInter, Set.Finite, LocallyConvexSpace.ofBases, Prod.fst, And, And.right, Prod.snd, convex_iInter
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
refine :
  ∀ (x : E),
    (𝓝 x).HasBasis (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
      ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
          If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
        x)
      ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine .ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
      (fun x => fun If : Set ts × (ts → Set E) =>
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
      (fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
rw :
  HasBasis.{u_3, u_3 + 1} (α := E) (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    (⨅ (i : (↑ts : Type u_3)), 𝓝 x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)
⊢ (𝓝 x).HasBasis (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)

Tactic:
rw [nhds_sInf, ← iInf_subtype'']

Premises used: nhds_sInf, iInf_subtype''
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis.{u_3, u_3 + 1} (α := E) (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    (⨅ (i : (↑ts : Type u_3)), 𝓝 x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)

Tactic:
.iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ _ ↑i).mp (h (↑i) i.2) x

Premises used: locallyConvexSpace_iff, Filter.HasBasis.iInf', Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis.{u_3, u_3 + 1} (α := E) (ι := Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E))
    (⨅ (i : (↑ts : Type u_3)), 𝓝 x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦
        If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i))
      x)
    ((fun (x : E) (If : Set (↑ts : Type u_3) × ((↑ts : Type u_3) → Set E)) ↦ (⋂ i ∈ If.1, If.2 i : Set E)) x)

Tactic:
exact .iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ _ ↑i).mp (h (↑i) i.2) x
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
ts' : ι → TopologicalSpace E
h' rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ ∀ (t : TopologicalSpace E),
    Membership.mem (γ := Set (TopologicalSpace E)) (range fun (i : ι) ↦ ts' i) t → LocallyConvexSpace 𝕜 E

Tactic:
rwa [forall_mem_range]

Premises used: Set.forall_mem_range
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
rw : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
.iInf fun b => ?_

Premises used: LocallyConvexSpace.iInf
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
refine : ∀ (b : Bool), LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine .iInf fun b => ?_
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
false : LocallyConvexSpace 𝕜 E
true : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
cases b
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
assumption
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
⊢ LocallyConvexSpace 𝕜 E

Tactic:
LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
    (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
    hs.linear_preimage f

Premises used: Membership.mem, nhds, LocallyConvexSpace.ofBases, _private.0.LocallyConvexSpace.induced.match_1, And, Set.preimage, Convex, DFunLike.coe, Convex.linear_preimage
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
refine :
  ∀ (x : E),
    HasBasis.{u_3, u_4 + 1} (ι := Set F) (𝓝 x)
      ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
      ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
    (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
    hs.linear_preimage f

Premises used: Membership.mem, nhds, LocallyConvexSpace.ofBases, _private.0.LocallyConvexSpace.induced.match_1, And, Set.preimage, Convex, DFunLike.coe, Convex.linear_preimage
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
x : E
rw :
  HasBasis.{u_3, u_4 + 1} (α := E) (ι := Set F)
    (comap.{u_3, u_4} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F))
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)
⊢ HasBasis.{u_3, u_4 + 1} (ι := Set F) (𝓝 x)
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)

Tactic:
rw [nhds_induced]

Premises used: nhds_induced
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
x : E
⊢ HasBasis.{u_3, u_4 + 1} (α := E) (ι := Set F)
    (comap.{u_3, u_4} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F))
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)

Tactic:
(LocallyConvexSpace.convex_basis <| f x).comap f

Premises used: Filter.HasBasis.comap, LocallyConvexSpace.convex_basis, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.LocallyConvex
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid F
inst_5 : Module 𝕜 F
t : TopologicalSpace F
inst_6 : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (⇑f : (a : E) → F) t
x : E
⊢ HasBasis.{u_3, u_4 + 1} (α := E) (ι := Set F)
    (comap.{u_3, u_4} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (𝓝 ((f : (a : E) → F) x) : Filter F))
    ((fun (x : E) (s : Set F) ↦ Membership.mem (γ := Filter F) (𝓝 ((f : (a : E) → F) x) : Filter F) s ∧ Convex 𝕜 s) x)
    ((fun (x : E) ↦ (preimage (⇑f : (a : E) → F) : (s : Set F) → Set E)) x)

Tactic:
exact (LocallyConvexSpace.convex_basis <| f x).comap f

Premises used: Filter.HasBasis.comap, LocallyConvexSpace.convex_basis, DFunLike.coe