ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
letI : TopologicalSpace E := sInf ts
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
refine'
  LocallyConvexSpace.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
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (⨅ (i : ↑ts), 𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
rw [nhds_sInf, ← iInf_subtype'']
no goals
ι : Sort ?u.41463
𝕜 : Type u_2
E : Type u_1
F : Type ?u.41472
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (⨅ (i : ↑ts), 𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
exact hasBasis_iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ ↑i).mp (h (↑i) i.2) x