awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  (↑(HAdd.hAdd (α := ↥R[X]_(m + n)) (β := ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1) :
            ↥R[X]_(m + n))
          ((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
              ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2) :
            ↥R[X]_(m + n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
rw₁ :
  HAdd.hAdd (α := R[X])
      (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1)) :
        R[X])
      (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2)) :
        R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
rw₂ :
  (↑PQ.1 : R[X]) +
      (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2)) :
        R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          (HAdd.hAdd (α := ↥R[X]_m × ↥R[X]_n) (β := ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_m) → ↥R[X]_m × ↥R[X]_n) PQ.1 : ↥R[X]_m × ↥R[X]_n)
            ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n : (a : ↥R[X]_n) → ↥R[X]_m × ↥R[X]_n) PQ.2 : ↥R[X]_m × ↥R[X]_n))) :
      R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
have rw₃ : (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X]) =
    (↑PQ.1 : R[X]) + HPow.hPow (α := R[X]) X m * (↑PQ.2 : R[X])
have rw : (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X]) =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [X_pow_mul, addLinearEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
rw :
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X]) =
    (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
⊢ (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n)) PQ) : R[X]) =
    (↑PQ.1 : R[X]) + HPow.hPow (α := R[X]) X m * (↑PQ.2 : R[X])
have rw₁ : (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m =
  (↑PQ.1 : R[X]) + (↑PQ.2 : R[X]) * HPow.hPow (α := R[X]) X m
Tactic: rw [X_pow_mul, addLinearEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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 ∧
    (↑((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
have rw : (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
    (↑((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 =
    (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
Tactic: rw [and_comm, eq_comm, eq_comm (b := _ %ₘ _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (hypothesis)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
⊢ (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((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 =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((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 =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
have refine_1 : (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
    HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
  (↑f : R[X])
Tactic: refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
refine_1 :
  (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
      HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X])
⊢ (↑f : R[X]) /ₘ HPow.hPow (α := R[X]) X m =
      (↑((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 =
      (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
have refine_2 : degree.{u_2} (R := R) (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) <
  (HPow.hPow (α := R[X]) X m).degree
Tactic: refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
      HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X])
have refine_1 : (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
        ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f)) :
    R[X]) =
  (↑f : R[X])
Tactic: rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
refine_1 :
  (↑((LinearEquiv.symm (addLinearEquiv R m n) : (a : ↥R[X]_m × ↥R[X]_n) → ↥R[X]_(m + n))
          ((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f)) :
      R[X]) =
    (↑f : R[X])
⊢ (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) +
      HPow.hPow (α := R[X]) X m * (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).2 : R[X]) =
    (↑f : R[X])
have refine_1₁ : (↑f : R[X]) = (↑f : R[X])
Tactic: rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
m n : ℕ
R : Type u_2
inst : Ring R
f : ↥R[X]_(m + n)
h : Nontrivial R
⊢ degree.{u_2} (R := R) (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X]) <
    (HPow.hPow (α := R[X]) X m).degree
have refine_2 : Membership.mem (γ := Submodule R R[X]) (R[X]_m)
  (↑((addLinearEquiv R m n : (a : ↥R[X]_(m + n)) → ↥R[X]_m × ↥R[X]_n) f).1 : R[X])
Tactic: rw [degree_X_pow, ← mem_degreeLT]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Submodule.comap (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n = R[X]_n
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Submodule.map (↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) R[X]_n = R[X]_n
have hf : Function.Surjective (α := R[X]) (β := R[X])
  (⇑(↑(↑(taylorEquiv r) : R[X] ≃ₗ[R] R[X]) : R[X] →ₗ[R] R[X]) : (a : R[X]) → R[X])
Tactic: nth_rw 1 [← comap_taylorEquiv_degreeLT (r := r), Submodule.map_comap_eq_of_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ 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)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
⊢ 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)
have 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)
Tactic: rw [← LinearMap.det_toMatrix (degreeLT.basis R n),
    Matrix.det_of_upperTriangular, Fintype.prod_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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)
⊢ 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)
have 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
Tactic: rw [← LinearMap.det_toMatrix (degreeLT.basis R n),
    Matrix.det_of_upperTriangular, Fintype.prod_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i : 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) i i :
      R)
    (1 : R)
have 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
Tactic: rw [LinearMap.toMatrix_apply, degreeLT.basis_repr, ← natDegree_X_pow (R := R) (i : ℕ)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i : Fin n
⊢ 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
have 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
Tactic: change (taylor r (degreeLT.basis R n i)).coeff _ = 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i : Fin n
⊢ 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
have 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
Tactic: rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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
⊢ 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
have h₁ : (HPow.hPow (α := R[X]) X (↑i : ℕ)).leadingCoeff = 1
Tactic: rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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
⊢ 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
have h₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [degreeLT.basis_val, coeff_taylor_natDegree, leadingCoeff_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ 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)
have 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
Tactic: rw [LinearMap.toMatrix_apply, LinearEquiv.coe_coe, degreeLT.basis_repr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ 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
have 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
Tactic: change (taylor r (degreeLT.basis R n j)).coeff i = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
h : Nontrivial R
i j : Fin n
hji : id j < id i
⊢ 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
have rw : Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (↑j : ℕ))) (↑i : ℕ)) 0
Tactic: rw [degreeLT.basis_val, coeff_eq_zero_of_degree_lt (by simpa [-taylor_X_pow, -taylor_pow])]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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
⊢ 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
have rw₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [degreeLT.basis_val, coeff_eq_zero_of_degree_lt (by simpa [-taylor_X_pow, -taylor_pow])]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : ↥R[X]_n ≃ₗ[R] ↥R[X]_n) → Rˣ) (taylorLinearEquiv r n)) : R) (↑1 : R)
have 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)
Tactic: rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : ↥R[X]_n ≃ₗ[R] ↥R[X]_n) → Rˣ) (taylorLinearEquiv r n)) : R) (↑1 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 1 (↑1 : R)
Tactic: rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : ↥R[X]_n ≃ₗ[R] ↥R[X]_n) → Rˣ) (taylorLinearEquiv r n)) : R) (↑1 : R)
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (↑n ! : ℤ[X]) * shiftedLegendre n =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n)
have symm : (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
  (↑n ! : ℤ[X]) * shiftedLegendre n
Tactic: symm
-- 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)
have 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)
Tactic: rw [← mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
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)
⊢ (⇑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)
have 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)
Tactic: rw [← mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
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)
⊢ (⇑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)
have 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)
Tactic: rw [← mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ (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)
have 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))
Tactic: rw [sub_eq_add_neg, add_comm, add_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ 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))
have 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)
Tactic: congr! 1 with m hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n 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)
have e_a : m ≤ n
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (hypothesis)
Goal:
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n
have hm₁ : m < n + 1
Tactic: rw [Finset.mem_range] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n m : ℕ
hm : m < n + 1
⊢ m ≤ n
have linarith : n < m →
  -1 + (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - (↑m : ℤ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ShiftedLegendre (goal)
Goal:
n : ℕ
⊢ 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)
have 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)
Tactic: rw [iterate_derivative_sum]