awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ[X])
    (∑ b ∈ range (n + 1),
      (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
        (n.choose b • HPow.hPow (α := ℤ[X]) (-1) b * HPow.hPow (α := ℤ[X]) X (n + b)))
    (∑ x ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X x)
have a : ∀ x ∈ range (n + 1),
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (n.choose x • HPow.hPow (α := ℤ[X]) (-1) x * HPow.hPow (α := ℤ[X]) X (n + x)) =
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X x
Tactic: congr! 1 with x _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (n.choose x • HPow.hPow (α := ℤ[X]) (-1) x * HPow.hPow (α := ℤ[X]) X (n + x)) =
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X x
have a : HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (n.choose x • HPow.hPow (α := ℤ) (-1) x) : ℤ[X])
    (HSMul.hSMul (α := ℤ) (↑((n + x)! / x !) : ℤ) (HPow.hPow (α := ℤ[X]) X x)) =
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
      ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
    HPow.hPow (α := ℤ[X]) X x
Tactic: rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (n.choose x • HPow.hPow (α := ℤ) (-1) x) : ℤ[X])
      (HSMul.hSMul (α := ℤ) (↑((n + x)! / x !) : ℤ) (HPow.hPow (α := ℤ[X]) X x)) =
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X x
have a : (↑(n.choose x) : ℤ[X]) * HPow.hPow (α := ℤ[X]) (-1) x * ((↑((n + x)! / x !) : ℤ[X]) * HPow.hPow (α := ℤ[X]) X x) =
  (↑((n + x)! / x !) : ℤ[X]) * ((↑(n.choose x) : ℤ[X]) * HPow.hPow (α := ℤ[X]) (-1) x) * HPow.hPow (α := ℤ[X]) X x
Tactic: simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ[X])
    (∑ x ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X x)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) i * (↑(n.choose i) : ℤ) * (↑((n + i).choose n) : ℤ)) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X i)
have a : ∀ x ∈ range (n + 1),
  HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
      ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
      ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ) * (↑((n + x).choose n) : ℤ)) : ℤ[X])
Tactic: congr! 2 with x _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
      ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
      ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ) * (↑((n + x).choose n) : ℤ)) : ℤ[X])
have a : HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ)) : ℤ[X])
    ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X]) =
  HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ)) : ℤ[X])
    (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X]))
Tactic: rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ)) : ℤ[X])
      ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ)) : ℤ[X])
      (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X]))
have a : (↑((n + x)! / x !) : ℤ[X]) = HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X])
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ (↑((n + x)! / x !) : ℤ[X]) = HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X])
have a : (↑((x + n)! / x !) : ℤ[X]) = HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((x + n)! / (x ! * n !)) : ℤ)) (↑n ! : ℤ[X])
Tactic: rw [add_comm, add_choose]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ (↑((x + n)! / x !) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) (↑((↑(x + n)! : ℤ) / HMul.hMul (α := ℤ) (↑x ! : ℤ) (↑n ! : ℤ)) : ℤ[X]) (↑n ! : ℤ[X])
have a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / (x ! * n !) * n !) : ℤ[X])
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / (x ! * n !) * n !) : ℤ[X])
have a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])
Tactic: rw [mul_comm, ← Nat.mul_div_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / (x ! * n !) * n !) : ℤ[X])
have a₁ : x ! * n ! ∣ (x + n)!
Tactic: rw [mul_comm, ← Nat.mul_div_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])
have a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! * n ! / (x ! * n !)) : ℤ[X])
Tactic: rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! * n ! / (x ! * n !)) : ℤ[X])
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])
have a₁ : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / x !) : ℤ[X])
Tactic: rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
have _ : (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
Tactic: calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
_ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
have _₁ : (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n) =
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
    (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))
Tactic: calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
_ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
_₁ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
have _₂ : Eq (α := ℤ[X])
  ((⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
    (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)))
  (∑ x ∈ range (n + 1),
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X x)
Tactic: calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
_ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
_₁ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))
_₂ :
  Eq (α := ℤ[X])
    ((⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)))
    (∑ x ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X x)
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
have _₃ : Eq (α := ℤ[X])
  (∑ x ∈ range (n + 1),
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X x)
  (∑ i ∈ range (n + 1),
    HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
        ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) i * (↑(n.choose i) : ℤ) * (↑((n + i).choose n) : ℤ)) : ℤ[X]) *
      HPow.hPow (α := ℤ[X]) X i)
Tactic: calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n k : ℕ
⊢ (shiftedLegendre n).coeff k = HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
have rw : ∑ b ∈ range (n + 1),
    (HMul.hMul (α := ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) b * (↑(n.choose b) : ℤ) * (↑((n + b).choose n) : ℤ)) : ℤ[X])
          (HPow.hPow (α := ℤ[X]) X b)).coeff
      k =
  HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
Tactic: rw [shiftedLegendre, finsetSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n k : ℕ
⊢ ∑ b ∈ range (n + 1),
      (HMul.hMul (α := ℤ[X])
            ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) b * (↑(n.choose b) : ℤ) * (↑((n + b).choose n) : ℤ)) : ℤ[X])
            (HPow.hPow (α := ℤ[X]) X b)).coeff
        k =
    HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
have simp_rw : (∑ x ∈ range (n + 1),
    if k = x then HPow.hPow (α := ℤ) (-1) x * (↑(n.choose x) : ℤ) * (↑((n + x).choose n) : ℤ) else 0) =
  HPow.hPow (α := ℤ) (-1) k * (↑(n.choose k) : ℤ) * (↑((n + k).choose n) : ℤ)
Tactic: simp_rw [coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (shiftedLegendre n).degree = (↑n : WithBot ℕ)
have refine_1 : (shiftedLegendre n).degree ≤ (↑n : WithBot ℕ)
Tactic: refine le_antisymm ?_ (le_degree_of_ne_zero ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
refine_1 : (shiftedLegendre n).degree ≤ (↑n : WithBot ℕ)
⊢ (shiftedLegendre n).degree = (↑n : WithBot ℕ)
have refine_2 : (shiftedLegendre n).coeff n ≠ 0
Tactic: refine le_antisymm ?_ (le_degree_of_ne_zero ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (shiftedLegendre n).degree ≤ (↑n : WithBot ℕ)
have refine_1 : ∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑m : WithBot ℕ) → (shiftedLegendre n).coeff m = 0
Tactic: rw [degree_le_iff_coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (hypothesis)
Goal:
n k : ℕ
h : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑k : WithBot ℕ)
⊢ (shiftedLegendre n).coeff k = 0
have h₁ : n < k
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X) = shiftedLegendre n
have refine : (↑n ! : ℤ[X]) * (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
  (↑n ! : ℤ[X]) * shiftedLegendre n
Tactic: refine nat_mul_inj' ?_ (factorial_ne_zero n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (↑n ! : ℤ[X]) * (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
have rw : (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
    ((HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n).comp (HSub.hSub (α := ℤ[X]) 1 X)) =
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n)
Tactic: rw [← mul_assoc, mul_comm (n ! : ℤ[X]), mul_assoc, ← natCast_mul_comp,
    factorial_mul_shiftedLegendre_eq, ← iterate_derivative_comp_one_sub_X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (hypothesis)
Goal:
n : ℕ
R : Type u_1
inst : Ring R
x : R
⊢ (aeval x : (a : ℤ[X]) → R) (shiftedLegendre n) =
    HMul.hMul (β := R) (HPow.hPow (α := R) (-1) n) ((aeval (1 - x) : (a : ℤ[X]) → R) (shiftedLegendre n) : R)
have this : Eq (α := R)
  ((aeval x : (a : ℤ[X]) → R) (HPow.hPow (α := ℤ[X]) (-1) n * (shiftedLegendre n).comp (HSub.hSub (α := ℤ[X]) 1 X)) : R)
  ((aeval x : (a : ℤ[X]) → R) (shiftedLegendre n) : R)
Tactic: have := congr(aeval x $(neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq n))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : (s : (a : Unit) → ℕ) () = n
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (coeff n) (MvPowerSeries.coeff s)
have rw : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () n)) (MvPowerSeries.coeff s)
Tactic: rw [coeff, ← h, ← Finsupp.unique_single s]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : (s : (a : Unit) → ℕ) () = n
rw : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () n)) (MvPowerSeries.coeff s)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (coeff n) (MvPowerSeries.coeff s)
have rw₁ : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () ((s : (a : Unit) → ℕ) ()))) (MvPowerSeries.coeff s)
Tactic: rw [coeff, ← h, ← Finsupp.unique_single s]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Unit →₀ ℕ
n : ℕ
h : (s : (a : Unit) → ℕ) () = n
rw : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () n)) (MvPowerSeries.coeff s)
rw₁ :
  Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff (single () ((s : (a : Unit) → ℕ) ()))) (MvPowerSeries.coeff s)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (coeff n) (MvPowerSeries.coeff s)
have rw₂ : Eq.{u_1 + 1} (α := R⟦X⟧ →ₗ[R] R) (MvPowerSeries.coeff s) (MvPowerSeries.coeff s)
Tactic: rw [coeff, ← h, ← Finsupp.unique_single s]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
n : Unit →₀ ℕ
⊢ Eq (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) φ : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) ψ : R)
have rw : Eq (α := R) ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) φ : R)
  ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) ψ : R)
Tactic: rw [← coeff_def]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) ((coeff n : (a : R⟦X⟧) → R) ψ : R)
n : Unit →₀ ℕ
rw :
  Eq (α := R) ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) φ : R)
    ((coeff ((n : (a : Unit) → ℕ) ()) : (a : MvPowerSeries Unit R) → R) ψ : R)
⊢ Eq (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) φ : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries Unit R) → R) ψ : R)
have rw₁ : Eq (α := ℕ) ((n : (a : Unit) → ℕ) () : ℕ) ((n : (a : Unit) → ℕ) () : ℕ)
Tactic: rw [← coeff_def]