awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₂ : log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
  log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₃ : log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
  log
    (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
      ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
rwa₃ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log
      (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
        ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₄ : log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
  log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
rwa₃ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log
      (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
        ε)
rwa₄ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₅ : log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
  log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
rwa₃ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log
      (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
        ε)
rwa₄ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₅ :
  log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₆ : log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
  log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
rwa₃ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log
      (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
        ε)
rwa₄ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₅ :
  log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₆ :
  log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₇ : log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
  log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) b.natDegree * ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
rwa :
  log (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₁ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
rwa₂ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree • ε)
rwa₃ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log
      (HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ)
        ε)
rwa₄ :
  log (↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (A i₁ % b - A i₀ % b).natDegree) : ℝ) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₅ :
  log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₆ :
  log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log ((↑(HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) b.natDegree) : ℝ) * ε)
rwa₇ :
  log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
    log (HPow.hPow (α := ℝ) (↑(↑(Fintype.card Fq) : ℤ) : ℝ) b.natDegree * ε)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rwa₈ : log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) (A i₁ % b - A i₀ % b).natDegree) <
  log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) b.natDegree * ε)
Tactic: rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have neg : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
Tactic: suffices (natDegree (A i₁ % b - A i₀ % b) : ℝ) < b.natDegree + log ε / log (Fintype.card Fq) by
    rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
have apply : ℕ
Tactic: apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
apply : ℕ
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
have apply₁ : (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
Tactic: apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
apply : ℕ
apply₁ :
  (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) <
    (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
have apply₂ : (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : ℝ) ≤
  (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
Tactic: apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) <
    (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
have h₁ : (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (A i₁ % b - A i₀ % b).degree
Tactic: convert! deg_lt