awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : HasQuotient.Quotient G (B := Subgroup G) (stabilizer G x)
rw :
  g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₁ :
  HSMul.hSMul (β := R[X]) g X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₂ :
  X - HSMul.hSMul (β := R[X]) g ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
rw₃ rw₄ :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (g • ofQuotientStabilizer G x g') : R[X])
⊢ g • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x g') : R[X]) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ofQuotientStabilizer G x (g • g')) : R[X])

Tactic:
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

Premises used: Polynomial.smul_X, smul_sub, Polynomial.smul_C, MulAction.ofQuotientStabilizer_smul
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
G : Type u_2
inst : Group G
inst_1 : Fintype G
R : Type u_3
inst_2 : CommRing R
inst_3 : MulSemiringAction G R
x : R
g : G
n : ℕ
rw : (HSMul.hSMul (β := R[X]) g (prodXSubSMul G R x)).coeff n = Polynomial.coeff (prodXSubSMul G R x) n
rw₁ rw₂ : Polynomial.coeff (prodXSubSMul G R x) n = Polynomial.coeff (prodXSubSMul G R x) n
⊢ g • Polynomial.coeff (prodXSubSMul G R x) n = Polynomial.coeff (prodXSubSMul G R x) n

Tactic:
rw [← Polynomial.coeff_smul, prodXSubSMul.smul]

Premises used: prodXSubSMul.smul, Polynomial.coeff_smul
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p : P[X]
b : P
rw :
  map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₁ :
  map (↑g : P →+* Q) ((C : (a : P) → P[X]) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₂ :
  (C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₃ :
  (C : (a : Q) → Q[X]) ((g : (a : P) → Q) (m • b)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₄ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))
rw₅ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) (((↑g : P →+* Q) : (a : P) → Q) b) : Q[X])
rw₆ :
  (C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) =
    HSMul.hSMul (β := Q[X]) m ((C : (a : Q) → Q[X]) ((g : (a : P) → Q) b) : Q[X])
rw₇ rw₈ :
  Eq (α := Q[X]) ((C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) : Q[X])
    ((C : (a : Q) → Q[X]) (HSMul.hSMul (β := Q) m ((g : (a : P) → Q) b : Q)) : Q[X])
⊢ map (↑g : P →+* Q) (HSMul.hSMul (β := P[X]) m ((C : (a : P) → P[X]) b : P[X])) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M)
      (map (↑g : P →+* Q) ((C : (a : P) → P[X]) b))

Tactic:
rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C,
          coe_fn_coe, smul_C]

Premises used: MulSemiringActionHom.map_smul, MulSemiringActionHom.coe_fn_coe, MonoidHom.id_apply, Polynomial.smul_C, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
m : M
p_1 p q : P[X]
ihp :
  map (↑g : P →+* Q) (m • p) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p)
ihq :
  map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
rw :
  map (↑g : P →+* Q) (m • p + m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₁ :
  HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) (m • p)) (map (↑g : P →+* Q) (m • q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₂ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      map (↑g : P →+* Q) (m • q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₃ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))
rw₄ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
    HSMul.hSMul (α := M) ((MonoidHom.id M : (a : M) → M) m : M)
      (HAdd.hAdd (α := Q[X]) (map (↑g : P →+* Q) p) (map (↑g : P →+* Q) q))
rw₅ rw₆ :
  HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) p) +
      HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) q)
⊢ map (↑g : P →+* Q) (m • (p + q)) =
    HSMul.hSMul (α := M) (β := Q[X]) ((MonoidHom.id M : (a : M) → M) m : M) (map (↑g : P →+* Q) (p + q))

Tactic:
rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]

Premises used: Polynomial.map_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.GroupRingAction
Goal:
M : Type u_1
inst : Monoid M
P : Type u_2
inst_1 : CommSemiring P
inst_2 : MulSemiringAction M P
Q : Type u_3
inst_3 : CommSemiring Q
inst_4 : MulSemiringAction M Q
g : P →+*[M] Q
⊢ Eq (α := (a : P[X]) → Q[X]) (⇑g.polynomial : (a : P[X]) → Q[X]) (map (↑g : P →+* Q))

Tactic:
rfl

Premises used: Polynomial.map, rfl
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
dsimp :
  Eq (α := R[X]) (f.sum fun (x1 : ℕ) (x2 : R) ↦ (monomial (x1 - k) : (a : R) → R[X]) (x1.choose k • x2))
    (f.sum fun (i : ℕ) (r : R) ↦ (monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * r))
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) f : R[X])
    (f.sum fun (i : ℕ) (r : R) ↦ (monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * r) : R[X])

Tactic:
dsimp [hasseDeriv]

Premises used: Polynomial.hasseDeriv
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
⊢ Eq (α := R[X]) (f.sum fun (x1 : ℕ) (x2 : R) ↦ (monomial (x1 - k) : (a : R) → R[X]) (x1.choose k • x2))
    (f.sum fun (i : ℕ) (r : R) ↦ (monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * r))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
rw :
  (if n + k - k = n then (↑((n + k).choose k) : R) * f.coeff (n + k) else 0) =
    (↑((n + k).choose k) : R) * f.coeff (n + k)
h₀ :
  ∀ b ∈ f.support,
    b ≠ n + k →
      Eq.{u_1 + 1} (α := R) (coeff ((monomial (b - k) : (a : R) → R[X]) ((↑(b.choose k) : R) * f.coeff b)) n) 0
h₁ :
  n + k ∉ f.support →
    Eq.{u_1 + 1} (α := R)
      (coeff ((monomial (n + k - k) : (a : R) → R[X]) ((↑((n + k).choose k) : R) * f.coeff (n + k))) n) 0
⊢ coeff ((hasseDeriv k : (a : R[X]) → R[X]) f) n = (↑((n + k).choose k) : R) * f.coeff (n + k)

Tactic:
rw [hasseDeriv_apply, coeff_sum, sum_def, Finset.sum_eq_single (n + k), coeff_monomial]

Premises used: Polynomial.coeff_monomial, Finset.sum_eq_single, Polynomial.coeff_sum, HAdd.hAdd, Polynomial.sum_def, Polynomial.hasseDeriv_apply
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then (↑((n + k).choose k) : R) * f.coeff (n + k) else 0) =
    (↑((n + k).choose k) : R) * f.coeff (n + k)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
h₀ : (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
⊢ Eq.{u_1 + 1} (α := R) (coeff ((monomial (i - k) : (a : R) → R[X]) ((↑(i.choose k) : R) * f.coeff i)) n) 0

Tactic:
rw [coeff_monomial]

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
pos : ∀ (hik : i < k), (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
neg : ∀ (hik : ¬i < k), (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0
⊢ (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0

Tactic:
by_cases hik : i < k
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : i < k
⊢ (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0

Tactic:
simp only [Nat.choose_eq_zero_of_lt hik, ite_self, Nat.cast_zero, zero_mul]

Premises used: ite_self, MulZeroClass.zero_mul, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n i : ℕ
_hi : i ∈ f.support
hink : i ≠ n + k
hik : ¬i < k
⊢ (if i - k = n then (↑(i.choose k) : R) * f.coeff i else 0) = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f : R[X]
n : ℕ
h : n + k ∉ f.support
⊢ Eq.{u_1 + 1} (α := R)
    (coeff ((monomial (n + k - k) : (a : R) → R[X]) ((↑((n + k).choose k) : R) * f.coeff (n + k))) n) 0

Tactic:
simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.notMem_support_iff, Polynomial.monomial_zero_right, Iff.mp, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ (hasseDeriv 0 : (a : R[X]) → R[X]) f = f

Tactic:
simp only [hasseDeriv_apply, Nat.sub_zero, choose_zero_right, cast_one, one_mul, sum_monomial_eq]

Premises used: Polynomial.sum_monomial_eq, Polynomial.hasseDeriv_apply, Nat.sub_zero, Nat.cast_one, Nat.choose_zero_right, one_mul
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X] →ₗ[R] R[X]) (hasseDeriv 0) LinearMap.id

Tactic:
LinearMap.ext <| hasseDeriv_zero'

Premises used: Polynomial.hasseDeriv_zero', LinearMap.ext
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
rw :
  Eq.{u_1 + 1} (α := R[X])
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) 0
⊢ Eq (α := R[X]) ((hasseDeriv n : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])

Tactic:
rw [hasseDeriv_apply, sum_def]

Premises used: Polynomial.sum_def, Polynomial.hasseDeriv_apply
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) 0

Tactic:
Finset.sum_eq_zero fun x hx => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
refine :
  ∀ (x : ℕ) (hx : x ∈ p.support),
    Eq (α := R[X]) ((monomial (x - n) : (a : R) → R[X]) ((↑(x.choose n) : R) * p.coeff x) : R[X]) (0 : R[X])
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ n_1 ∈ p.support, (monomial (n_1 - n) : (a : R) → R[X]) ((↑(n_1.choose n) : R) * p.coeff n_1)) 0

Tactic:
refine Finset.sum_eq_zero fun x hx => ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
x : ℕ
hx : x ∈ p.support
⊢ Eq (α := R[X]) ((monomial (x - n) : (a : R) → R[X]) ((↑(x.choose n) : R) * p.coeff x) : R[X]) (0 : R[X])

Tactic:
simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]

Premises used: Polynomial.le_natDegree_of_mem_supp, Nat.choose_eq_zero_of_lt, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ Eq (α := R[X]) ((hasseDeriv 1 : (a : R[X]) → R[X]) f : R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])

Tactic:
simp only [hasseDeriv_apply, derivative_apply, ← C_mul_X_pow_eq_monomial, Nat.choose_one_right,
    (Nat.cast_commute _ _).eq]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Nat.choose_one_right, Polynomial.hasseDeriv_apply, Commute.eq, Polynomial.derivative_apply, Nat.cast_commute
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X] →ₗ[R] R[X]) (hasseDeriv 1) derivative

Tactic:
LinearMap.ext <| hasseDeriv_one'

Premises used: Polynomial.hasseDeriv_one', LinearMap.ext
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
a :
  ∀ (i : ℕ),
    Eq.{u_1 + 1} (α := R) (coeff ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r)) i)
      (coeff ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r)) i)
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r) : R[X])
    ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r) : R[X])

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
a : ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ Eq.{u_1 + 1} (α := R) (coeff ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) r)) i)
    (coeff ((monomial (n - k) : (a : R) → R[X]) ((↑(n.choose k) : R) * r)) i)

Tactic:
simp only [hasseDeriv_coeff, coeff_monomial]

Premises used: Polynomial.coeff_monomial, Polynomial.hasseDeriv_coeff
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
pos :
  ∀ (hnik : n = i + k),
    ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
neg :
  ∀ (hnik : ¬n = i + k),
    ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
by_cases hnik : n = i + k
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : n = i + k
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
neg : 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ ((↑((i + k).choose k) : R) * if n = i + k then r else 0) = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
rw [if_neg hnik, mul_zero]

Premises used: MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
pos : ∀ (hkn : k ≤ n), 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
neg : ∀ (hkn : n < k), 0 = if n - k = i then (↑(n.choose k) : R) * r else 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
by_cases! hkn : k ≤ n
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ ¬n - k = i

Tactic:
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik

Premises used: tsub_eq_iff_eq_add_of_le
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
hnik₁ : ¬n - k = i
⊢ k ≤ n

Tactic:
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik

Premises used: tsub_eq_iff_eq_add_of_le
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n - k = i
hkn : k ≤ n
pos pos₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
rw [if_neg hnik]

Premises used: if_neg
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : n < k
neg : 0 = if n - k = i then (↑0 : R) * r else 0
neg₁ : 0 = if n - k = i then 0 * r else 0
neg₂ : Eq.{u_1 + 1} (α := R) 0 (if n - k = i then 0 else 0)
neg₃ neg₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = if n - k = i then (↑(n.choose k) : R) * r else 0

Tactic:
rw [Nat.choose_eq_zero_of_lt hkn, Nat.cast_zero, zero_mul, ite_self]

Premises used: ite_self, MulZeroClass.zero_mul, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
r : R
hk : 0 < k
rw : Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 0 : (a : R) → R[X]) r) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑(choose 0 k) : R) * r) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) ((↑0 : R) * r) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) (0 * r) : R[X]) (0 : R[X])
rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (0 - k) : (a : R) → R[X]) 0) 0
rw₅ rw₆ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) (0 : R[X])

Tactic:
rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]

Premises used: MulZeroClass.zero_mul, Polynomial.hasseDeriv_monomial, Polynomial.monomial_zero_right, Nat.choose_eq_zero_of_lt, Polynomial.monomial_zero_left, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 0 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) 1) 0

Tactic:
rw [← C_1, hasseDeriv_C k _ hk]

Premises used: Polynomial.C_1, Polynomial.hasseDeriv_C
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
hk : 1 < k
rw : Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) ((monomial 1 : (a : R) → R[X]) 1) : R[X]) (0 : R[X])
rw₁ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑(choose 1 k) : R) 1) : R[X]) (0 : R[X])
rw₂ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) (↑0 : R) 1) : R[X]) (0 : R[X])
rw₃ : Eq (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) (HMul.hMul (α := R) 0 1) : R[X]) (0 : R[X])
rw₄ : Eq.{u_1 + 1} (α := R[X]) ((monomial (1 - k) : (a : R) → R[X]) 0) 0
rw₅ rw₆ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq.{u_1 + 1} (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) X : R[X]) (0 : R[X])

Tactic:
rw [← monomial_one_one_eq_X, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]

Premises used: Polynomial.monomial_one_one_eq_X, MulZeroClass.zero_mul, Polynomial.hasseDeriv_monomial, Polynomial.monomial_zero_right, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
zero :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₁ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]
zero₂ :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (α := ℕ) (β := R[X] →ₗ[R] R[X]) 1 LinearMap.id) : (a : R[X]) → R[X]) id
zero₃ : Eq.{u_1 + 1} (α := (a : R[X]) → R[X]) (⇑LinearMap.id : (a : R[X]) → R[X]) id
zero₄ zero₅ : Eq.{u_1 + 1} (α := (a : R[X]) → R[X]) id id
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) 0! (hasseDeriv 0)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[0]

Tactic:
rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]

Premises used: LinearMap.id_coe, Function.iterate_zero, Polynomial.hasseDeriv_zero, one_smul, Nat.factorial_zero
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1))) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k + 1]

Tactic:
?_
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
succ :
  ∀ (k : ℕ)
    (ih :
      Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
        (⇑derivative : (a : R[X]) → R[X])^[k]),
    Eq (α := (a : R[X]) → R[X])
      (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1))) : (a : R[X]) → R[X])
      (⇑derivative : (a : R[X]) → R[X])^[k + 1]
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]

Tactic:
induction k with
  | zero => rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
  | succ k ih => ?_

Premises used: LinearMap.id_coe, Function.iterate_zero, Polynomial.hasseDeriv_zero, one_smul, Nat.zero, Nat.factorial_zero, Nat.succ
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
succ :
  ∀ (f : R[X]) (n : ℕ),
    coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n =
      ((⇑derivative : (a : R[X]) → R[X])^[k + 1] f).coeff n
⊢ Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1))) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k + 1]

Tactic:
ext f n : 2
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k_1 k : ℕ
ih :
  Eq (α := (a : R[X]) → R[X]) (⇑(HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k)) : (a : R[X]) → R[X])
    (⇑derivative : (a : R[X]) → R[X])^[k]
f : R[X]
n : ℕ
succ :
  Eq.{u_1 + 1} (α := R)
    (coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n)
    (coeff
      ((derivative : (a : R[X]) → R[X]) ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) k ! (hasseDeriv k) : (a : R[X]) → R[X]) f))
      n)
⊢ coeff ((HSMul.hSMul (β := R[X] →ₗ[R] R[X]) (k + 1)! (hasseDeriv (k + 1)) : (a : R[X]) → R[X]) f) n =
    ((⇑derivative : (a : R[X]) → R[X])^[k + 1] f).coeff n

Tactic:
rw [iterate_succ_apply', ← ih]

Premises used: Function.iterate_succ_apply'