case inl
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r

case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r
cases' hr.lt_or_lt with hr hr
case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r
case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r
refine' Subset.antisymm _ ball_subset_interior_closedBall
case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r
case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r
intro y hy
case inr.inl
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝¹ : r ≠ 0
hr✝ : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r

case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
case inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r
rcases (mem_closedBall.1 <| interior_subset hy).lt_or_eq with (hr | rfl)
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ y ∈ ball x (dist y x)
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
set f : ℝ → E := fun c : ℝ => c • (y - x) + x
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ y ∈ ball x (dist y x)
suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
  have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const
  have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa
  have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
    interior_mono this (preimage_interior_subset_interior_preimage hfc hf1)
  contrapose h1
  simp
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
⊢ f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
intro c hc
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1
rw [mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← mul_le_mul_right hr]
no goals
case inr.inr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
simpa [dist_eq_norm, norm_smul] using hc
no goals
case inl
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r
rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]
no goals
case inr.inl
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝¹ : r ≠ 0
hr✝ : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
hr : dist y x < r
⊢ y ∈ ball x r
exact hr
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ y ∈ ball x (dist y x)
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ y ∈ ball x (dist y x)
have hfc : Continuous f := (continuous_id.smul continuous_const).add continuous_const
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ y ∈ ball x (dist y x)
have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : 1 ∈ interior (Icc (-1) 1)
⊢ y ∈ ball x (dist y x)
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
  interior_mono this (preimage_interior_subset_interior_preimage hfc hf1)
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : ¬y ∈ ball x (dist y x)
⊢ ¬1 ∈ interior (Icc (-1) 1)
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : 1 ∈ interior (Icc (-1) 1)
⊢ y ∈ ball x (dist y x)
contrapose h1
no goals
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
h1 : ¬y ∈ ball x (dist y x)
⊢ ¬1 ∈ interior (Icc (-1) 1)
simp
no goals
α : Type ?u.47288
β : Type ?u.47291
γ : Type ?u.47294
ι : Type ?u.47297
inst✝⁶ : NormedField α
inst✝⁵ : SeminormedAddCommGroup β
E : Type u_1
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace α E
F : Type ?u.47328
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace α F
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
simpa