awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
⊢ Eq (α := A)
    ((PowerSeries.coeff 0 : (a : A⟦X⟧) → A)
        ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
          (exp A - 1)) :
      A)
    ((PowerSeries.coeff 0 : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)

Tactic:
simp
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
h :
  ∑ x ∈ range (n + 1),
        HMul.hMul (α := A) (β := A)
          ((PowerSeries.coeff (x, n + 1 - x).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          ((PowerSeries.coeff (x, n + 1 - x).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      HMul.hMul (α := A) (β := A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ Eq (α := A)
    ((PowerSeries.coeff (n + 1) : (a : A⟦X⟧) → A)
        ((PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) *
          (exp A - 1)) :
      A)
    ((PowerSeries.coeff (n + 1) : (a : A⟦X⟧) → A)
        (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) PowerSeries.X ((rescale t : (a : A⟦X⟧) → A⟦X⟧) (exp A) : A⟦X⟧)) :
      A)

Tactic:
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]

Premises used: PowerSeries.coeff_rescale, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, PowerSeries.coeff_exp, PowerSeries.coeff_mul, PowerSeries.coeff_succ_X_mul, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
h :
  ∑ x ∈ range (n + 1),
      HMul.hMul (α := A)
        ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ ∑ x ∈ range (n + 1),
        HMul.hMul (α := A) (β := A)
          ((PowerSeries.coeff (x, n + 1 - x).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          ((PowerSeries.coeff (x, n + 1 - x).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      HMul.hMul (α := A) (β := A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        ((PowerSeries.coeff (n + 1, n + 1 - (n + 1)).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
simp only [map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
    coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]

Premises used: map_sub, sub_self, tsub_self, PowerSeries.constantCoeff_one, MulZeroClass.mul_zero, PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.constantCoeff_exp, add_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
⊢ IsUnit (M := ℚ) (↑(n + 1)! : ℚ)

Tactic:
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))
⊢ ∑ x ∈ range (n + 1),
      HMul.hMul (α := A)
        ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]

Premises used: Algebra.algebraMap, Rat, IsUnit.mul_right_inj, IsUnit.map
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A))

Tactic:
rw [mul_left_comm, ← map_mul]

Premises used: mul_left_comm, map_mul
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n)
      ((algebraMap ℚ A : (a : ℚ) → A) ((↑((n + 1) * n !) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n) ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))

Premises used: HMul.hMul, Algebra.algebraMap, Rat, HDiv.hDiv, Nat.cast, HAdd.hAdd, Nat.factorial, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    (aeval t : (a : ℚ[X]) → A) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    HMul.hMul (β := A) (t ^ n)
      ((algebraMap ℚ A : (a : ℚ) → A) ((↑((n + 1) * n !) : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ)) : A)

Tactic:
rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]

Premises used: Iff.mpr, mul_assoc, mul_one_div_cancel, Nat.cast_add, Nat.factorial_ne_zero, Nat.cast_mul, HPow.hPow, mul_comm, Polynomial.aeval_monomial, mul_one, Nat.cast_one, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  Eq.{u_1 + 1} (α := A)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
        (HMul.hMul (α := A)
          ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))))
    (∑ x ∈ range (n + 1), (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)))
⊢ HMul.hMul (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (∑ x ∈ range (n + 1),
          HMul.hMul (α := A)
            ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
                (PowerSeries.mk fun (n : ℕ) ↦
                  (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
              A)
            (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
              ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A)) :
        A) =
    (aeval t : (a : ℚ[X]) → A) ((monomial n : (a : ℚ) → ℚ[X]) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) : ℚ[X])

Tactic:
rw [← sum_bernoulli, Finset.mul_sum, map_sum]

Premises used: Finset.mul_sum, Polynomial.sum_bernoulli, map_sum
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
h :
  ∀ x ∈ range (n + 1),
    HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
        (HMul.hMul (α := A)
          ((PowerSeries.coeff x : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - x) : (a : A⟦X⟧) → A) 1 : A))) =
      (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x))
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
        (HMul.hMul (α := A)
          ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦
                (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
            A)
          (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
            ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))))
    (∑ x ∈ range (n + 1), (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose x) : ℚ) (bernoulli x)))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
i : ℕ
hi : i ∈ range (n + 1)
h :
  HMul.hMul (α := A) (β := A)
      ((algebraMap ℚ A : (a : ℚ) → A)
          ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑i ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n + 1 - i)! : ℚ)) :
        A)
      ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) / HMul.hMul (α := ℚ) (↑i ! : ℚ) (↑(n + 1 - i)! : ℚ)) : A)
      ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A)
⊢ HMul.hMul (α := A) ((algebraMap ℚ A : (a : ℚ) → A) (↑(n + 1)! : ℚ) : A)
      (HMul.hMul (α := A)
        ((PowerSeries.coeff i : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (aeval t : (a : ℚ[X]) → A) (HDiv.hDiv (α := ℚ) 1 (↑n ! : ℚ) • bernoulli n)) :
          A)
        (HSub.hSub (α := A) (β := A) ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) (exp A) : A)
          ((PowerSeries.coeff (n + 1 - i) : (a : A⟦X⟧) → A) 1 : A))) =
    (aeval t : (a : ℚ[X]) → A) (HSMul.hSMul (α := ℚ) (↑((n + 1).choose i) : ℚ) (bernoulli i))

Tactic:
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
    PowerSeries.coeff_one, coeff_exp, sub_zero, Algebra.smul_def,
    mul_right_comm _ ((aeval t) _), ← mul_assoc, ← map_mul, ← Polynomial.C_eq_algebraMap,
    Polynomial.aeval_mul, Polynomial.aeval_C]

Premises used: sub_zero, Rat, mul_assoc, PowerSeries.coeff_mk, Polynomial.C_eq_algebraMap, PowerSeries.coeff_exp, Finset.mem_range_sub_ne_zero, Polynomial.aeval_mul, map_mul, Finset.mem_range_le, PowerSeries.coeff_one, mul_right_comm, Polynomial.aeval_C, Algebra.smul_def, Polynomial.aeval, Nat.cast_choose, if_neg, DFunLike.coe
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit (M := ℚ) (↑(n + 1)! : ℚ)
i : ℕ
hi : i ∈ range (n + 1)
⊢ HMul.hMul (α := A) (β := A)
      ((algebraMap ℚ A : (a : ℚ) → A)
          ((↑(n + 1)! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑i ! : ℚ) * HDiv.hDiv (α := ℚ) 1 (↑(n + 1 - i)! : ℚ)) :
        A)
      ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A) =
    HMul.hMul (α := A) (β := A)
      ((algebraMap ℚ A : (a : ℚ) → A) ((↑(n + 1)! : ℚ) / HMul.hMul (α := ℚ) (↑i ! : ℚ) (↑(n + 1 - i)! : ℚ)) : A)
      ((aeval t : (a : ℚ[X]) → A) (bernoulli i) : A)

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
⊢ ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)

Tactic:
have hf' : ∀ x, 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3) := fun x h =>
    div_pos (mul_pos h (rpow_pos_of_pos (mul_pos two_pos h) _)) (rpow_pos_of_pos four_pos _)
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
⊢ 0 < 2 * x

Tactic:
have h6 := mul_pos (zero_lt_two' ℝ) h5
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
⊢ 0 < (2 * x) ^ √(2 * x)

Tactic:
have h7 := rpow_pos_of_pos h6 (√(2 * x))
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x_1 : ℝ
x_large : 512 ≤ x_1
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
rw : f x = log (x * (2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₁ : f x = log x + log ((2 * x) ^ √(2 * x)) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₂ : f x = log x + √(2 * x) * log (2 * x) - log (HPow.hPow (α := ℝ) 4 (x / 3))
rw₃ : f x = log x + √(2 * x) * log (2 * x) - x / 3 * log 4
rw₄ : f x = log x + √(2 * x) * log (2 * x) - x * log 4 / 3
rw₅ : f x = log x + √(2 * x) * log (2 * x) - x * (log 4 / 3)
rw₆ rw₇ : f x = log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
⊢ f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))

Tactic:
rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
      log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x]

Premises used: mul_div, Real.rpow_pos_of_pos, four_pos, Real.log_rpow, Real.log_div, mul_div_right_comm, LT.lt.ne', mul_pos, mul_comm, zero_lt_four, Real.log_mul
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
⊢ ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))

Tactic:
have hf : ∀ x, 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)) := by
    intro x h5
    have h6 := mul_pos (zero_lt_two' ℝ) h5
    have h7 := rpow_pos_of_pos h6 (√(2 * x))
    rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
      log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x]
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
⊢ LT.lt (α := ℝ) 0 512

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
⊢ 0 < x

Tactic:
have h5 : 0 < x := lt_of_lt_of_le (by norm_num1) x_large
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ 1 - 2 / 3 = 1 / 3

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
rw : f x ≤ 0
⊢ x * (2 * x) ^ √(2 * x) * HPow.hPow (α := ℝ) 4 (2 * x / 3) ≤ HPow.hPow (α := ℝ) 4 x

Tactic:
rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos, ←
    mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
    mul_one_div, ← log_nonpos_iff (hf' x h5).le, ← hf x h5]

Premises used: mul_div, Real.rpow_pos_of_pos, four_pos, div_div_eq_mul_div, LT.lt.le, mul_one_sub, div_le_one, mul_one_div, Real.rpow_sub, Real.log_nonpos_iff, OfNat.ofNat, mul_div_left_comm
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hf₁ : ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)
hg : ConvexOn ℝ (E := ℝ) (Set.Ioi 0.5) (HMul.hMul (log 4 / 3))
⊢ ConcaveOn ℝ (Set.Ioi 0.5) f

Tactic:
apply ConcaveOn.sub

Premises used: ConcaveOn.sub
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
hf₁ : ConcaveOn ℝ (Set.Ioi 0.5) log
hf₂ : ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ √(2 * x) * log (2 * x)
⊢ ConcaveOn ℝ (β := ℝ) (Set.Ioi 0.5) fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x)

Tactic:
apply ConcaveOn.add

Premises used: ConcaveOn.add
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ LE.le (α := ℝ) 0 0.5

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) log

Tactic:
exact strictConcaveOn_log_Ioi.concaveOn.subset
          (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)

Premises used: OfScientific.ofScientific, ConcaveOn.subset, Bool.true, Set.Ioi_subset_Ioi, strictConcaveOn_log_Ioi, StrictConcaveOn.concaveOn, convex_Ioi
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (E := ℝ) (β := ℝ)
    (Set.preimage (β := ℝ) (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ) (Set.Ioi 1))
    ((fun (x : ℝ) ↦ √x * log x) ∘ (⇑(HSMul.hSMul (α := ℝ) (β := ℝ →ₗ[ℝ] ℝ) 2 LinearMap.id) : (a : ℝ) → ℝ))

Tactic:
((strictConcaveOn_sqrt_mul_log_Ioi.concaveOn.comp_linearMap ((2 : ℝ) • LinearMap.id)))

Premises used: LinearMap.id, ConcaveOn.comp_linearMap, strictConcaveOn_sqrt_mul_log_Ioi, HSMul.hSMul, StrictConcaveOn.concaveOn, OfNat.ofNat