case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (ball p 0 r₁) (ball p 0 r₂)
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r : ℝ
x : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
⊢ Absorbs 𝕜 (ball p 0 r₁) (ball p 0 r₂)
rcases exists_pos_lt_mul hr₁ r₂ with ⟨r, hr₀, hr⟩
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ ball p 0 r₂
⊢ x ∈ a • ball p 0 r₁
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a : 𝕜
r✝ : ℝ
x : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
⊢ Absorbs 𝕜 (ball p 0 r₁) (ball p 0 r₂)
refine' ⟨r, hr₀, fun a ha x hx => _⟩
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ ball p 0 r₂
⊢ ↑p x < ‖a‖ * r₁
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ ball p 0 r₂
⊢ x ∈ a • ball p 0 r₁
rw [smul_ball_zero (norm_pos_iff.1 <| hr₀.trans_le ha), p.mem_ball_zero]
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : ↑p x < r₂
⊢ ↑p x < ‖a‖ * r₁
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : x ∈ ball p 0 r₂
⊢ ↑p x < ‖a‖ * r₁
rw [p.mem_ball_zero] at hx
no goals
case intro.intro
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : ↑p x < r₂
⊢ ↑p x < ‖a‖ * r₁
exact hx.trans (hr.trans_le <| by gcongr)
no goals
R : Type ?u.1218120
R' : Type ?u.1218123
𝕜 : Type u_1
𝕜₂ : Type ?u.1218129
𝕜₃ : Type ?u.1218132
𝕝 : Type ?u.1218135
E : Type u_2
E₂ : Type ?u.1218141
E₃ : Type ?u.1218144
F : Type ?u.1218147
G : Type ?u.1218150
ι : Type ?u.1218153
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ : Seminorm 𝕜 E
A B : Set E
a✝ : 𝕜
r✝ : ℝ
x✝ : E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₁ : 0 < r₁
r : ℝ
hr₀ : 0 < r
hr : r₂ < r * r₁
a : 𝕜
ha : r ≤ ‖a‖
x : E
hx : ↑p x < r₂
⊢ r * r₁ ≤ ‖a‖ * r₁
gcongr