x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ st x = r
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ st x = r
have h : ∃ r, IsSt x r := ⟨r, hxr⟩
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ choose h = r
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ st x = r
rw [st, dif_pos h]
no goals
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ choose h = r
exact (Classical.choose_spec h).unique hxr