case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' U
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU : U ∈ basisSets p
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' U
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' U
rw [hU]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r

case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
by_cases h : x ≠ 0
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬x ≠ 0
⊢ ball (Finset.sup s p) 0 r ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
refine' ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, _⟩
no goals
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬x ≠ 0
⊢ ball (Finset.sup s p) 0 r ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
simp only [not_ne_iff.mp h, subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
  preimage_const_of_mem, zero_smul]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ ball (Finset.sup s p) 0 (r / ‖x‖)
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun y => x • y) ⁻¹' ball (Finset.sup s p) 0 r
rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ball (Finset.sup s p) 0 (r / ‖x‖) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧
    ball (Finset.sup s p) 0 (r / ‖x‖) ⊆ ball (Finset.sup s p) 0 (r / ‖x‖)
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ ball (Finset.sup s p) 0 (r / ‖x‖)
use (s.sup p).ball 0 (r / ‖x‖)
no goals
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.68753
𝕝 : Type ?u.68756
𝕝₂ : Type ?u.68759
E : Type u_1
F : Type ?u.68765
G : Type ?u.68768
ι : Type u_3
ι' : Type ?u.68774
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
x : 𝕜
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : x ≠ 0
⊢ ball (Finset.sup s p) 0 (r / ‖x‖) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧
    ball (Finset.sup s p) 0 (r / ‖x‖) ⊆ ball (Finset.sup s p) 0 (r / ‖x‖)
exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩