Theorem: inverse (Test/Real/Inverse.lean)

State before:
x : ℝ
⊢ x ≠ 0 → ∃ y, x * y = 1
Tactic:
sorry
State after:
no goals