ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
⊢ y ∈ ↑(homothety x t) '' interior s
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
⊢ closure s ⊆ ↑(homothety x t) '' interior s
intro y hy
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ y ∈ ↑(homothety x t) '' interior s
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
⊢ y ∈ ↑(homothety x t) '' interior s
have hne : t ≠ 0 := (one_pos.trans ht).ne'
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(homothety x t⁻¹) y ∈ openSegment ℝ x y
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ y ∈ ↑(homothety x t) '' interior s
refine'
  ⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy _,
    (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(lineMap x y) t⁻¹ ∈ (fun x_1 => ↑(lineMap x y) x_1⁻¹) '' Ioi 1
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(homothety x t⁻¹) y ∈ openSegment ℝ x y
rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi (zero_lt_one' ℝ), ← image_inv, image_image,
  homothety_eq_lineMap]
no goals
ι : Type ?u.164256
𝕜 : Type ?u.164259
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ ↑(lineMap x y) t⁻¹ ∈ (fun x_1 => ↑(lineMap x y) x_1⁻¹) '' Ioi 1
exact mem_image_of_mem _ ht