Dimitrov's lower bound for the house of a nonzero algebraic integer that is not a root of unity

Problem statement

Notes: Statement-only benchmark problem. The theorem uses Mathlib's NumberField.house and IsOfFinOrder.

Source: James McKee and Chris Smyth, Around the Unit Circle, Chapter 4, Theorem 4.1; Vesselin Dimitrov (2019).

Informal solution: Dimitrov's proof of the Schinzel--Zassenhaus conjecture.

theorem declaration uses `sorry`dimitrov {K : Type*} [Field K] [NumberField K]
    (α : K)
    (α_int : IsIntegral ℤ α)
    (α_ne_zero : α ≠ 0)
    (α_not_rootOfUnity : ¬ IsOfFinOrder α) :
    (2 : ℝ) ^ (1 / (4 * (Finset.univ.image fun σ : K →+* ℂ ↦ (σ α).arg).card) : ℝ) ≤
      NumberField.house α := byK:Type u_1inst✝¹:Field Kinst✝:NumberField Kα:Kα_int:IsIntegral ℤ αα_ne_zero:α ≠ 0α_not_rootOfUnity:¬IsOfFinOrder α⊢ 2 ^ (1 / (4 * ↑(Finset.image (fun σ => (σ α).arg) Finset.univ).card)) ≤ NumberField.house α
  sorryAll goals completed! 🐙