-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ :=
  ⌈HPow.hPow (α := ℝ≥0) (max ((sqrt : (a : ℝ≥0) → ℝ≥0) (1 + HPow.hPow (β := ℕ) B 2)) 1 : ℝ≥0) D *
      (↑(D.choose (D / 2)) : ℝ≥0)⌉₊
x : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
h :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      Set.Nonempty.{u_2} (α := InfinitePlace ↥(↑K : IntermediateField ℚ A))
          {w : InfinitePlace ↥(↑K : IntermediateField ℚ A) | w.IsComplex} ∧
        |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
hK₂ :
  |discr.{u_2}
        ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
            IntermediateField ℚ A)| ≤
    (↑N : ℤ)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
w₀ :
  InfinitePlace
    ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
        IntermediateField ℚ A)
hw₀ :
  Membership.mem (γ :=
    Set
      (InfinitePlace
        ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
            IntermediateField ℚ A)))
    {w :
      InfinitePlace
        ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
            IntermediateField ℚ A) |
      w.IsComplex}
    w₀
suffices : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
⊢ ∃ (x : A),
    (∃ (i : ℤ[X]) (_ :
        i.natDegree ≤ D ∧ ∀ (i_1 : ℕ), Membership.mem (γ := Set ℤ) (Set.Icc (-(↑C : ℤ)) (↑C : ℤ)) (i.coeff i_1)),
        x ∈ (↑(roots (Polynomial.map (algebraMap ℤ A) i)).toFinset : Set A)) ∧
      K = ℚ⟮x⟯

Tactic:
suffices minkowskiBound K ↑1 < (convexBodyLT'Factor K) * boundOfDiscBdd N by
    obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isComplex K hw₀ this
    have hx := x.isIntegral_coe
    refine ⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩
    · exact natDegree_le_rankOfDiscrBdd hK₂ x hx₁
    · rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
      refine (Eq.trans_le ?_ <| Embeddings.coeff_bdd_of_norm_le
          ((le_iff_le (x : K) _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_
      · rw [minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx, coeff_map, eq_intCast,
          Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
      · refine le_trans ?_ (Nat.le_ceil _)
        rw [val_eq_coe, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one,
          Real.coe_sqrt, NNReal.coe_add 1, NNReal.coe_one, NNReal.coe_pow]
        gcongr
        · exact le_max_right _ 1
        · exact rank_le_rankOfDiscrBdd hK₂
        · rw [NNReal.coe_natCast, Nat.cast_le]
          exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans
            (Nat.choose_le_middle _ _)
    · refine mem_rootSet.mpr ⟨minpoly.ne_zero hx, ?_⟩
      exact (aeval_algebraMap_eq_zero_iff A (x : K) _).mpr (minpoly.aeval ℤ (x : K))
    · rw [← (IntermediateField.lift_injective _).eq_iff, eq_comm] at hx₁
      convert! hx₁
      · simp only [IntermediateField.lift_top]
      · simp only [IntermediateField.lift_adjoin, Set.image_singleton]