-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem finite_of_discr_bdd_of_isReal :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F} |
      haveI :  NumberField K := @NumberField.mk _ _ inferInstance K.prop
      {w : InfinitePlace K | IsReal w}.Nonempty ∧ |discr K| ≤ N }.Finite

Proof state:
case intro.intro.refine_4
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : IntermediateField.lift ⊤ = IntermediateField.lift ℚ⟮↑x⟯
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(B ⊔ 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = ℚ⟮↑↑x⟯

Tactic:
convert hx₁

Result:
case h.e'_2
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : IntermediateField.lift ⊤ = IntermediateField.lift ℚ⟮↑x⟯
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(B ⊔ 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ K = IntermediateField.lift ⊤

case h.e'_3
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : IntermediateField.lift ⊤ = IntermediateField.lift ℚ⟮↑x⟯
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(B ⊔ 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
⊢ ℚ⟮↑↑x⟯ = IntermediateField.lift ℚ⟮↑x⟯

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
⊢ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}.Finite

Tactic:
refine finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
    (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)

Result:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₁ : {w | w.IsReal}.Nonempty
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
⊢ ∃
    x ∈
      ⋃ f,
        ⋃ (_ : f.natDegree ≤ D ∧ ∀ (i : ℕ), f.coeff i ∈ Set.Icc (-↑C) ↑C),
          ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset,
    ↑⟨K, hK₀⟩ = ℚ⟮x⟯

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₁ : {w | w.IsReal}.Nonempty
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this : CharZero ↥K
⊢ ∃ x,
    (∃ i,
        ∃ (_ : i.natDegree ≤ D ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Set.Icc (-↑C) ↑C),
          x ∈ ↑(Polynomial.map (algebraMap ℤ A) i).roots.toFinset) ∧
      K = ℚ⟮x⟯

Tactic:
haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀

Result:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₁ : {w | w.IsReal}.Nonempty
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝ : CharZero ↥K
this : NumberField ↥K
⊢ ∃ x,
    (∃ i,
        ∃ (_ : i.natDegree ≤ D ∧ ∀ (i_1 : ℕ), i.coeff i_1 ∈ Set.Icc (-↑C) ↑C),
          x ∈ ↑(Polynomial.map (algebraMap ℤ A) i).roots.toFinset) ∧
      K = ℚ⟮x⟯