E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = ⋃ (x : E) (_ : x ∈ s), ball x δ
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = thickening δ s
rw [thickening_eq_biUnion_ball]
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s = ⋃ (i : E) (_ : i ∈ s), {i}

case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s * ball 1 δ = ⋃ (x : E) (_ : x ∈ s), ball x δ
convert iUnion₂_mul (fun x (_ : x ∈ s) => {x}) (ball (1 : E) δ)
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
case h.e'_2.h.e'_5
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ s = ⋃ (i : E) (_ : i ∈ s), {i}

case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
exact s.biUnion_of_singleton.symm
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝² y x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
case h.e'_3.h.e'_3.h.f
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ
ext x
no goals
case h.e'_3.h.e'_3.h.f.h
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x✝² y x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
simp_rw [singleton_mul_ball, mul_one]