sorry_proof
R : Type
inst✝⁴ : RealScalar R
inst✝³ : MeasureSpace R
X : Type u_1
inst✝² : AddCommGroup X
inst✝¹ : Module R X
inst✝ : Module ℝ X
x y : X
θ : R
h : θ ∈ Set.Ioo 0 1
this : θ ≠ 0
⊢ 1 - θ ≠ 0
no goals