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 : ℕ := ⌈max B 1 ^ 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.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 : 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₀
bc : 1 ≤ (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞)
⊢ 1 * (↑B : ℝ≥0∞) ≤ (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞) * (↑B : ℝ≥0∞)

Tactic:
gcongr
-- 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 : { 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 : 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₀
⊢ 1 ≤ (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞)

Tactic:
mod_cast one_le_convexBodyLTFactor K

Premises used: NumberField.mixedEmbedding.one_le_convexBodyLTFactor, ENNReal.ofNNReal, ENNReal.natCast_le_ofNNReal._simp_1, congrArg, cast, Membership.mem, Subtype, LE.le, NumberField.mixedEmbedding.convexBodyLTFactor, congrFun', Eq.symm, Nat.cast_one, Eq.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 : ℕ := ⌈max B 1 ^ 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.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 : 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₀
⊢ 1 ≤ (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞)

Tactic:
exact mod_cast one_le_convexBodyLTFactor K

Premises used: NumberField.mixedEmbedding.one_le_convexBodyLTFactor, Membership.mem, Subtype
-- 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 : { 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 : 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₀
minkowskiBound : (↑B : ℝ≥0∞) = 1 * (↑B : ℝ≥0∞)
minkowskiBound₁ : 1 * (↑B : ℝ≥0∞) ≤ (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞) * (↑B : ℝ≥0∞)
⊢ mixedEmbedding.minkowskiBound.{u_2} (↥K) 1 < (↑(convexBodyLTFactor.{u_2} ↥K) : ℝ≥0∞) * (↑B : ℝ≥0∞)

Tactic:
calc
    minkowskiBound K 1 < B := minkowskiBound_lt_boundOfDiscBdd hK₂
    _ = 1 * B := by rw [one_mul]
    _ ≤ convexBodyLTFactor K * B := by gcongr; exact mod_cast one_le_convexBodyLTFactor K

Premises used: NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, NumberField.mixedEmbedding.minkowskiBound, Membership.mem, Subtype, NumberField.mixedEmbedding.convexBodyLTFactor, OfNat.ofNat
-- 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)⌉₊
⊢ 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:
finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
      (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)

Premises used: Multiset.toFinset, _private.0.NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex.match_1, Polynomial.roots, Algebra.algebraMap, Rat, Membership.mem, Polynomial.bUnion_roots_finite, Exists, NumberField.hermiteTheorem.finite_of_finite_generating_set, Int, Set.finite_Icc, Nat.cast, Subtype.mk, And, SetLike.coe, IntermediateField.adjoin, Polynomial.map, _private.0.NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex.match_2, Singleton.singleton, Subtype.val, Eq, Set.iUnion, Neg.neg
-- 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)⌉₊
refine :
  ∀ (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⟯
⊢ 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:
refine finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
      (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)
-- 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₁ :
  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 : ℤ)
simp_rw :
  ∃ (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⟯
⊢ ∃ (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⟯

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- 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₁ :
  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 : ℤ)
⊢ CharZero.{u_2} ↥K

Tactic:
have : CharZero K := SubsemiringClass.instCharZero K
-- 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₁ :
  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
⊢ NumberField.{u_2} ↥K

Tactic:
haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀
-- 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₁ :
  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_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
obtain :
  ∀
    (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⟯
⊢ ∃ (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:
obtain ⟨w₀, hw₀⟩ := hK₁
-- 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_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∞)
obtain :
  ∀ (x : 𝓞 ↥K) (hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤)
    (hx₂ :
      ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < √(1 + HPow.hPow (β := ℕ) (↑(boundOfDiscBdd N) : ℝ) 2)),
    ∃ (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⟯
⊢ ∃ (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:
obtain ⟨x, hx₁, hx₂⟩ := exists_primitive_element_lt_of_isComplex K hw₀ this

Premises used: NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, Membership.mem, Subtype