no goals
R : Type u_1
E : Type ?u.20960
F : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ IsOpenMap ↑(homothety x t)
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹) <;> intro e <;>
  simp [← AffineMap.comp_apply, ← homothety_mul, ht]