-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma coeff_preHilbertPoly_self [CharZero F] (d k : ℕ) :
    (preHilbertPoly F d k).coeff d = (d ! : F)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Tactic:
nth_rw 3 [heq]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree =
    (↑d !)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Tactic:
have hne : (d ! : F) ≠ 0 := by norm_cast; positivity

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).coeff d = (↑d !)⁻¹

Tactic:
delta preHilbertPoly

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Tactic:
have heq : d = ((ascPochhammer F d).comp (X - C (k : F) + 1)).natDegree :=
  (natDegree_preHilbertPoly F d k).symm.trans (natDegree_smul _ (inv_ne_zero hne))

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff = (↑d !)⁻¹

Tactic:
simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
  (monic_ascPochhammer _ _), one_mul, leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree =
    (↑d !)⁻¹ • ((ascPochhammer F d).comp (X - C (↑k - 1))).leadingCoeff

Tactic:
simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
hne : ↑d ! ≠ 0
heq : d = ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff ((ascPochhammer F d).comp (X - C ↑k + 1)).natDegree =
    (↑d !)⁻¹

Tactic:
calc
_ = (d ! : F)⁻¹ • ((ascPochhammer F d).comp (X - C ((k : F) - 1))).leadingCoeff := by
  simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]
_ = (d ! : F)⁻¹ := by
  simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero), Monic.def.1
    (monic_ascPochhammer _ _), one_mul, leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ¬d ! = 0

Tactic:
positivity

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ↑d ! ≠ 0

Tactic:
norm_cast

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ¬d ! = 0