case intro.intro.intro.intro
R : Type ?u.878378
R' : Type ?u.878381
𝕜 : Type u_1
𝕜₂ : Type ?u.878387
𝕜₃ : Type ?u.878390
𝕝 : Type ?u.878393
E : Type u_2
E₂ : Type ?u.878399
E₃ : Type ?u.878402
F : Type ?u.878405
G : Type ?u.878408
ι : Type ?u.878411
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ y₂ : E
hy₁ : y₁ ∈ closedBall p x₁ r₁
hy₂ : y₂ ∈ closedBall p x₂ r₂
⊢ (fun x x_1 => x + x_1) y₁ y₂ ∈ closedBall p (x₁ + x₂) (r₁ + r₂)
R : Type ?u.878378
R' : Type ?u.878381
𝕜 : Type u_1
𝕜₂ : Type ?u.878387
𝕜₃ : Type ?u.878390
𝕝 : Type ?u.878393
E : Type u_2
E₂ : Type ?u.878399
E₃ : Type ?u.878402
F : Type ?u.878405
G : Type ?u.878408
ι : Type ?u.878411
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ : E
⊢ closedBall p x₁ r₁ + closedBall p x₂ r₂ ⊆ closedBall p (x₁ + x₂) (r₁ + r₂)
rintro x ⟨y₁, y₂, hy₁, hy₂, rfl⟩
case intro.intro.intro.intro
R : Type ?u.878378
R' : Type ?u.878381
𝕜 : Type u_1
𝕜₂ : Type ?u.878387
𝕜₃ : Type ?u.878390
𝕝 : Type ?u.878393
E : Type u_2
E₂ : Type ?u.878399
E₃ : Type ?u.878402
F : Type ?u.878405
G : Type ?u.878408
ι : Type ?u.878411
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ y₂ : E
hy₁ : y₁ ∈ closedBall p x₁ r₁
hy₂ : y₂ ∈ closedBall p x₂ r₂
⊢ ↑p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂
case intro.intro.intro.intro
R : Type ?u.878378
R' : Type ?u.878381
𝕜 : Type u_1
𝕜₂ : Type ?u.878387
𝕜₃ : Type ?u.878390
𝕝 : Type ?u.878393
E : Type u_2
E₂ : Type ?u.878399
E₃ : Type ?u.878402
F : Type ?u.878405
G : Type ?u.878408
ι : Type ?u.878411
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ y₂ : E
hy₁ : y₁ ∈ closedBall p x₁ r₁
hy₂ : y₂ ∈ closedBall p x₂ r₂
⊢ (fun x x_1 => x + x_1) y₁ y₂ ∈ closedBall p (x₁ + x₂) (r₁ + r₂)
rw [mem_closedBall, add_sub_add_comm]
no goals
case intro.intro.intro.intro
R : Type ?u.878378
R' : Type ?u.878381
𝕜 : Type u_1
𝕜₂ : Type ?u.878387
𝕜₃ : Type ?u.878390
𝕝 : Type ?u.878393
E : Type u_2
E₂ : Type ?u.878399
E₃ : Type ?u.878402
F : Type ?u.878405
G : Type ?u.878408
ι : Type ?u.878411
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ y₂ : E
hy₁ : y₁ ∈ closedBall p x₁ r₁
hy₂ : y₂ ∈ closedBall p x₂ r₂
⊢ ↑p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂
exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)