awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
simp_rw :
  (sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0) * HPow.hPow (α := ℝ≥0) 2 (rankOfDiscrBdd N) + 1 - 1 <
    (sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0) * HPow.hPow (α := ℝ≥0) 2 (rankOfDiscrBdd N) + 1
simp_rw₁ :
  (sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0) * HPow.hPow (α := ℝ≥0) 2 (rankOfDiscrBdd N) <
    (sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0) * HPow.hPow (α := ℝ≥0) 2 (rankOfDiscrBdd N) + 1
simp_rw₂ : LT.lt (α := ℝ≥0) 0 1
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N

Tactic:
simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]

Premises used: lt_add_iff_pos_right, NumberField.hermiteTheorem.boundOfDiscBdd, zero_lt_one, add_tsub_cancel_right
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N

Tactic:
have : boundOfDiscBdd N - 1 < boundOfDiscBdd N := by
    simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 < (↑(boundOfDiscBdd N) : ℝ≥0∞)

Tactic:
lt_of_le_of_lt ?_ (coe_lt_coe.mpr this)

Premises used: Iff.mpr, lt_of_le_of_lt, ENNReal.coe_lt_coe
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
refine : minkowskiBound K 1 ≤ (↑(boundOfDiscBdd N - 1) : ℝ≥0∞)
⊢ minkowskiBound K 1 < (↑(boundOfDiscBdd N) : ℝ≥0∞)

Tactic:
refine lt_of_le_of_lt ?_ (coe_lt_coe.mpr this)
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
rw rw₁ : (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) = (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞)
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) = 1 * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
rw :
  HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞) *
      HPow.hPow (α := ℝ≥0∞) 2 (finrank ℚ K) ≤
    1 * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) 2 (rankOfDiscrBdd N)
⊢ minkowskiBound K 1 ≤ (↑(boundOfDiscBdd N - 1) : ℝ≥0∞)

Tactic:
rw [minkowskiBound, volume_fundamentalDomain_fractionalIdealLatticeBasis, boundOfDiscBdd,
    add_tsub_cancel_right, Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one,
    ENNReal.ofReal_one, one_mul, mixedEmbedding.finrank, volume_fundamentalDomain_latticeBasis,
    coe_mul, ENNReal.coe_pow, coe_ofNat, show sqrt N = (1 : ℝ≥0∞) * sqrt N by rw [one_mul]]

Premises used: NumberField.mixedEmbedding.minkowskiBound, NumberField.hermiteTheorem.boundOfDiscBdd, ENNReal.ofReal_one, ENNReal.coe_mul, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, ENNReal.coe_pow, Units.val_one, NumberField.mixedEmbedding.finrank, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, add_tsub_cancel_right, ENNReal.coe_ofNat, one_mul, Rat.cast_one, FractionalIdeal.absNorm_one
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) ≤ 1
h₂ : ‖discr K‖₊ ≤ (↑N : ℝ≥0)
h₃ : LE.le (α := ℝ≥0∞) 1 2
h₄ : finrank ℚ K ≤ rankOfDiscrBdd N
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) ‖discr K‖₊) : ℝ≥0∞) *
      HPow.hPow (α := ℝ≥0∞) 2 (finrank ℚ K) ≤
    1 * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) 2 (rankOfDiscrBdd N)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ LE.le (α := ℝ≥0∞) 0 2⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ LE.le (α := ℝ≥0∞) 2⁻¹ 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) ≤ 1

Tactic:
exact pow_le_one₀ (by positivity) (by simp)

Premises used: pow_le_one₀
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : (↑‖discr K‖₊ : ℝ) ≤ (↑(↑N : ℝ≥0) : ℝ)
h₂ : ‖discr K‖ ≤ (↑(↑N : ℝ≥0) : ℝ)
h₃ : |(↑(discr K) : ℝ)| ≤ (↑(↑N : ℝ≥0) : ℝ)
h₄ : (↑|discr K| : ℝ) ≤ (↑(↑N : ℝ≥0) : ℝ)
h₅ : LE.le (α := ℝ) (↑|discr K| : ℝ) (↑N : ℝ)
h₆ : LE.le (α := ℝ) (↑|discr K| : ℝ) (↑(↑N : ℤ) : ℝ)
h₇ h₈ h₉ h₁₀ : |discr K| ≤ (↑N : ℤ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)

Tactic:
rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs,
      NNReal.coe_natCast, ← Int.cast_natCast, Int.cast_le]

Premises used: Int.cast_natCast, Int.cast_abs, Int.cast_le, Int.norm_eq_abs, NNReal.coe_natCast, coe_nnnorm, NNReal.coe_le_coe
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ LE.le (α := ℝ≥0∞) 1 2

Tactic:
one_le_two

Premises used: one_le_two
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ LE.le (α := ℝ≥0∞) 1 2

Tactic:
exact one_le_two

Premises used: one_le_two
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
rank_le_rankOfDiscrBdd hK

Premises used: NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N

Tactic:
exact rank_le_rankOfDiscrBdd hK

Premises used: NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
a : 𝓞 K
h : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
⊢ natDegree (minpoly ℤ (B := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)) = finrank ℚ K

Tactic:
rw [Field.primitive_element_iff_minpoly_natDegree_eq,
    minpoly.isIntegrallyClosed_eq_field_fractions' ℚ a.isIntegral_coe,
    (minpoly.monic a.isIntegral_coe).natDegree_map] at h

Premises used: minpoly.monic, Rat, NumberField.RingOfIntegers.isIntegral_coe, Polynomial.Monic.natDegree_map, Field.primitive_element_iff_minpoly_natDegree_eq, minpoly.isIntegrallyClosed_eq_field_fractions'
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
a : 𝓞 K
h : natDegree (minpoly ℤ (B := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)) = finrank ℚ K
⊢ natDegree (minpoly ℤ (↑a : K)) ≤ rankOfDiscrBdd N

Tactic:
h.symm ▸ rank_le_rankOfDiscrBdd hK

Premises used: Eq.rec, Eq.symm, NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
a : 𝓞 K
h : natDegree (minpoly ℤ (B := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)) = finrank ℚ K
⊢ natDegree (minpoly ℤ (↑a : K)) ≤ rankOfDiscrBdd N

Tactic:
exact h.symm ▸ rank_le_rankOfDiscrBdd 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 : ℕ := ⌈max B 1 ^ 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.IsReal} ∧
        |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, Polynomial.roots, Algebra.algebraMap, Rat, _private.0.NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal.match_2, 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, Singleton.singleton, Subtype.val, Eq, Set.iUnion, Neg.neg, _private.0.NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal.match_1
-- 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)⌉₊
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.IsReal} ∧
            |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.IsReal})
        (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.IsReal} ∧
        |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 : ℕ := ⌈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₁ :
  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.IsReal}
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 : ℕ := ⌈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₁ :
  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.IsReal}
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 : ℕ := ⌈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₁ :
  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.IsReal}
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 : ℕ := ⌈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₁ :
  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.IsReal}
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.IsReal}
        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 : ℕ := ⌈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_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∞)
obtain :
  ∀ (x : 𝓞 ↥K) (hx₁ : Eq (α := IntermediateField ℚ ↥K) ℚ⟮(↑x : ↥K)⟯ ⊤)
    (hx₂ : ∀ (w : InfinitePlace ↥K), (w : (a : ↥K) → ℝ) (↑x : ↥K) < (↑(max B 1) : ℝ)),
    ∃ (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_isReal K hw₀ this

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