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
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)

Tactic:
le_trans (this (finrank ℚ K) h) ?_

Premises used: Rat, Module.finrank, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
refine :
  a (finrank ℚ K) ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).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)

Tactic:
refine le_trans (this (finrank ℚ K) h) ?_

Premises used: Rat, Module.finrank, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
simp :
  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)
⊢ a (finrank ℚ K) ≤
    HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K * 2) /
      ((4 / π) ^ (2 * nrComplexPlaces K) * HPow.hPow (α := ℝ) (β := ℕ) (↑(finrank ℚ K).factorial : ℝ) 2)

Tactic:
simp only [a]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 / π
hdb₁ : 2 * nrComplexPlaces K ≤ finrank ℚ K
⊢ 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)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ 1 ≤ 4 / π

Tactic:
(one_le_div Real.pi_pos).2 Real.pi_le_four

Premises used: Iff.mpr, Real.pi_le_four, Real.pi_pos, one_le_div
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ 1 ≤ 4 / π

Tactic:
exact (one_le_div Real.pi_pos).2 Real.pi_le_four

Premises used: Iff.mpr, Real.pi_le_four, Real.pi_pos, one_le_div
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 : nrComplexPlaces K * 2 ≤ nrRealPlaces K + nrComplexPlaces K * 2
⊢ 2 * nrComplexPlaces K ≤ finrank ℚ K

Tactic:
rw [← card_add_two_mul_card_eq_rank, mul_comm]

Premises used: mul_comm, NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ nrComplexPlaces K * 2 ≤ nrRealPlaces K + nrComplexPlaces K * 2

Tactic:
Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ nrComplexPlaces K * 2 ≤ nrRealPlaces K + nrComplexPlaces K * 2

Tactic:
exact Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
suffices : ∀ (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)

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 _ _
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 : ℕ
simp :
  4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 =
    HPow.hPow (α := ℝ) (β := ℕ) 2 4 / (HPow.hPow (β := ℕ) (4 / π) 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2)
⊢ 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 = a 2

Tactic:
simp [a, Nat.factorial_two]

Premises used: Nat.factorial_two
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 =
    HPow.hPow (α := ℝ) (β := ℕ) 2 4 / (HPow.hPow (β := ℕ) (4 / π) 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2)

Tactic:
field
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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

Tactic:
exact le_of_eq <| by simp [a, Nat.factorial_two]; field

Premises used: le_of_eq
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 / π)
convert_2 : 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)

Tactic:
convert_to _ ≤ (a m) * (1 + 1 / m : ℝ) ^ (2 * m) / (4 / π)

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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₁ :
  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 / π)
⊢ a (m + 1) = a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)

Tactic:
simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]

Premises used: add_mul, Nat.factorial_succ, pow_succ, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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₁ :
  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)
⊢ 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:
field_simp
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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₁ :
  HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (m * 2) * HPow.hPow (α := ℝ) (↑m : ℝ) (2 * m) =
    HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (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)

Tactic:
simp [field, div_pow]

Premises used: div_pow
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (m * 2) * HPow.hPow (α := ℝ) (↑m : ℝ) (2 * m) =
    HPow.hPow (α := ℝ) (↑m : ℝ) (m * 2) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 ^ (2 * m)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
⊢ 0 < 4 / π

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
convert_2 : 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m) / (4 / π)

Tactic:
rw [_root_.le_div_iff₀ (by positivity), pow_succ]

Premises used: pow_succ, le_div_iff₀
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
⊢ LE.le (α := ℝ) 0 3

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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)
⊢ 0 ≤ a m

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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₁ : 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) = 4 / 9 * (3 * π / 4) ^ m * 3
⊢ 4 / 9 * ((3 * π / 4) ^ m * (3 * π / 4)) * (4 / π) ≤ a m * (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)

Tactic:
convert! (mul_le_mul h_m this (by positivity) (by positivity)) using 1

Premises used: mul_le_mul
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 / π) = 4 / 9 * (3 * π / 4) ^ m * 3

Tactic:
field
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
succ : 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)

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
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
simp : 3 = HAdd.hAdd (α := ℝ) 1 2
⊢ 3 = 1 + (↑(2 * m) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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 = HAdd.hAdd (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
succ : -2 ≤ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)
⊢ 3 ≤ (1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)) ^ (2 * m)

Tactic:
refine le_trans (le_of_eq (by simp [field]; norm_num)) (one_add_mul_le_pow ?_ (2 * m))

Premises used: HMul.hMul, le_of_eq, OfNat.ofNat, one_add_mul_le_pow, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ LE.le (α := ℝ) (-2) 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
⊢ -2 ≤ HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)

Tactic:
exact le_trans (by norm_num : (-2 : ℝ) ≤ 0) (by positivity)

Premises used: le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
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
base : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ a 2
succ : ∀ (m : ℕ), 2 ≤ m → ∀ (h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m), 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)
⊢ 4 / 9 * (3 * π / 4) ^ n ≤ a n

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)

Premises used: le_of_eq, le_trans
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
⊢ Nat.succ 1 ≤ finrank ℚ K

Tactic:
rw [← Nat.succ_le_iff] at h

Premises used: Nat.succ_le_iff
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
rify : LT.lt (α := ℝ) 2 |(↑(discr K) : ℝ)|
⊢ 2 < |discr K|

Tactic:
rify
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
nlinarith : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 9 / 9 = 1
nlinarith₁ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 9 = 9
nlinarith₂ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₃ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 4 / 4 = 1
nlinarith₄ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 4 = 4
nlinarith₅ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 4 2 = 16
nlinarith₆ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 9 16 = 144
nlinarith₇ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 144 0
nlinarith₈ :
  4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 →
    HMul.hMul (α := ℝ) 36 (-1) +
            (HMul.hMul (α := ℝ) 1 4 * (1 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 1 3 * (1 * π)) 2) -
              HMul.hMul (α := ℝ) 144 2) +
          216 * (3 - π) +
        36 * (0 - (3 - π) * (3 - π)) =
      0
nlinarith₉ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 36 0
nlinarith₁₀ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 216 0
nlinarith₁₁ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 36 0
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2

Tactic:
nlinarith [Real.pi_gt_three]

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
hbc : 1 ≤ 3 * π / 4
⊢ 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
linarith : 3 * π / 4 < 1 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : 3 * π / 4 < 1 → 4 / 4 = 1
linarith₂ : 3 * π / 4 < 1 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₃ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 4 0
linarith₄ :
  3 * π / 4 < 1 →
    HMul.hMul (α := ℝ) 5 (-1) + (HMul.hMul (α := ℝ) 1 3 * (1 * π) - HMul.hMul (α := ℝ) 4 1) + 3 * (3 - π) = 0
linarith₅ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 5 0
linarith₆ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 3 0
⊢ 1 ≤ 3 * π / 4

Tactic:
linarith [Real.pi_gt_three]

Premises used: Real.pi_gt_three
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ |(↑(discr K) : ℝ)|

Tactic:
mod_cast abs_discr_ge h

Premises used: Real.pi, HMul.hMul, NumberField.abs_discr_ge, congrArg, Rat, cast, HDiv.hDiv, LE.le, Nat.cast, HPow.hPow, Int.cast_abs._simp_1, OfNat.ofNat, Eq.symm, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
π : 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
π₁ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K
⊢ LT.lt (α := ℝ) 2 |(↑(discr K) : ℝ)|

Tactic:
calc
    (2 : ℝ) < (4 / 9) * (3 * π / 4) ^ 2 := by
      nlinarith [Real.pi_gt_three]
    _ ≤ (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K := by
      gcongr
      linarith [Real.pi_gt_three]
    _ ≤ |(discr K : ℝ)| := mod_cast abs_discr_ge h

Premises used: Int.cast, Real.pi, HMul.hMul, NumberField.abs_discr_ge, Rat, HDiv.hDiv, NumberField.discr, OfNat.ofNat, Module.finrank