R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ ∀ (x : E), x ∈ Metric.closedBall 0 r₁ • closedBall p 0 r₂ → x ∈ closedBall p 0 (r₁ * r₂)
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ Metric.closedBall 0 r₁ • closedBall p 0 r₂ ⊆ closedBall p 0 (r₁ * r₂)
rw [Set.subset_def]
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
hx : x ∈ Metric.closedBall 0 r₁ • closedBall p 0 r₂
⊢ x ∈ closedBall p 0 (r₁ * r₂)
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
⊢ ∀ (x : E), x ∈ Metric.closedBall 0 r₁ • closedBall p 0 r₂ → x ∈ closedBall p 0 (r₁ * r₂)
intro x hx
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
hx : ∃ x_1 y, x_1 ∈ Metric.closedBall 0 r₁ ∧ y ∈ closedBall p 0 r₂ ∧ x_1 • y = x
⊢ x ∈ closedBall p 0 (r₁ * r₂)
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
hx : x ∈ Metric.closedBall 0 r₁ • closedBall p 0 r₂
⊢ x ∈ closedBall p 0 (r₁ * r₂)
rw [Set.mem_smul] at hx
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : a ∈ Metric.closedBall 0 r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ x ∈ closedBall p 0 (r₁ * r₂)
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
hx : ∃ x_1 y, x_1 ∈ Metric.closedBall 0 r₁ ∧ y ∈ closedBall p 0 r₂ ∧ x_1 • y = x
⊢ x ∈ closedBall p 0 (r₁ * r₂)
rcases hx with ⟨a, y, ha, hy, hx⟩
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : a ∈ Metric.closedBall 0 r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y ≤ r₁ * r₂
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : a ∈ Metric.closedBall 0 r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ x ∈ closedBall p 0 (r₁ * r₂)
rw [← hx, mem_closedBall_zero, map_smul_eq_mul]
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y ≤ r₁ * r₂
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : a ∈ Metric.closedBall 0 r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y ≤ r₁ * r₂
rw [mem_closedBall_zero_iff] at ha
case intro.intro.intro.intro.b0
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ 0 ≤ r₁

case intro.intro.intro.intro.h₂
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ↑p y ≤ r₂
case intro.intro.intro.intro
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y ≤ r₁ * r₂
gcongr
no goals
case intro.intro.intro.intro.b0
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ 0 ≤ r₁
exact (norm_nonneg a).trans ha
no goals
case intro.intro.intro.intro.h₂
R : Type ?u.1129059
R' : Type ?u.1129062
𝕜 : Type u_1
𝕜₂ : Type ?u.1129068
𝕜₃ : Type ?u.1129071
𝕝 : Type ?u.1129074
E : Type u_2
E₂ : Type ?u.1129080
E₃ : Type ?u.1129083
F : Type ?u.1129086
G : Type ?u.1129089
ι : Type ?u.1129092
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x : E
a : 𝕜
y : E
ha : ‖a‖ ≤ r₁
hy : y ∈ closedBall p 0 r₂
hx : a • y = x
⊢ ↑p y ≤ r₂
exact p.mem_closedBall_zero.mp hy