-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 * ε)
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) + log ε
rwa₁₀ :
  log (HPow.hPow (α := ℝ) (β := ℝ) (↑(Fintype.card Fq) : ℝ) (↑(A i₁ % b - A i₀ % b).natDegree : ℝ)) <
    log (HPow.hPow (α := ℝ) (↑(Fintype.card Fq) : ℝ) b.natDegree) + log ε
rwa₁₁ :
  log (HPow.hPow (α := ℝ) (β := ℝ) (↑(Fintype.card Fq) : ℝ) (↑(A i₁ % b - A i₀ % b).natDegree : ℝ)) <
    log (HPow.hPow (α := ℝ) (β := ℝ) (↑(Fintype.card Fq) : ℝ) (↑b.natDegree : ℝ)) + log ε
rwa₁₂ :
  (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) * log (↑(Fintype.card Fq) : ℝ) <
    log (HPow.hPow (α := ℝ) (β := ℝ) (↑(Fintype.card Fq) : ℝ) (↑b.natDegree : ℝ)) + log ε
rwa₁₃ :
  (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) * log (↑(Fintype.card Fq) : ℝ) <
    (↑b.natDegree : ℝ) * log (↑(Fintype.card Fq) : ℝ) + log ε
rwa₁₄ :
  (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) <
    ((↑b.natDegree : ℝ) * log (↑(Fintype.card Fq) : ℝ) + log ε) / log (↑(Fintype.card Fq) : ℝ)
rwa₁₅ :
  (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) <
    (↑b.natDegree : ℝ) * log (↑(Fintype.card Fq) : ℝ) / log (↑(Fintype.card Fq) : ℝ) +
      log ε / log (↑(Fintype.card Fq) : ℝ)
rwa₁₆ rwa₁₇ rwa₁₈ rwa₁₉ :
  (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

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']

Premises used: Iff.mpr, Int.cast_natCast, lt_div_iff₀, Real.log_rpow, Int.cast_pow, pow_ne_zero, Real.log_pos, eq_intCast, AbsoluteValue.pos, LT.lt.ne', mul_div_cancel_right₀, Polynomial.cardPowDegree_nonzero, Real.log_lt_log_iff, Algebra.smul_def, Polynomial.cardPowDegree, Int.cast_pos, Real.log_mul, Real.rpow_natCast, add_div