R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ closedBall p 0 (‖k‖ * r) ⊆ k • closedBall p 0 r
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ k • closedBall p 0 r = closedBall p 0 (‖k‖ * r)
refine' subset_antisymm smul_closedBall_subset _
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ closedBall p 0 (‖k‖ * r) → x ∈ k • closedBall p 0 r
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ closedBall p 0 (‖k‖ * r) ⊆ k • closedBall p 0 r
intro x
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ ↑p x ≤ ‖k‖ * r → ∃ y, y ∈ closedBall p 0 r ∧ k • y = x
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ closedBall p 0 (‖k‖ * r) → x ∈ k • closedBall p 0 r
rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]
case refine'_1
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : ↑p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ closedBall p 0 r

case refine'_2
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : ↑p x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ ↑p x ≤ ‖k‖ * r → ∃ y, y ∈ closedBall p 0 r ∧ k • y = x
refine' fun hx => ⟨k⁻¹ • x, _, _⟩
no goals
case refine'_2
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : ↑p x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]
no goals
case refine'_1
R : Type ?u.1205076
R' : Type ?u.1205079
𝕜 : Type u_1
𝕜₂ : Type ?u.1205085
𝕜₃ : Type ?u.1205088
𝕝 : Type ?u.1205091
E : Type u_2
E₂ : Type ?u.1205097
E₃ : Type ?u.1205100
F : Type ?u.1205103
G : Type ?u.1205106
ι : Type ?u.1205109
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : ↑p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ closedBall p 0 r
rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, ← mul_le_mul_left hk, ← mul_assoc,
  ← div_eq_mul_inv ‖k‖ ‖k‖, div_self (ne_of_gt hk), one_mul]