-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem nhds_hasBasis_absConvex :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ AbsConvex 𝕜 s) id

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
⊢ (𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ AbsConvex 𝕜 s) id

Tactic:
refine
  (LocallyConvexSpace.convex_basis_zero ℝ E).to_hasBasis (fun s hs => ?_) fun s hs =>
    ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ AbsConvex 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s))

Tactic:
refine ⟨(balancedCore_balanced s).convexHull, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Convex ℝ ((convexHull ℝ) (balancedCore 𝕜 s))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Convex ℝ ((convexHull ℝ) (balancedCore 𝕜 s))

Tactic:
exact convex_convexHull ℝ (balancedCore 𝕜 s)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨convexHull ℝ (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ (convexHull ℝ) (balancedCore 𝕜 s) ∈ 𝓝 0 ∧ AbsConvex 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ (convexHull ℝ) (balancedCore 𝕜 s) ∈ 𝓝 0 ∧ AbsConvex 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s))

Tactic:
refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull ℝ _), ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ AbsConvex 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s))