case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V + V ⊆ U
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ basisSets p
⊢ ∃ V, V ∈ basisSets p ∧ V + V ⊆ U
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (r / 2) ∈ basisSets p ∧ ball (Finset.sup s p) 0 (r / 2) + ball (Finset.sup s p) 0 (r / 2) ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ basisSets p ∧ V + V ⊆ U
use (s.sup p).ball 0 (r / 2)
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (r / 2) + ball (Finset.sup s p) 0 (r / 2) ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (r / 2) ∈ basisSets p ∧ ball (Finset.sup s p) 0 (r / 2) + ball (Finset.sup s p) 0 (r / 2) ⊆ U
refine' ⟨p.basisSets_mem s (div_pos hr zero_lt_two), _⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) (0 + 0) (r / 2 + r / 2) ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (r / 2) + ball (Finset.sup s p) 0 (r / 2) ⊆ U
refine' Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) _
no goals
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.44684
𝕝 : Type ?u.44687
𝕝₂ : Type ?u.44690
E : Type u_1
F : Type ?u.44696
G : Type ?u.44699
ι : Type u_3
ι' : Type ?u.44705
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) (0 + 0) (r / 2 + r / 2) ⊆ U
rw [hU, add_zero, add_halves']