-- Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E)

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : ∃ i r, 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r
⊢ 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s

Tactic:
rcases hs with ⟨t, r, hr, rfl⟩

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧
    IsOpen ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧ AbsConvex 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ ⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r ∧
    IsOpen (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧ AbsConvex 𝕜 (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)

Tactic:
refine
  ⟨mem_iInter₂.mpr fun _ _ => by simp [Seminorm.mem_ball_zero, hr],
    isOpen_biInter_finset fun S _ => ?_,
    balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
    convex_iInter₂ fun _ _ => Seminorm.convex_ball ..⟩

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
⊢ IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
hr' : r = ‖↑r‖ * 1
⊢ ↑r ≠ 0

Tactic:
simp [hr.ne']

Result:
no goals

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
hr' : r = ‖↑r‖ * 1
⊢ IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)

Tactic:
have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ t
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s
⊢ ∃ i' ∈ (gaugeSeminormFamily 𝕜 E).basisSets, id i' ⊆ id s

Tactic:
refine ⟨s, ⟨?_, rfl.subset⟩⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s
⊢ s ∈ (gaugeSeminormFamily 𝕜 E).basisSets

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ ∃ i, (0 ∈ i ∧ IsOpen i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
refine ⟨s, ⟨?_, rfl.subset⟩⟩

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets
⊢ 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s

Proof state:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧
    IsOpen ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧ AbsConvex 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)

Tactic:
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]

Result:
case refine_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ ⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r ∧
    IsOpen (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧ AbsConvex 𝕜 (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)