case intro.intro
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ closedBall p 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ closedBall p 0 r
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (closedBall p 0 r)
rintro a ha x ⟨y, hy, hx⟩
case intro.intro
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ closedBall p 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * ↑p y ≤ r
case intro.intro
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ closedBall p 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ closedBall p 0 r
rw [mem_closedBall_zero, ← hx, map_smul_eq_mul]
no goals
case intro.intro
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ closedBall p 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * ↑p y ≤ r
calc
  _ ≤ p y := mul_le_of_le_one_left (map_nonneg p _) ha
  _ ≤ r := by rwa [mem_closedBall_zero] at hy
no goals
R : Type ?u.1062708
R' : Type ?u.1062711
𝕜 : Type u_1
𝕜₂ : Type ?u.1062717
𝕜₃ : Type ?u.1062720
𝕝 : Type ?u.1062723
E : Type u_2
E₂ : Type ?u.1062729
E₃ : Type ?u.1062732
F : Type ?u.1062735
G : Type ?u.1062738
ι : Type ?u.1062741
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ closedBall p 0 r
hx : (fun x => a • x) y = x
⊢ ↑p y ≤ r
rwa [mem_closedBall_zero] at hy