Lean: α⁻¹ is algebraic via Polynomial.reverse and eval₂_reverse_eq_zero_iff

To transfer a Liouville-type bound from an algebraic α to α⁻¹ in Mathlib: create an instance with let _ := invertibleOfNonzero hα0 (inside a proof the style linter prefers let over letI), then rw [Polynomial.eval_map, ← invOf_eq_inv, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.eval_map, fα] proves (f.reverse.map (algebraMap ℤ ℝ)).eval α⁻¹ = 0. Nonvanishing is mt Polynomial.reverse_eq_zero.1 f0, irrationality is hirr.inv. Then Liouville.exists_pos_real_of_irrational_root applies to α⁻¹ directly. Its form 1 ≤ (b+1)^d·(|α − a/(b+1)|·A) converts to |qα − a| ≥ (1/A)/q^{d+1} for all q ≥ 1.