∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : ℝ) (x_1 : NumberField.mixedEmbedding.realSpace K)
  (x_2 : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }),
  (x • x_1) ↑x_2 - (↑(↑x_2).mult * ∑ w', (x • x_1) w') * (↑(Module.finrank ℚ K))⁻¹ =
    ((RingHom.id ℝ) x • fun w => x_1 ↑w - (↑(↑w).mult * ∑ w', x_1 w') * (↑(Module.finrank ℚ K))⁻¹) x_2