-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
The The₁ The₂ The₃ The₄ :
  Set.Finite.{u_2} (α := { 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 : ℤ)}
The₅ :
  let D := rankOfDiscrBdd N;
  let B := boundOfDiscBdd N;
  let 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),
    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₁ :
          Set.Nonempty.{u_2} (α :=
            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})
        (hK₂ :
          |discr.{u_2}
                ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
                    IntermediateField ℚ A)| ≤
            (↑N : ℤ)),
        ∃ (x : A),
          Membership.mem (γ := Set A)
              (⋃ (f : ℤ[X]),
                ⋃ (_ :
                  f.natDegree ≤ D ∧ ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Set.Icc (-(↑C : ℤ)) (↑C : ℤ)) (f.coeff i)),
                  (↑(roots (Polynomial.map (algebraMap ℤ A) f)).toFinset : Set A))
              x ∧
            (↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
                IntermediateField ℚ A) =
              ℚ⟮x⟯
The₆ :
  let D := rankOfDiscrBdd N;
  let B := boundOfDiscBdd N;
  let 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),
    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₁ :
          Set.Nonempty.{u_2} (α :=
            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})
        (hK₂ :
          |discr.{u_2}
                ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
                    IntermediateField ℚ A)| ≤
            (↑N : ℤ)),
        ∃ (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⟯
The₇ :
  let D := rankOfDiscrBdd N;
  let B := boundOfDiscBdd N;
  let 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),
    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₁ :
          Set.Nonempty.{u_2} (α :=
            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})
        (hK₂ :
          |discr.{u_2}
                ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
                    IntermediateField ℚ A)| ≤
            (↑N : ℤ))
        (this : CharZero.{u_2} ↥K),
        ∃ (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⟯
The₈ :
  let D := rankOfDiscrBdd N;
  let B := boundOfDiscBdd N;
  let 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),
    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₁ :
          Set.Nonempty.{u_2} (α :=
            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})
        (hK₂ :
          |discr.{u_2}
                ↥(↑(Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀) :
                    IntermediateField ℚ A)| ≤
            (↑N : ℤ))
        (this : CharZero.{u_2} ↥K) (this : NumberField.{u_2} ↥K),
        ∃ (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⟯
The₉ :
  let D := rankOfDiscrBdd N;
  let B := boundOfDiscBdd N;
  let 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),
    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 : 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₀),
        ∃ (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⟯
The₁₀ :
  ∀ (x : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F }) (K : IntermediateField ℚ A)
    (hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K),
    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 : 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₀),
        minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
⊢ Set.Finite.{u_2} (α := { 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 : ℤ)}

Tactic:
classical
  -- The bound on the degree of the generating polynomials
  let D := rankOfDiscrBdd N
  -- The bound on the Minkowski bound
  let B := boundOfDiscBdd N
  -- The bound on the coefficients of the generating polynomials
  let C := Nat.ceil ((max (sqrt (1 + B ^ 2)) 1) ^ D * Nat.choose D (D / 2))
  refine finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
      (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)
  -- We now need to prove that each field is generated by an element of the union of the root set
  simp_rw [Set.mem_iUnion]
  -- this is purely an optimization
  have : CharZero K := SubsemiringClass.instCharZero K
  haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀
  obtain ⟨w₀, hw₀⟩ := hK₁
  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]
  calc
    minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
    _ = 1 * B := by rw [one_mul]
    _ ≤ convexBodyLT'Factor K * B := by gcongr; exact mod_cast one_le_convexBodyLT'Factor K

Premises used: Set.mem_iUnion