R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ • ball p 0 r₂ → x ∈ ball p 0 (r₁ * r₂)
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ • ball p 0 r₂ ⊆ ball p 0 (r₁ * r₂)
rw [Set.subset_def]
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ • ball p 0 r₂
⊢ x ∈ ball p 0 (r₁ * r₂)
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ • ball p 0 r₂ → x ∈ ball p 0 (r₁ * r₂)
intro x hx
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ ∧ y ∈ ball p 0 r₂ ∧ x_1 • y = x
⊢ x ∈ ball p 0 (r₁ * r₂)
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ • ball p 0 r₂
⊢ x ∈ ball p 0 (r₁ * r₂)
rw [Set.mem_smul] at hx
case intro.intro.intro.intro
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ x ∈ ball p 0 (r₁ * r₂)
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁ ∧ y ∈ ball p 0 r₂ ∧ x_1 • y = x
⊢ x ∈ ball p 0 (r₁ * r₂)
rcases hx with ⟨a, y, ha, hy, hx⟩
case intro.intro.intro.intro
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y < r₁ * r₂
case intro.intro.intro.intro
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ x ∈ ball p 0 (r₁ * r₂)
rw [← hx, mem_ball_zero, map_smul_eq_mul]
case intro.intro.intro.intro.a
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ‖a‖ < r₁

case intro.intro.intro.intro.a
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ↑p y < r₂
case intro.intro.intro.intro
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ‖a‖ * ↑p y < r₁ * r₂
gcongr
no goals
case intro.intro.intro.intro.a
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ‖a‖ < r₁
exact mem_ball_zero_iff.mp ha
no goals
case intro.intro.intro.intro.a
R : Type ?u.1107787
R' : Type ?u.1107790
𝕜 : Type u_1
𝕜₂ : Type ?u.1107796
𝕜₃ : Type ?u.1107799
𝕝 : Type ?u.1107802
E : Type u_2
E₂ : Type ?u.1107808
E₃ : Type ?u.1107811
F : Type ?u.1107814
G : Type ?u.1107817
ι : Type ?u.1107820
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.ball 0 r₁
hy : y ∈ ball p 0 r₂
hx : a • y = x
⊢ ↑p y < r₂
exact p.mem_ball_zero.mp hy