-- Mathlib/Analysis/LocallyConvex/StrongTopology.lean
theorem locallyConvexSpace (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty)
    (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) :
    LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)

Proof state:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : IsTopologicalAddGroup F
inst✝⁸ : OrderedSemiring R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
⊢ ∀ (i : Set E × Set F), i.1 ∈ 𝔖 ∧ i.2 ∈ 𝓝 0 ∧ Convex R i.2 → Convex R {f | ∀ x ∈ i.1, f x ∈ id i.2}

Tactic:
rintro ⟨S, V⟩ ⟨_, _, hVconvex⟩ f hf g hg a b ha hb hab x hx

Result:
case mk.intro.intro
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : IsTopologicalAddGroup F
inst✝⁸ : OrderedSemiring R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
S : Set E
V : Set F
left✝¹ : (S, V).1 ∈ 𝔖
left✝ : (S, V).2 ∈ 𝓝 0
hVconvex : Convex R (S, V).2
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
g : UniformConvergenceCLM σ F 𝔖
hg : g ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : E
hx : x ∈ (S, V).1
⊢ (a • f + b • g) x ∈ id (S, V).2

Proof state:
case mk.intro.intro
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : IsTopologicalAddGroup F
inst✝⁸ : OrderedSemiring R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
S : Set E
V : Set F
left✝¹ : (S, V).1 ∈ 𝔖
left✝ : (S, V).2 ∈ 𝓝 0
hVconvex : Convex R (S, V).2
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
g : UniformConvergenceCLM σ F 𝔖
hg : g ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : E
hx : x ∈ (S, V).1
⊢ (a • f + b • g) x ∈ id (S, V).2

Tactic:
exact hVconvex (hf x hx) (hg x hx) ha hb hab

Result:
no goals

Proof state:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : IsTopologicalAddGroup F
inst✝⁸ : OrderedSemiring R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
⊢ LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)

Tactic:
apply LocallyConvexSpace.ofBasisZero _ _ _ _
  (UniformConvergenceCLM.hasBasis_nhds_zero_of_basis _ _ _ h𝔖₁ h𝔖₂
    (LocallyConvexSpace.convex_basis_zero R F)) _

Result:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : IsTopologicalAddGroup F
inst✝⁸ : OrderedSemiring R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
⊢ ∀ (i : Set E × Set F), i.1 ∈ 𝔖 ∧ i.2 ∈ 𝓝 0 ∧ Convex R i.2 → Convex R {f | ∀ x ∈ i.1, f x ∈ id i.2}