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
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
⊢ 4 / 9 * (3 * π / 4) ^ n ≤ a n
have succ : ∀ (m : ℕ), 2 ≤ m → ∀ (h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m), 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a (m + 1)
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : 1 < finrank ℚ K
⊢ 2 < |discr K|
have h₁ : Nat.succ 1 ≤ finrank ℚ K
Tactic: rw [← Nat.succ_le_iff] at h
Cleared hypotheses: 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 : Nat.succ 1 ≤ finrank ℚ K
⊢ 2 < |discr K|
have rify : LT.lt (α := ℝ) 2 |(↑(discr K) : ℝ)|
Tactic: rify
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
have nlinarith : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 9 / 9 = 1
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₁ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 9 = 9
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₂ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₃ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 4 / 4 = 1
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₄ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₅ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 4 2 = 16
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₆ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → HMul.hMul (α := ℝ) 9 16 = 144
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₇ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 144 0
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have 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
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₉ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 36 0
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
have nlinarith₁₀ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 2 → GT.gt (α := ℝ) 216 0
Tactic: nlinarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ K
have hbc : 1 ≤ 3 * π / 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 : Nat.succ 1 ≤ finrank ℚ K
⊢ 1 ≤ 3 * π / 4
have linarith : 3 * π / 4 < 1 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₁ : 3 * π / 4 < 1 → 4 / 4 = 1
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₂ : 3 * π / 4 < 1 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₃ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 4 0
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₄ : 3 * π / 4 < 1 →
  HMul.hMul (α := ℝ) 5 (-1) + (HMul.hMul (α := ℝ) 1 3 * (1 * π) - HMul.hMul (α := ℝ) 4 1) + 3 * (3 - π) = 0
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₅ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 5 0
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ 1 ≤ 3 * π / 4
have linarith₆ : 3 * π / 4 < 1 → GT.gt (α := ℝ) 3 0
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Nat.succ 1 ≤ finrank ℚ K
⊢ LT.lt (α := ℝ) 2 |(↑(discr K) : ℝ)|
have π : 2 < 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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
⊢ LT.lt (α := ℝ) 2 |(↑(discr K) : ℝ)|
have π₁ : 4 / 9 * HPow.hPow (β := ℕ) (3 * π / 4) 2 ≤ 4 / 9 * (3 * π / 4) ^ finrank ℚ 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : T.Finite
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
⊢ S.Finite
have hT₁ : Finite.{u_2 + 1} (↑T : Type u_2)
Tactic: rw [← Set.finite_coe_iff] at hT
Cleared hypotheses: hT, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
⊢ S.Finite
have refine : ∀ (x x_1 : (↑S : Type u_2))
  (h_eq :
    Eq.{u_2 + 1} (α := { x : A // x ∈ T })
      ((fun (x : (↑S : Type u_2)) ↦
          (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
            | ⟨F, hF⟩ =>
              Subtype.mk (p := fun (x : A) ↦ x ∈ T)
                (sorry.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) sorry :
            { x : A // x ∈ T }))
        x)
      ((fun (x : (↑S : Type u_2)) ↦
          (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
            | ⟨F, hF⟩ =>
              Subtype.mk (p := fun (x : A) ↦ x ∈ T)
                (sorry.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) sorry :
            { x : A // x ∈ T }))
        x_1)),
  x = x_1
Tactic: refine Set.finite_coe_iff.mp <| Finite.of_injective
    (fun ⟨F, hF⟩ ↦ (⟨(h F hF).choose, (h F hF).choose_spec.1⟩ : T)) (fun _ _ h_eq ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ x = x_1
have rw : (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
  (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
⊢ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A)
have h₁ : (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
  ℚ⟮sorry.choose (p := fun (x_2 : A) ↦
      x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)⟯
Tactic: convert! congr_arg (ℚ⟮·⟯) (Subtype.mk_eq_mk.mp h_eq)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
A : Type u_2
inst : Field A
inst_1 : CharZero A
p : IntermediateField ℚ A → Prop
S : Set { F : IntermediateField ℚ A // p F }
T : Set A
hT : Finite.{u_2 + 1} (↑T : Type u_2)
h : ∀ F ∈ S, ∃ x ∈ T, (↑F : IntermediateField ℚ A) = ℚ⟮x⟯
x x_1 : (↑S : Type u_2)
h_eq :
  Eq.{u_2 + 1} (α := { x : A // x ∈ T })
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x)
    ((fun (x : (↑S : Type u_2)) ↦
        (match (motive := (↑S : Type u_2) → { x : A // x ∈ T }) x with
          | ⟨F, hF⟩ =>
            Subtype.mk (p := fun (x : A) ↦ x ∈ T)
              (⋯.choose (p := fun (x : A) ↦ x ∈ T ∧ (↑F : IntermediateField ℚ A) = ℚ⟮x⟯)) ⋯ :
          { x : A // x ∈ T }))
      x_1)
h₁ :
  (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    ℚ⟮⋯.choose (p := fun (x_2 : A) ↦
        x_2 ∈ T ∧ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x_2⟯)⟯
⊢ (↑(↑x : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
    (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A)
have h₂ : (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) =
  ℚ⟮sorry.choose (p := fun (x : A) ↦
      x ∈ T ∧ (↑(↑x_1 : { F : IntermediateField ℚ A // p F }) : IntermediateField ℚ A) = ℚ⟮x⟯)⟯
Tactic: convert! congr_arg (ℚ⟮·⟯) (Subtype.mk_eq_mk.mp h_eq)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
⊢ N ≠ 0
have refine : ∀ (h : N = 0), discr K = 0
Tactic: refine fun h ↦ discr_ne_zero K ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h : N = 0
⊢ discr K = 0
have rwa : ∀ (hK : |discr K| ≤ (↑0 : ℤ)) (h : N = 0), discr K = 0
Tactic: rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
Cleared hypotheses: hK, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h : N = 0
rwa : ∀ (hK : |discr K| ≤ (↑0 : ℤ)) (h : N = 0), discr K = 0
⊢ discr K = 0
have rwa₁ : ∀ (hK : |discr K| ≤ 0) (h : N = 0), discr K = 0
Tactic: rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
Cleared hypotheses: hK, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h : N = 0
rwa : ∀ (hK : |discr K| ≤ (↑0 : ℤ)) (h : N = 0), discr K = 0
rwa₁ : ∀ (hK : |discr K| ≤ 0) (h : N = 0), discr K = 0
⊢ discr K = 0
have rwa₂ : ∀ (hK : discr K = 0) (h : N = 0), discr K = 0
Tactic: rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
Cleared hypotheses: hK, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
have h_nz : N ≠ 0
Tactic: have h_nz : N ≠ 0 := by
    refine fun h ↦ discr_ne_zero K ?_
    rwa [h, Nat.cast_zero, abs_nonpos_iff] at hK
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
⊢ 1 < 3 * π / 4
have rw : 4 / 3 < π
Tactic: rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
⊢ 4 / 3 < π
have linarith : π ≤ 4 / 3 → 3 / 3 = 1
Tactic: linarith [Real.pi_gt_three]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
linarith : π ≤ 4 / 3 → 3 / 3 = 1
⊢ 4 / 3 < π
have linarith₁ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 1 3 = 3
Tactic: linarith [Real.pi_gt_three]