[GOAL]
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : Set.Nonempty s
⊢ ContractibleSpace ↑s
[PROOFSTEP]
refine'
  (contractible_iff_id_nullhomotopic s).2
    ⟨⟨x, h.mem hne⟩, ⟨⟨⟨fun p => ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), _⟩, _⟩, fun x => _, fun x => _⟩⟩⟩
[GOAL]
case refine'_1
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : Set.Nonempty s
p : ↑unitInterval × ↑s
⊢ ↑p.fst • x + (1 - ↑p.fst) • ↑p.snd ∈ s
[PROOFSTEP]
exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel'_right _ _)
[GOAL]
case refine'_2
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : Set.Nonempty s
⊢ Continuous fun p =>
    { val := ↑p.fst • x + (1 - ↑p.fst) • ↑p.snd, property := (_ : ↑p.fst • x + (1 - ↑p.fst) • ↑p.snd ∈ s) }
[PROOFSTEP]
exact
  ((continuous_subtype_val.fst'.smul continuous_const).add
        ((continuous_const.sub continuous_subtype_val.fst').smul continuous_subtype_val.snd')).subtype_mk
    _
[GOAL]
case refine'_3
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : Set.Nonempty s
x : ↑s
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun p =>
        { val := ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd, property := (_ : ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd ∈ s) })
      (0, x) =
    ↑(ContinuousMap.id ↑s) x
[PROOFSTEP]
ext1
[GOAL]
case refine'_3.a
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : Set.Nonempty s
x : ↑s
⊢ ↑(ContinuousMap.toFun
        (ContinuousMap.mk fun p =>
          { val := ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd, property := (_ : ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd ∈ s) })
        (0, x)) =
    ↑(↑(ContinuousMap.id ↑s) x)
[PROOFSTEP]
simp
[GOAL]
case refine'_4
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : Set.Nonempty s
x : ↑s
⊢ ContinuousMap.toFun
      (ContinuousMap.mk fun p =>
        { val := ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd, property := (_ : ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd ∈ s) })
      (1, x) =
    ↑(ContinuousMap.const ↑s { val := x✝, property := (_ : x✝ ∈ s) }) x
[PROOFSTEP]
ext1
[GOAL]
case refine'_4.a
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
s : Set E
x✝ : E
h : StarConvex ℝ x✝ s
hne : Set.Nonempty s
x : ↑s
⊢ ↑(ContinuousMap.toFun
        (ContinuousMap.mk fun p =>
          { val := ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd, property := (_ : ↑p.fst • x✝ + (1 - ↑p.fst) • ↑p.snd ∈ s) })
        (1, x)) =
    ↑(↑(ContinuousMap.const ↑s { val := x✝, property := (_ : x✝ ∈ s) }) x)
[PROOFSTEP]
simp
