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 ℚ A) (IntermediateField.lift (F := K) ⊤) (IntermediateField.lift (F := 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)
⊢ Eq (α := IntermediateField ℚ A) ℚ⟮(↑(↑x : ↥K) : A)⟯ (IntermediateField.lift (F := K) ℚ⟮(↑x : ↥K)⟯)

Tactic:
simp only [IntermediateField.lift_adjoin, Set.image_singleton]

Premises used: Set.image_singleton, IntermediateField.lift_adjoin
-- 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 : 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 < (↑B : ℝ≥0∞)

Tactic:
minkowskiBound_lt_boundOfDiscBdd hK₂

Premises used: NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd
-- 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 : 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₀
rw rw₁ : (↑B : ℝ≥0∞) = (↑B : ℝ≥0∞)
⊢ (↑B : ℝ≥0∞) = 1 * (↑B : ℝ≥0∞)

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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 : 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₀
bc : 1 ≤ (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞)
⊢ 1 * (↑B : ℝ≥0∞) ≤ (↑(convexBodyLT'Factor.{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 : ℕ :=
  ⌈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 : 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₀
⊢ 1 ≤ (↑(convexBodyLT'Factor.{u_2} ↥K) : ℝ≥0∞)

Tactic:
mod_cast one_le_convexBodyLT'Factor K

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

Tactic:
exact mod_cast one_le_convexBodyLT'Factor K

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

Tactic:
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: NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, NumberField.mixedEmbedding.minkowskiBound, Membership.mem, Subtype, OfNat.ofNat, NumberField.mixedEmbedding.convexBodyLT'Factor
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
⊢ Set.Finite.{u_2} (α := { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}

Tactic:
Set.Finite.subset (Set.Finite.union (finite_of_discr_bdd_of_isReal A N)
    (finite_of_discr_bdd_of_isComplex A N)) ?_

Premises used: Set.Finite.union, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, Set.Finite.subset, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
refine :
  Subset.{u_2} (α := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    ({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 : ℤ)} ∪
      {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 : ℤ)})
⊢ Set.Finite.{u_2} (α := { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}

Tactic:
refine Set.Finite.subset (Set.Finite.union (finite_of_discr_bdd_of_isReal A N)
    (finite_of_discr_bdd_of_isComplex A N)) ?_

Premises used: Set.Finite.union, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, Set.Finite.subset, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
⊢ 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 : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
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 : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
obtain :
  ∀ (w₀ : InfinitePlace ↥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.IsReal} ∧
            |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)} ∪
        {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₀)
⊢ 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 : ℤ)} ∪
      {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₀)

Tactic:
obtain ⟨w₀⟩ := (inferInstance : Nonempty (InfinitePlace K))

Premises used: inferInstance
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
N : ℕ
K : IntermediateField ℚ A
hK₀ : FiniteDimensional.{0, u_2} ℚ ↥K
hK₁ :
  Membership.mem (γ := Set { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F })
    {K : { F : IntermediateField ℚ A // FiniteDimensional.{0, u_2} ℚ ↥F } |
      |discr.{u_2} ↥(↑K : IntermediateField ℚ A)| ≤ (↑N : ℤ)}
    (Subtype.mk (p := fun (F : IntermediateField ℚ A) ↦ FiniteDimensional.{0, u_2} ℚ ↥F) K hK₀)
this_1 : CharZero.{u_2} ↥K
this : NumberField.{u_2} ↥K
w₀ : InfinitePlace ↥K
pos :
  ∀ (hw₀ : w₀.IsReal),
    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 : ℤ)} ∪
        {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₀)
neg :
  ∀ (hw₀ : ¬w₀.IsReal),
    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 : ℤ)} ∪
        {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₀)
⊢ 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 : ℤ)} ∪
      {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₀)

Tactic:
by_cases hw₀ : IsReal w₀

Premises used: NumberField.InfinitePlace.IsReal