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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
linarith : π ≤ 4 / 3 → 3 / 3 = 1
linarith₁ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 1 3 = 3
⊢ 4 / 3 < π
have linarith₂ : π ≤ 4 / 3 → 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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
linarith : π ≤ 4 / 3 → 3 / 3 = 1
linarith₁ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ 4 / 3 → GT.gt (α := ℝ) 3 0
⊢ 4 / 3 < π
have linarith₃ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 5 (-1) + (3 * π - HMul.hMul (α := ℝ) 1 4) + 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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
linarith : π ≤ 4 / 3 → 3 / 3 = 1
linarith₁ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 1 3 = 3
linarith₂ : π ≤ 4 / 3 → GT.gt (α := ℝ) 3 0
linarith₃ : π ≤ 4 / 3 → HMul.hMul (α := ℝ) 5 (-1) + (3 * π - HMul.hMul (α := ℝ) 1 4) + 3 * (3 - π) = 0
⊢ 4 / 3 < π
have linarith₄ : π ≤ 4 / 3 → GT.gt (α := ℝ) 5 0
Tactic: linarith [Real.pi_gt_three]
-- 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 : ℤ)
h_nz : N ≠ 0
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
have h₂ : 1 < 3 * π / 4
Tactic: have h₂ : 1 < 3 * π / 4 := by
    rw [_root_.lt_div_iff₀ (by positivity), ← _root_.div_lt_iff₀' (by positivity), one_mul]
    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
h₂ : 1 < 3 * π / 4
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
have inl : ∀ (h : 1 < finrank ℚ K), finrank ℚ K ≤ rankOfDiscrBdd N
Tactic: obtain h | h := lt_or_ge 1 (finrank ℚ 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_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
inl : ∀ (h : 1 < finrank ℚ K), finrank ℚ K ≤ rankOfDiscrBdd N
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
have inr : ∀ (h : finrank ℚ K ≤ 1), finrank ℚ K ≤ rankOfDiscrBdd N
Tactic: obtain h | h := lt_or_ge 1 (finrank ℚ 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_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ rankOfDiscrBdd N
have inl : finrank ℚ K ≤ ⌊Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)⌋₊
Tactic: apply le_max_of_le_right
-- 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
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)⌋₊
have inl : (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
Tactic: rw [Nat.le_floor_iff]
-- 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
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
inl : (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
⊢ finrank ℚ K ≤ ⌊Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)⌋₊
have inl₁ : 0 ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
Tactic: rw [Nat.le_floor_iff]
-- 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 : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
have h₁ : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑(↑N : ℤ) : ℝ)
Tactic: have h := le_trans (abs_discr_ge h) (Int.cast_le.mpr 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : 4 / 9 * (3 * π / 4) ^ finrank ℚ K ≤ (↑(↑N : ℤ) : ℝ)
⊢ (↑(finrank ℚ K) : ℝ) ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
have inl : ∀ (h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)),
  (↑(↑N : ℤ) : ℝ) < 4 / 9 * (3 * π / 4) ^ finrank ℚ K
Tactic: contrapose! 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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) < 4 / 9 * (3 * π / 4) ^ finrank ℚ K
have inl : (↑(↑N : ℤ) : ℝ) < 4 / 9 * HPow.hPow (β := ℝ) (3 * π / 4) (↑(finrank ℚ K) : ℝ)
Tactic: rw [← Real.rpow_natCast]
-- 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 : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4) < (↑(finrank ℚ K) : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) < 4 / 9 * HPow.hPow (β := ℝ) (3 * π / 4) (↑(finrank ℚ K) : ℝ)
have h₁ : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
Tactic: rw [Real.log_div_log] 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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
h_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) < 4 / 9 * HPow.hPow (β := ℝ) (3 * π / 4) (↑(finrank ℚ K) : ℝ)
have inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
Tactic: refine lt_of_le_of_lt ?_ (mul_lt_mul_of_pos_left
        (Real.rpow_lt_rpow_of_exponent_lt h₂ h) (by positivity : (0 : ℝ) < 4 / 9))
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl₂ : (↑(↑N : ℤ) : ℝ) ≤ (9 / 4)⁻¹ * (9 / 4) * (↑N : ℝ)
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
inl₂ : (↑(↑N : ℤ) : ℝ) ≤ (9 / 4)⁻¹ * (9 / 4) * (↑N : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl₃ : (↑(↑N : ℤ) : ℝ) ≤ HMul.hMul (α := ℝ) 1 (↑N : ℝ)
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
inl₂ : (↑(↑N : ℤ) : ℝ) ≤ (9 / 4)⁻¹ * (9 / 4) * (↑N : ℝ)
inl₃ : (↑(↑N : ℤ) : ℝ) ≤ HMul.hMul (α := ℝ) 1 (↑N : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl₄ : LE.le (α := ℝ) (↑(↑N : ℤ) : ℝ) (↑N : ℝ)
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h_1 : 1 < finrank ℚ K
h : Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ)) < (↑(finrank ℚ K) : ℝ)
inl : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4 * (↑N : ℝ))
inl₁ : (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (9 / 4) * (↑N : ℝ)
inl₂ : (↑(↑N : ℤ) : ℝ) ≤ (9 / 4)⁻¹ * (9 / 4) * (↑N : ℝ)
inl₃ : (↑(↑N : ℤ) : ℝ) ≤ HMul.hMul (α := ℝ) 1 (↑N : ℝ)
inl₄ : LE.le (α := ℝ) (↑(↑N : ℤ) : ℝ) (↑N : ℝ)
⊢ (↑(↑N : ℤ) : ℝ) ≤ 4 / 9 * (3 * π / 4) ^ Real.logb (3 * π / 4) (9 / 4 * (↑N : ℝ))
have inl₅ : LE.le (α := ℝ) (↑N : ℝ) (↑N : ℝ)
Tactic: rw [Real.rpow_logb (lt_trans zero_lt_one h₂) (ne_of_gt h₂) (by positivity), ← mul_assoc,
            ← inv_div, inv_mul_cancel₀ (by simp), one_mul, Int.cast_natCast]
-- 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
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 0 ≤ Real.log (9 / 4 * (↑N : ℝ)) / Real.log (3 * π / 4)
have inl : 1 ≤ 9 / 4 * (↑N : ℝ)
Tactic: refine div_nonneg (Real.log_nonneg ?_) (Real.log_nonneg (le_of_lt 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_nz : N ≠ 0
h₂ : 1 < 3 * π / 4
h : 1 < finrank ℚ K
⊢ 1 ≤ 9 / 4 * (↑N : ℝ)
have inl : 4 / 9 ≤ (↑N : ℝ)
Tactic: rw [mul_comm, ← mul_div_assoc, _root_.le_div_iff₀ (by positivity), one_mul,
        ← _root_.div_le_iff₀ (by positivity)]
-- 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 : ℤ)
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N
have 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
Tactic: simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]
-- 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 : ℤ)
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
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N
have 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
Tactic: simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]
-- 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 : ℤ)
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
⊢ boundOfDiscBdd N - 1 < boundOfDiscBdd N
have simp_rw₂ : LT.lt (α := ℝ≥0) 0 1
Tactic: simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]
-- 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 : ℤ)
⊢ minkowskiBound K 1 < (↑(boundOfDiscBdd N) : ℝ≥0∞)
have this : 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]
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 < (↑(boundOfDiscBdd N) : ℝ≥0∞)
have refine : minkowskiBound K 1 ≤ (↑(boundOfDiscBdd N - 1) : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt ?_ (coe_lt_coe.mpr this)
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) = 1 * (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞)
have rw : (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞) = (↑((sqrt : (a : ℝ≥0) → ℝ≥0) (↑N : ℝ≥0)) : ℝ≥0∞)
Tactic: rw [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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ minkowskiBound K 1 ≤ (↑(boundOfDiscBdd N - 1) : ℝ≥0∞)
have 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)
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]]
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd 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)
have h₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) ≤ 1
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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) ≤ 1
⊢ 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)
have h₂ : ‖discr K‖₊ ≤ (↑N : ℝ≥0)
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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (nrComplexPlaces K) ≤ 1
h₂ : ‖discr K‖₊ ≤ (↑N : ℝ≥0)
⊢ 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)
have h₃ : LE.le (α := ℝ≥0∞) 1 2
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
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
⊢ 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)
have h₄ : finrank ℚ K ≤ rankOfDiscrBdd N
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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₁ : (↑‖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]
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : (↑‖discr K‖₊ : ℝ) ≤ (↑(↑N : ℝ≥0) : ℝ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₂ : ‖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]
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : (↑‖discr K‖₊ : ℝ) ≤ (↑(↑N : ℝ≥0) : ℝ)
h₂ : ‖discr K‖ ≤ (↑(↑N : ℝ≥0) : ℝ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₃ : |(↑(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]
-- 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 : ℤ)
this : boundOfDiscBdd N - 1 < boundOfDiscBdd N
h₁ : (↑‖discr K‖₊ : ℝ) ≤ (↑(↑N : ℝ≥0) : ℝ)
h₂ : ‖discr K‖ ≤ (↑(↑N : ℝ≥0) : ℝ)
h₃ : |(↑(discr K) : ℝ)| ≤ (↑(↑N : ℝ≥0) : ℝ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₄ : (↑|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]
-- 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 : ℤ)
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) : ℝ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₅ : LE.le (α := ℝ) (↑|discr K| : ℝ) (↑N : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs,
      NNReal.coe_natCast, ← Int.cast_natCast, Int.cast_le]
-- 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 : ℤ)
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 : ℝ)
⊢ ‖discr K‖₊ ≤ (↑N : ℝ≥0)
have h₆ : LE.le (α := ℝ) (↑|discr K| : ℝ) (↑(↑N : ℤ) : ℝ)
Tactic: rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs,
      NNReal.coe_natCast, ← Int.cast_natCast, 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
N : ℕ
hK : |discr K| ≤ (↑N : ℤ)
a : 𝓞 K
h : Eq (α := IntermediateField ℚ K) ℚ⟮(↑a : K)⟯ ⊤
⊢ natDegree (minpoly ℤ (↑a : K)) ≤ rankOfDiscrBdd N
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Basic (goal)
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 : ℤ)}
have 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⟯
Tactic: refine finite_of_finite_generating_set A _ (bUnion_roots_finite (algebraMap ℤ A) D
      (Set.finite_Icc (-C : ℤ) C)) (fun ⟨K, hK₀⟩ ⟨hK₁, hK₂⟩ ↦ ?_)