awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
⊢ IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)

Tactic:
have hx := x.isIntegral_coe
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥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⟯

Tactic:
⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩

Premises used: NumberField.RingOfIntegers.val, Int, minpoly, And.intro, Exists.intro, Subtype.val
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
refine_1 : natDegree (minpoly ℤ (↑x : ↥K)) ≤ D
refine_2 : ∀ (i : ℕ), Membership.mem (γ := Set ℤ) (Set.Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ (↑x : ↥K)) i)
refine_3 : (↑(↑x : ↥K) : A) ∈ (↑(roots (Polynomial.map (algebraMap ℤ A) (minpoly ℤ (↑x : ↥K)))).toFinset : Set A)
refine_4 : K = ℚ⟮(↑(↑x : ↥K) : A)⟯
⊢ ∃ (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:
refine ⟨x, ⟨⟨minpoly ℤ (x : K), ⟨?_, fun i ↦ ?_⟩, ?_⟩, ?_⟩⟩
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
⊢ natDegree (minpoly ℤ (↑x : ↥K)) ≤ D

Tactic:
natDegree_le_rankOfDiscrBdd hK₂ x hx₁

Premises used: Set.Mem, RingHom.codRestrict, NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
⊢ natDegree (minpoly ℤ (↑x : ↥K)) ≤ D

Tactic:
exact natDegree_le_rankOfDiscrBdd hK₂ x hx₁

Premises used: NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
i : ℕ
refine_2 : LE.le (α := ℝ) (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) (↑(↑C : ℤ) : ℝ)
⊢ Membership.mem (γ := Set ℤ) (Set.Icc (-(↑C : ℤ)) (↑C : ℤ)) (coeff (minpoly ℤ (↑x : ↥K)) i)

Tactic:
rw [Set.mem_Icc, ← abs_le, ← @Int.cast_le ℝ]

Premises used: Int.cast_le, abs_le, Set.mem_Icc
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
i : ℕ
⊢ LE.le (α := ℝ) (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) (↑(↑C : ℤ) : ℝ)

Tactic:
(Eq.trans_le ?_ <| Embeddings.coeff_bdd_of_norm_le
          ((le_iff_le (x : K) _).mp (fun w ↦ le_of_lt (hx₂ w))) i).trans ?_

Premises used: NumberField.InfinitePlace.le_iff_le, le_of_lt, NumberField.RingOfIntegers.val, Eq.trans_le, NumberField.Embeddings.coeff_bdd_of_norm_le, Iff.mp, LE.le.trans
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
i : ℕ
refine_2 : (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) = ‖coeff (minpoly ℚ (↑x : ↥K)) i‖
refine_2₁ :
  max (√(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)) 1 ^ finrank.{0, u_2} ℚ ↥K *
      (↑((finrank.{0, u_2} ℚ ↥K).choose (finrank.{0, u_2} ℚ ↥K / 2)) : ℝ) ≤
    (↑(↑C : ℤ) : ℝ)
⊢ LE.le (α := ℝ) (↑|coeff (minpoly ℤ (↑x : ↥K)) i| : ℝ) (↑(↑C : ℤ) : ℝ)

Tactic:
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 ?_

Premises used: NumberField.InfinitePlace.le_iff_le, le_of_lt, NumberField.RingOfIntegers.val, Eq.trans_le, NumberField.Embeddings.coeff_bdd_of_norm_le, Iff.mp, LE.le.trans
-- 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_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.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_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.IsComplex}
    w₀
this : minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞) * (↑(boundOfDiscBdd N) : ℝ≥0∞)
x : 𝓞 ↥K
hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)
hx : IsIntegral ℤ (A := ↥K) ((algebraMap (𝓞 ↥K) ↥K : (a : 𝓞 ↥K) → ↥K) x : ↥K)
i : ℕ
⊢ max (√(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)) 1 ^ finrank.{0, u_2} ℚ ↥K *
      (↑((finrank.{0, u_2} ℚ ↥K).choose (finrank.{0, u_2} ℚ ↥K / 2)) : ℝ) ≤
    (↑(↑C : ℤ) : ℝ)

Tactic:
le_trans ?_ (Nat.le_ceil _)

Premises used: Nat.le_ceil, le_trans