case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i : Set E),
    i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i → ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id i

case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i' : Set E),
    0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i' → ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id i'
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ Filter.HasBasis (𝓝 0) (fun s => 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
refine' (nhds_basis_abs_convex 𝕜 E).to_hasBasis _ _
case refine'_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
case refine'_2
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i' : Set E),
    0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i' → ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id i'
rintro s ⟨hs_zero, hs_open, hs_balanced, hs_convex⟩
no goals
case refine'_2.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
exact ⟨s, ⟨hs_open.mem_nhds hs_zero, hs_balanced, hs_convex⟩, rfl.subset⟩
case refine'_1.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
case refine'_1
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i : Set E),
    i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i → ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id i
rintro s ⟨hs_nhds, hs_balanced, hs_convex⟩
case refine'_1.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ 0 ∈ interior s ∧ IsOpen (interior s) ∧ Balanced 𝕜 (interior s) ∧ Convex ℝ (interior s)
case refine'_1.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
refine' ⟨interior s, _, interior_subset⟩
no goals
case refine'_1.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.25341
G : Type ?u.25344
ι : Type ?u.25347
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ 0 ∈ interior s ∧ IsOpen (interior s) ∧ Balanced 𝕜 (interior s) ∧ Convex ℝ (interior s)
exact
  ⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior,
    hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds), hs_convex.interior⟩