awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ ∃ (a : 𝓞 K),
    a ≠ 0 ∧
      (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
            HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
          √|(↑(discr K) : ℝ)|
have refine : (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
  (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
    √|(↑(discr K) : ℝ)|
Tactic: refine ⟨a, ne_zero_of_map h_nz, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : 𝓞 K
h_mem :
  Membership.mem (α := K) (γ := FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K) (↑1 : FractionalIdeal (𝓞 K)⁰ K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
h_nz : Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ) (↑1 : FractionalIdeal (𝓞 K)⁰ K)) : ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
have h_nm₁ : (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
  (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
    √|(↑(discr K) : ℝ)|
Tactic: simp_rw [Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, one_mul] at h_nm
Cleared hypotheses: h_nm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have obtain : ∀ (x : 𝓞 K) (h_nz : x ≠ 0)
  (h_bd :
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
      (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
          HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
        √|(↑(discr K) : ℝ)|),
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
Tactic: obtain ⟨x, h_nz, h_bd⟩ := exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
have rw : LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) x| : ℤ)
Tactic: rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
Tactic: have h_nm : (1 : ℝ) ≤ |Algebra.norm ℚ (x : K)| := by
    rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
    exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr h_nz)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_bd :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have h_bd₁ : 1 ≤
  (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
    √|(↑(discr K) : ℝ)|
Tactic: replace h_bd := le_trans h_nm h_bd
Cleared hypotheses: h_bd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑x : K)| : ℝ)
h_bd :
  1 ≤
    (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have rwa : 0 < (4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K).factorial : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K)
Tactic: rwa [← inv_mul_le_iff₀, inv_div, mul_one, Real.le_sqrt (by positivity) (by positivity),
    ← Int.cast_abs, div_pow, mul_pow, ← pow_mul, mul_comm _ 2, ← pow_mul, mul_comm _ 2] at h_bd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have this : HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
    ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
  (↑|discr K| : ℝ)
Tactic: have := abs_discr_ge' K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
this :
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
have rwa : ∀
  (this :
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
        ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
      (↑|discr K| : ℝ)),
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    (↑|discr K| : ℝ)
Tactic: rwa [← IsTotallyComplex.finrank] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K) : ℝ) 2 /
      (4 / π * HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹
have h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
Tactic: have h : 0 < (finrank ℚ K : ℝ) := Nat.cast_pos.mpr finrank_pos
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsTotallyComplex K
h : LT.lt (α := ℝ) 0 (↑(finrank ℚ K) : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K) : ℝ) 2 /
      (4 / π * HPow.hPow (α := ℝ) (↑(finrank ℚ K).factorial : ℝ) (HMul.hMul (α := ℝ) 2 (↑(finrank ℚ K) : ℝ)⁻¹)) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑|discr K| : ℝ) (↑(finrank ℚ K) : ℝ)⁻¹
have rw : HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
    ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
  (↑|discr K| : ℝ)
Tactic: rw [← Real.rpow_le_rpow_iff (z := finrank ℚ K) (by positivity) (by positivity) h, Real.div_rpow
    (by positivity) (by positivity), ← Real.rpow_mul (by positivity), inv_mul_cancel₀ h.ne',
    Real.rpow_one, Real.mul_rpow (by positivity) (by positivity), Real.rpow_natCast,
    Real.rpow_natCast, ← pow_mul, ← Real.rpow_mul (by positivity),
    inv_mul_cancel_right₀ h.ne', Real.rpow_two]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑|discr K| : ℝ)
have refine : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
    ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
Tactic: refine le_trans ?_ (abs_discr_ge' K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (2 * finrank ℚ K) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
have rw : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
    ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
Tactic: rw [mul_comm 2 _]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
have refine : a (finrank ℚ K) ≤
  HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
    ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
Tactic: refine le_trans (this (finrank ℚ K) h) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
have hdb : 1 ≤ 4 / π
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
hdb : 1 ≤ 4 / π
⊢ HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ finrank ℚ K * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2) ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
have hdb₁ : 2 * nrComplexPlaces K ≤ finrank ℚ K
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
this : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
⊢ 2 * nrComplexPlaces K ≤ finrank ℚ K
have hdb : nrComplexPlaces K * 2 ≤ nrRealPlaces K + nrComplexPlaces K * 2
Tactic: rw [← card_add_two_mul_card_eq_rank, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)
have suffices : ∀ (n : ℕ), 2 ≤ n → 4 / 9 * (3 * π / 4) ^ n ≤ a n
Tactic: suffices ∀ n, 2 ≤ n → (4 / 9 : ℝ) * (3 * π / 4) ^ n ≤ a n by
    refine le_trans (this (finrank ℚ K) h) ?_
    simp only [a]
    gcongr
    · exact (one_le_div Real.pi_pos).2 Real.pi_le_four
    · rw [← card_add_two_mul_card_eq_rank, mul_comm]
      exact Nat.le_add_left _ _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n : ℕ
⊢ 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 = a 2
have simp : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 =
  HPow.hPow (α := ℝ) (β := ℕ) 2 4 / (HPow.hPow (β := ℕ) (4 / π) 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2)
Tactic: simp [a, Nat.factorial_two]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)
have h₁ : a (m + 1) = a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
Tactic: convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
h₁ : a (m + 1) = a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)
have convert_2 : 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
Tactic: convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ a (m + 1) = a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
have h₁ : HPow.hPow (α := ℝ) (↑(m + 1) : ℝ) (m * 2) * (↑(m + 1) : ℝ) * (↑(m + 1) : ℝ) /
    ((4 / π) ^ m * (4 / π) *
      (HPow.hPow (α := ℝ) (β := ℕ) (↑((m + 1) * m.factorial) : ℝ) 0 * (↑((m + 1) * m.factorial) : ℝ) *
        (↑((m + 1) * m.factorial) : ℝ))) =
  HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) /
        ((4 / π) ^ m * (HPow.hPow (α := ℝ) (β := ℕ) (↑m.factorial : ℝ) 0 * (↑m.factorial : ℝ) * (↑m.factorial : ℝ))) *
      (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) /
    (4 / π)
Tactic: simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ HPow.hPow (α := ℝ) (↑(m + 1) : ℝ) (m * 2) * (↑(m + 1) : ℝ) * (↑(m + 1) : ℝ) /
      ((4 / π) ^ m * (4 / π) *
        (HPow.hPow (α := ℝ) (β := ℕ) (↑((m + 1) * m.factorial) : ℝ) 0 * (↑((m + 1) * m.factorial) : ℝ) *
          (↑((m + 1) * m.factorial) : ℝ))) =
    HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) /
          ((4 / π) ^ m * (HPow.hPow (α := ℝ) (β := ℕ) (↑m.factorial : ℝ) 0 * (↑m.factorial : ℝ) * (↑m.factorial : ℝ))) *
        (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) /
      (4 / π)
have h₁ : HPow.hPow (α := ℝ) (↑(m + 1) : ℝ) (m * 2) * HPow.hPow (α := ℝ) (β := ℕ) (↑(m + 1) : ℝ) 2 *
    HPow.hPow (α := ℝ) (β := ℕ) (↑m.factorial : ℝ) 2 =
  HPow.hPow (α := ℝ) (β := ℕ) (↑((m + 1) * m.factorial) : ℝ) 2 * HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) *
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) ^ (2 * m)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ HPow.hPow (α := ℝ) (↑(m + 1) : ℝ) (m * 2) * HPow.hPow (α := ℝ) (β := ℕ) (↑(m + 1) : ℝ) 2 *
      HPow.hPow (α := ℝ) (β := ℕ) (↑m.factorial : ℝ) 2 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑((m + 1) * m.factorial) : ℝ) 2 * HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) *
      (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) ^ (2 * m)
have h₁ : HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (m * 2) * HPow.hPow (α := ℝ) (↑m : ℝ) (2 * m) =
  HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (2 * m)
Tactic: simp [field, div_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
have convert_2 : 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
Tactic: rw [_root_.le_div_iff₀ (by positivity), pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
have h₁ : 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) = 4 / 9 * (3 * π / 4) ^ m * 3
Tactic: convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)
have succ : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
Tactic: suffices (3 : ℝ) ≤ (1 + 1 / m : ℝ) ^ (2 * m) by
        convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
        · simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
          field_simp
          simp [field, div_pow]
          ring
        · rw [_root_.le_div_iff₀ (by positivity), pow_succ]
          convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
          field
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
⊢ 3 = 1 + (↑(2 * m) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)
have simp : 3 = HAdd.hAdd (α := ℝ) 1 2
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n m : ℕ
hmn : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
⊢ 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
have succ : -2 ≤ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)
Tactic: refine le_trans (le_of_eq (by simp [field]; norm_num)) (one_add_mul_le_pow ?_ (2 * m))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ :=
  fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) (n * 2) / ((4 / π) ^ n * HPow.hPow (α := ℝ) (β := ℕ) (↑n.factorial : ℝ) 2)
n : ℕ
hn : 2 ≤ n
⊢ 4 / 9 * (3 * π / 4) ^ n ≤ a n
have base : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ a 2
Tactic: induction n, hn using Nat.le_induction with
  | base => exact le_of_eq <| by simp [a, Nat.factorial_two]; field
  | succ m _ h_m =>
      suffices (3 : ℝ) ≤ (1 + 1 / m : ℝ) ^ (2 * m) by
        convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)
        · simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
          field_simp
          simp [field, div_pow]
          ring
        · rw [_root_.le_div_iff₀ (by positivity), pow_succ]
          convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1
          field
      refine le_trans (le_of_eq (by simp [field]; norm_num)) (one_add_mul_le_pow ?_ (2 * m))
      exact le_trans (by norm_num : (-2 : ℝ) ≤ 0) (by positivity)
Cleared hypotheses: hn