-- 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 : ℕ := ⌈max B 1 ^ D * (↑(D.choose (D / 2)) : ℝ≥0)⌉₊
x_1 : { 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.IsReal} ∧
        |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_2 : 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.IsReal}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < (↑(max B 1) : ℝ)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
i : ℕ
refine_2 :
  (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) =
    ‖(Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K))).coeff i‖
refine_2₁ :
  (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) =
    norm (E := ℚ)
      ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
          (coeff (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)) i) :
        ℚ)
refine_2₂ :
  (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) =
    norm (E := ℚ) (↑(coeff (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)) i) : ℚ)
refine_2₃ :
  (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) =
    ‖coeff (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)) i‖
refine_2₄ :
  Eq (α := ℝ) (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ)
    |(↑(coeff (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)) i) : ℝ)|
refine_2₅ refine_2₆ :
  Eq (α := ℝ) |(↑(coeff (minpoly ℤ (↑x : ↥K)) i) : ℝ)|
    |(↑(coeff (minpoly ℤ (B := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)) i) : ℝ)|
⊢ (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) = ‖coeff (minpoly ℚ (↑x : ↥K)) i‖

Tactic:
rw [minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx, coeff_map, eq_intCast,
          Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]

Premises used: Int.cast_abs, Polynomial.coeff_map, Rat, Int.norm_eq_abs, eq_intCast, Int.norm_cast_rat, minpoly.isIntegrallyClosed_eq_field_fractions'