case intro.intro.intro.intro
R : Type ?u.874093
R' : Type ?u.874096
𝕜 : Type u_1
𝕜₂ : Type ?u.874102
𝕜₃ : Type ?u.874105
𝕝 : Type ?u.874108
E : Type u_2
E₂ : Type ?u.874114
E₃ : Type ?u.874117
F : Type ?u.874120
G : Type ?u.874123
ι : Type ?u.874126
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₁ ∈ ball p x₁ r₁
hy₂ : y₂ ∈ ball p x₂ r₂
⊢ (fun x x_1 => x + x_1) y₁ y₂ ∈ ball p (x₁ + x₂) (r₁ + r₂)
R : Type ?u.874093
R' : Type ?u.874096
𝕜 : Type u_1
𝕜₂ : Type ?u.874102
𝕜₃ : Type ?u.874105
𝕝 : Type ?u.874108
E : Type u_2
E₂ : Type ?u.874114
E₃ : Type ?u.874117
F : Type ?u.874120
G : Type ?u.874123
ι : Type ?u.874126
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r : ℝ
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ : E
⊢ ball p x₁ r₁ + ball p x₂ r₂ ⊆ ball p (x₁ + x₂) (r₁ + r₂)
rintro x ⟨y₁, y₂, hy₁, hy₂, rfl⟩
case intro.intro.intro.intro
R : Type ?u.874093
R' : Type ?u.874096
𝕜 : Type u_1
𝕜₂ : Type ?u.874102
𝕜₃ : Type ?u.874105
𝕝 : Type ?u.874108
E : Type u_2
E₂ : Type ?u.874114
E₃ : Type ?u.874117
F : Type ?u.874120
G : Type ?u.874123
ι : Type ?u.874126
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₁ ∈ ball p x₁ r₁
hy₂ : y₂ ∈ ball p x₂ r₂
⊢ ↑p (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂
case intro.intro.intro.intro
R : Type ?u.874093
R' : Type ?u.874096
𝕜 : Type u_1
𝕜₂ : Type ?u.874102
𝕜₃ : Type ?u.874105
𝕝 : Type ?u.874108
E : Type u_2
E₂ : Type ?u.874114
E₃ : Type ?u.874117
F : Type ?u.874120
G : Type ?u.874123
ι : Type ?u.874126
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₁ ∈ ball p x₁ r₁
hy₂ : y₂ ∈ ball p x₂ r₂
⊢ (fun x x_1 => x + x_1) y₁ y₂ ∈ ball p (x₁ + x₂) (r₁ + r₂)
rw [mem_ball, add_sub_add_comm]
no goals
case intro.intro.intro.intro
R : Type ?u.874093
R' : Type ?u.874096
𝕜 : Type u_1
𝕜₂ : Type ?u.874102
𝕜₃ : Type ?u.874105
𝕝 : Type ?u.874108
E : Type u_2
E₂ : Type ?u.874114
E₃ : Type ?u.874117
F : Type ?u.874120
G : Type ?u.874123
ι : Type ?u.874126
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₁ ∈ ball p x₁ r₁
hy₂ : y₂ ∈ ball p x₂ r₂
⊢ ↑p (y₁ - x₁ + (y₂ - x₂)) < r₁ + r₂
exact (map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)