awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) =
    (↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m

Tactic:
(addLinearEquiv_apply' f).1

Premises used: Polynomial.degreeLT.addLinearEquiv_apply', And.left
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m

Tactic:
(addLinearEquiv_apply' f).2

Premises used: Polynomial.degreeLT.addLinearEquiv_apply', And.right
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n) ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f : ↥R[X]_m × ↥R[X]_n)
    ((Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_m) x)
          ((↑f : R[X]) %ₘ HPow.hPow (α := R[X]) X m) ⋯,
        Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x)
          ((↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m) ⋯) :
      ↥R[X]_m × ↥R[X]_n)

Tactic:
Prod.ext (Subtype.ext <| addLinearEquiv_apply_fst f) (Subtype.ext <| addLinearEquiv_apply_snd f)

Premises used: Polynomial.degreeLT.addLinearEquiv_apply_fst, Polynomial.degreeLT.addLinearEquiv_apply_snd, Prod.ext, Subtype.ext
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
f : R[X]
⊢ Membership.mem (α := R[X]) (γ := Submodule R R[X]) (R[X]_n) ((taylor r : (a : R[X]) → R[X]) f : R[X]) ↔
    Membership.mem (γ := Submodule R R[X]) (R[X]_n) f

Tactic:
simp [mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h :
  ∀ (x : R[X]),
    x ∈ Submodule.comap (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n ↔
      Membership.mem (γ := Submodule R R[X]) (R[X]_n) x
⊢ Submodule.comap (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n = R[X]_n

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
x : R[X]
⊢ x ∈ Submodule.comap (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n ↔
    Membership.mem (γ := Submodule R R[X]) (R[X]_n) x

Tactic:
simp [taylorEquiv]

Premises used: Polynomial.taylorEquiv
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
hf :
  Function.Surjective (α := R[X]) (β := R[X])
    (⇑(↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) : (a : R[X]) → R[X])
⊢ Submodule.map (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n = R[X]_n

Tactic:
nth_rw 1 [← comap_taylorEquiv_degreeLT (r := r), Submodule.map_comap_eq_of_surjective]

Premises used: Polynomial.comap_taylorEquiv_degreeLT, Submodule.map_comap_eq_of_surjective
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Function.Surjective (α := R[X]) (β := R[X])
    (⇑(↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) : (a : R[X]) → R[X])

Tactic:
(taylorEquiv r).surjective

Premises used: Polynomial.taylorEquiv, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Function.Surjective (α := R[X]) (β := R[X])
    (⇑(↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) : (a : R[X]) → R[X])

Tactic:
exact (taylorEquiv r).surjective

Premises used: Polynomial.taylorEquiv, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
r : R
⊢ Eq (α := ↥R[X]_n ≃ₗ[R] ↥R[X]_n) (LinearEquiv.symm (taylorLinearEquiv r n)) (taylorLinearEquiv (-r) n)

Tactic:
LinearEquiv.ext <| fun _ ↦ rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h_1 : Nontrivial R
h :
  ∀ (a : Fin n),
    Eq (α := R)
      ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n) :
            (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → Matrix (Fin n) (Fin n) R)
          (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) a a :
        R)
      (1 : R)
rw :
  Matrix.BlockTriangular.{u_1, 0, 0} (α := Fin n) (R := R)
    ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n) :
        (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → Matrix (Fin n) (Fin n) R)
      (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n))
    id
⊢ Eq (α := R) ((LinearMap.det : (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → R) (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) : R)
    (1 : R)

Tactic:
rw [← LinearMap.det_toMatrix (degreeLT.basis R n),
    Matrix.det_of_upperTriangular, Fintype.prod_eq_one]

Premises used: Fintype.prod_eq_one, Polynomial.degreeLT.basis, Matrix.det_of_upperTriangular, LinearMap.det_toMatrix
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h_1 : Nontrivial R
i : Fin n
h :
  Eq.{u_1 + 1} (α := R)
    (coeff
      (↑(((↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) : (a : ↥R[X]_n) → ↥R[X]_n)
            ((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) i)) :
        R[X])
      (HPow.hPow (α := R[X]) X (↑i : ℕ)).natDegree)
    1
⊢ Eq (α := R)
    ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n) :
          (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → Matrix (Fin n) (Fin n) R)
        (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) i i :
      R)
    (1 : R)

Tactic:
rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)]

Premises used: Fin.val, Polynomial.natDegree_X_pow, Polynomial.degreeLT.basis_repr, LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h_1 : Nontrivial R
i : Fin n
h :
  Eq (α := R)
    (coeff ((taylor r : (a : R[X]) → R[X]) (↑((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) i) : R[X]))
      (HPow.hPow (α := R[X]) X (↑i : ℕ)).natDegree)
    1
⊢ Eq.{u_1 + 1} (α := R)
    (coeff
      (↑(((↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) : (a : ↥R[X]_n) → ↥R[X]_n)
            ((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) i)) :
        R[X])
      (HPow.hPow (α := R[X]) X (↑i : ℕ)).natDegree)
    1

Tactic:
change (taylor r (degreeLT.basis R n i)).coeff _ = 1

Premises used: Polynomial.degreeLT.basis, Polynomial.taylor, Polynomial.coeff, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h_1 : Nontrivial R
i : Fin n
h :
  Eq.{u_1 + 1} (α := R)
    (coeff ((taylor r : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (↑i : ℕ)))
      (HPow.hPow (α := R[X]) X (↑i : ℕ)).natDegree)
    1
h₁ : (HPow.hPow (α := R[X]) X (↑i : ℕ)).leadingCoeff = 1
h₂ h₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq (α := R)
    (coeff ((taylor r : (a : R[X]) → R[X]) (↑((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) i) : R[X]))
      (HPow.hPow (α := R[X]) X (↑i : ℕ)).natDegree)
    1

Tactic:
rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]

Premises used: Polynomial.degreeLT.basis_val, Polynomial.coeff_taylor_natDegree, Polynomial.leadingCoeff_X_pow
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
rw :
  Eq.{u_1 + 1} (α := R)
    (coeff
      (↑((taylorLinearEquiv r n : (a : ↥R[X]_n) → ↥R[X]_n) ((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) j)) : R[X])
      (↑i : ℕ))
    0
⊢ Eq (α := R)
    ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n) :
          (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → Matrix (Fin n) (Fin n) R)
        (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) i j :
      R)
    (0 : R)

Tactic:
rw [LinearMap.toMatrix_apply, LinearEquiv.coe_coe, degreeLT.basis_repr]

Premises used: Polynomial.degreeLT.basis_repr, LinearMap.toMatrix_apply, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
change :
  Eq (α := R)
    (coeff ((taylor r : (a : R[X]) → R[X]) (↑((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) j) : R[X])) (↑i : ℕ)) 0
⊢ Eq.{u_1 + 1} (α := R)
    (coeff
      (↑((taylorLinearEquiv r n : (a : ↥R[X]_n) → ↥R[X]_n) ((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) j)) : R[X])
      (↑i : ℕ))
    0

Tactic:
change (taylor r (degreeLT.basis R n j)).coeff i = 0

Premises used: Polynomial.degreeLT.basis, Polynomial.taylor, Fin.val, Polynomial.coeff, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (↑j : ℕ))) < (↑(↑i : ℕ) : WithBot ℕ)

Tactic:
simpa [-taylor_X_pow, -taylor_pow]

Premises used: Polynomial.taylor_X_pow, Polynomial.taylor_pow
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
rw : Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (↑j : ℕ))) (↑i : ℕ)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R)
    (coeff ((taylor r : (a : R[X]) → R[X]) (↑((degreeLT.basis R n : (a : Fin n) → ↥R[X]_n) j) : R[X])) (↑i : ℕ)) 0

Tactic:
rw [degreeLT.basis_val, coeff_eq_zero_of_degree_lt (by simpa [-taylor_X_pow, -taylor_pow])]

Premises used: Polynomial.degreeLT.basis_val, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
rw :
  Eq (α := R) ((LinearMap.det : (a : ↥R[X]_n →ₗ[R] ↥R[X]_n) → R) (↑(taylorLinearEquiv r n) : ↥R[X]_n →ₗ[R] ↥R[X]_n) : R)
    ((↑1 : R) : R)
rw₁ : Eq.{u_1 + 1} (α := R) 1 (↑1 : R)
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : ↥R[X]_n ≃ₗ[R] ↥R[X]_n) → Rˣ) (taylorLinearEquiv r n)) : R) (↑1 : R)

Tactic:
rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]

Premises used: Polynomial.det_taylorLinearEquiv_toLinearMap, Units.val_one, LinearEquiv.coe_det
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
symm :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n
⊢ (↑n ! : ℤ[X]) * shiftedLegendre n =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n)

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
rw :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X * HSub.hSub (α := ℤ[X]) 1 X) ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
rw₁ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HMul.hMul (α := ℤ[X]) X X) ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
rw₂ rw₃ :
  (⇑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] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)

Tactic:
rw [← mul_pow, mul_one_sub, ← pow_two]

Premises used: pow_two, mul_one_sub, mul_pow
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
e_a :
  (X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n =
    ∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)
⊢ (⇑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:
congr
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
e_a :
  Eq (α := ℤ[X])
    (∑ m ∈ range (n + 1),
      (-HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ m * HPow.hPow (α := ℤ[X]) X (n - m) * (↑(n.choose m) : ℤ[X]))
    (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))
⊢ (X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n =
    ∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)

Tactic:
rw [sub_eq_add_neg, add_comm, add_pow]

Premises used: sub_eq_add_neg, add_comm, add_pow
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
e_a :
  ∀ (m : ℕ) (hm : m ∈ range (n + 1)),
    (-HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ m * HPow.hPow (α := ℤ[X]) X (n - m) * (↑(n.choose m) : ℤ[X]) =
      n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)
⊢ Eq (α := ℤ[X])
    (∑ m ∈ range (n + 1),
      (-HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ m * HPow.hPow (α := ℤ[X]) X (n - m) * (↑(n.choose m) : ℤ[X]))
    (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))

Tactic:
congr! 1 with m hm
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n m : ℕ
hm : m ∈ range (n + 1)
e_a : m ≤ n
⊢ (-HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ m * HPow.hPow (α := ℤ[X]) X (n - m) * (↑(n.choose m) : ℤ[X]) =
    n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)

Tactic:
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]

Premises used: pow_two, mul_assoc, pow_add, add_comm, neg_pow, mul_comm, nsmul_eq_mul, mul_pow, pow_mul_pow_sub
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m < n + 1

Tactic:
rw [Finset.mem_range] at hm

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n m : ℕ
hm : m < n + 1
linarith :
  n < m →
    -1 + (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - (↑m : ℤ)) =
      0
⊢ m ≤ n

Tactic:
linarith
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
rw :
  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)
⊢ 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:
rw [iterate_derivative_sum]

Premises used: Polynomial.iterate_derivative_sum
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
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
⊢ 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)

Tactic:
congr! 1 with x _
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ n.choose x • HPow.hPow (α := ℤ[X]) (-1) x = (C : (a : ℤ) → ℤ[X]) (n.choose x • HPow.hPow (α := ℤ) (-1) x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ n ≤ n + x

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ n + x - n = x

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
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
⊢ (⇑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:
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]

Premises used: Polynomial.iterate_derivative_X_pow_eq_smul, Nat.descFactorial_eq_div, Polynomial.iterate_derivative_C_mul
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
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
⊢ 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:
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]

Premises used: Int.cast_neg, Int.cast_natCast, zsmul_eq_mul, Int.reduceNeg, Int.cast_pow, eq_intCast, Int.cast_mul, nsmul_eq_mul, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ (↑(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:
ring
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
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])
⊢ 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:
congr! 2 with x _
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
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]))
⊢ 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:
rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]

Premises used: mul_assoc, Nat.cast, HPow.hPow, Nat.factorial, Polynomial.C_mul, mul_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : (↑((n + x)! / x !) : ℤ[X]) = HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X])
⊢ 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:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a :
  (↑((x + n)! / x !) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((x + n)! / (x ! * n !)) : ℤ)) (↑n ! : ℤ[X])
⊢ (↑((n + x)! / x !) : ℤ[X]) = HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (↑((n + x).choose n) : ℤ)) (↑n ! : ℤ[X])

Tactic:
rw [add_comm, add_choose]

Premises used: add_comm, Nat.add_choose
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / (x ! * n !) * n !) : ℤ[X])
⊢ (↑((x + n)! / x !) : ℤ[X]) =
    HMul.hMul (α := ℤ[X]) (↑((↑(x + n)! : ℤ) / HMul.hMul (α := ℤ) (↑x ! : ℤ) (↑n ! : ℤ)) : ℤ[X]) (↑n ! : ℤ[X])

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])
a₁ : x ! * n ! ∣ (x + n)!
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / (x ! * n !) * n !) : ℤ[X])

Tactic:
rw [mul_comm, ← Nat.mul_div_assoc]

Premises used: mul_comm, Nat.mul_div_assoc
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ 0 < n !

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
a : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! * n ! / (x ! * n !)) : ℤ[X])
a₁ a₂ : Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑((x + n)! / x !) : ℤ[X])
⊢ Eq (α := ℤ[X]) (↑((x + n)! / x !) : ℤ[X]) (↑(n ! * (x + n)! / (x ! * n !)) : ℤ[X])

Tactic:
rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]

Premises used: Nat.mul_div_mul_right, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ x ! * n ! ∣ (x + n)!

Tactic:
simp only [factorial_mul_factorial_dvd_factorial_add]

Premises used: Nat.factorial_mul_factorial_dvd_factorial_add
-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
⊢ ∑ 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 =
    (↑n ! : ℤ[X]) * shiftedLegendre n

Tactic:
simp [← mul_assoc, shiftedLegendre, mul_sum]

Premises used: Finset.mul_sum, mul_assoc, Polynomial.shiftedLegendre