case inl
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r : ℝ
⊢ ball p 0 (‖0‖ * r) ⊆ 0 • ball p 0 r

case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
⊢ ball p 0 (‖k‖ * r) ⊆ k • ball p 0 r
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
⊢ ball p 0 (‖k‖ * r) ⊆ k • ball p 0 r
rcases eq_or_ne k 0 with (rfl | hk)
case inl
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ 0 • ball p 0 r
case inl
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r : ℝ
⊢ ball p 0 (‖0‖ * r) ⊆ 0 • ball p 0 r
rw [norm_zero, MulZeroClass.zero_mul, ball_eq_emptyset _ le_rfl]
no goals
case inl
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r : ℝ
⊢ ∅ ⊆ 0 • ball p 0 r
exact empty_subset _
case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
⊢ x ∈ ball p 0 (‖k‖ * r) → x ∈ k • ball p 0 r
case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
⊢ ball p 0 (‖k‖ * r) ⊆ k • ball p 0 r
intro x
case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
⊢ ↑p x < ‖k‖ * r → ∃ y, y ∈ ball p 0 r ∧ k • y = x
case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
⊢ x ∈ ball p 0 (‖k‖ * r) → x ∈ k • ball p 0 r
rw [Set.mem_smul_set, Seminorm.mem_ball_zero]
case inr.refine'_1
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
hx : ↑p x < ‖k‖ * r
⊢ k⁻¹ • x ∈ ball p 0 r

case inr.refine'_2
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
hx : ↑p x < ‖k‖ * r
⊢ k • k⁻¹ • x = x
case inr
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
⊢ ↑p x < ‖k‖ * r → ∃ y, y ∈ ball p 0 r ∧ k • y = x
refine' fun hx => ⟨k⁻¹ • x, _, _⟩
no goals
case inr.refine'_2
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
hx : ↑p x < ‖k‖ * r
⊢ k • k⁻¹ • x = x
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self hk, one_smul]
no goals
case inr.refine'_1
R : Type ?u.1170073
R' : Type ?u.1170076
𝕜 : Type u_1
𝕜₂ : Type ?u.1170082
𝕜₃ : Type ?u.1170085
𝕝 : Type ?u.1170088
E : Type u_2
E₂ : Type ?u.1170094
E₃ : Type ?u.1170097
F : Type ?u.1170100
G : Type ?u.1170103
ι : Type ?u.1170106
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 : k ≠ 0
x : E
hx : ↑p x < ‖k‖ * r
⊢ k⁻¹ • x ∈ ball p 0 r
rwa [Seminorm.mem_ball_zero, map_smul_eq_mul, norm_inv, ←
  mul_lt_mul_left <| norm_pos_iff.mpr hk, ← mul_assoc, ← div_eq_mul_inv ‖k‖ ‖k‖,
  div_self (ne_of_gt <| norm_pos_iff.mpr hk), one_mul]