R : Type ?u.1242330
R' : Type ?u.1242333
𝕜 : Type u_2
𝕜₂ : Type ?u.1242339
𝕜₃ : Type ?u.1242342
𝕝 : Type ?u.1242345
E : Type u_1
E₂ : Type ?u.1242351
E₃ : Type ?u.1242354
F : Type ?u.1242357
G : Type ?u.1242360
ι : Type ?u.1242363
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : y ∈ ball p 0 (r - ↑p x)
⊢ y ∈ ball p x r
R : Type ?u.1242330
R' : Type ?u.1242333
𝕜 : Type u_2
𝕜₂ : Type ?u.1242339
𝕜₃ : Type ?u.1242342
𝕝 : Type ?u.1242345
E : Type u_1
E₂ : Type ?u.1242351
E₃ : Type ?u.1242354
F : Type ?u.1242357
G : Type ?u.1242360
ι : Type ?u.1242363
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
⊢ Absorbent 𝕜 (ball p x r)
refine' (p.absorbent_ball_zero <| sub_pos.2 hpr).subset fun y hy => _
R : Type ?u.1242330
R' : Type ?u.1242333
𝕜 : Type u_2
𝕜₂ : Type ?u.1242339
𝕜₃ : Type ?u.1242342
𝕝 : Type ?u.1242345
E : Type u_1
E₂ : Type ?u.1242351
E₃ : Type ?u.1242354
F : Type ?u.1242357
G : Type ?u.1242360
ι : Type ?u.1242363
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : ↑p y < r - ↑p x
⊢ y ∈ ball p x r
R : Type ?u.1242330
R' : Type ?u.1242333
𝕜 : Type u_2
𝕜₂ : Type ?u.1242339
𝕜₃ : Type ?u.1242342
𝕝 : Type ?u.1242345
E : Type u_1
E₂ : Type ?u.1242351
E₃ : Type ?u.1242354
F : Type ?u.1242357
G : Type ?u.1242360
ι : Type ?u.1242363
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : y ∈ ball p 0 (r - ↑p x)
⊢ y ∈ ball p x r
rw [p.mem_ball_zero] at hy
no goals
R : Type ?u.1242330
R' : Type ?u.1242333
𝕜 : Type u_2
𝕜₂ : Type ?u.1242339
𝕜₃ : Type ?u.1242342
𝕝 : Type ?u.1242345
E : Type u_1
E₂ : Type ?u.1242351
E₃ : Type ?u.1242354
F : Type ?u.1242357
G : Type ?u.1242360
ι : Type ?u.1242363
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
hpr : ↑p x < r
y : E
hy : ↑p y < r - ↑p x
⊢ y ∈ ball p x r
exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy)