awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
this : natDegree.{u_1} (R := R) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f) ≤ 0
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) (coeff ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f) 0) : R[X])
    ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₁ :
  Eq (α := R[X])
    ((C : (a : R) → R[X]) ((↑((0 + f.natDegree).choose f.natDegree) : R) * f.coeff (0 + f.natDegree)) : R[X])
    ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₂ :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(f.natDegree.choose f.natDegree) : R) * f.coeff f.natDegree) : R[X])
    ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₃ :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑1 : R) * f.coeff f.natDegree) : R[X])
    ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₄ :
  Eq (α := R[X]) ((C : (a : R) → R[X]) (1 * f.coeff f.natDegree) : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₅ : Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff f.natDegree) : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
rw₆ rw₇ :
  Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff f.natDegree) : R[X]) ((C : (a : R) → R[X]) (f.coeff f.natDegree) : R[X])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])

Tactic:
rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]

Premises used: Polynomial.eq_C_of_natDegree_le_zero, Polynomial.leadingCoeff, Polynomial.hasseDeriv_coeff, zero_add, Nat.cast_one, Nat.choose_self, one_mul
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) = p.natDegree - n

Tactic:
map_natDegree_eq_sub (fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _) ?_

Premises used: Polynomial.map_natDegree_eq_sub, Polynomial.hasseDeriv_eq_zero_of_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
refine :
  ∀ (n_1 : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) ((monomial n_1 : (a : R) → R[X]) c)) = n_1 - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) = p.natDegree - n

Tactic:
refine map_natDegree_eq_sub (fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _) ?_

Premises used: Polynomial.map_natDegree_eq_sub, Polynomial.hasseDeriv_eq_zero_of_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
simp : ∀ (n_1 : ℕ) (c : R), ¬c = 0 → (↑(n_1.choose n) : R) * c = 0 → 0 = n_1 - n
⊢ ∀ (n_1 : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) ((monomial n_1 : (a : R) → R[X]) c)) = n_1 - n

Tactic:
simp only [Ne, hasseDeriv_monomial, natDegree_monomial, ite_eq_right_iff]

Premises used: Ne, Polynomial.hasseDeriv_monomial, Polynomial.natDegree_monomial, ite_eq_right_iff
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ∀ (n_1 : ℕ) (c : R), ¬c = 0 → (↑(n_1.choose n) : R) * c = 0 → 0 = n_1 - n

Tactic:
simp +contextual [← nsmul_eq_mul, Nat.choose_eq_zero_iff, le_of_lt]

Premises used: Nat.choose_eq_zero_iff, le_of_lt, nsmul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
refine :
  ∀ (n_1 : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) ((monomial n_1 : (a : R) → R[X]) c)) = n_1 - n
refine₁ : ∀ (n_1 : ℕ) (c : R), ¬c = 0 → (↑(n_1.choose n) : R) * c = 0 → 0 = n_1 - n
⊢ natDegree.{u_1} (R := R) ((hasseDeriv n : (a : R[X]) → R[X]) p) = p.natDegree - n

Tactic:
classical
  refine map_natDegree_eq_sub (fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _) ?_
  simp only [Ne, hasseDeriv_monomial, natDegree_monomial, ite_eq_right_iff]
  simp +contextual [← nsmul_eq_mul, Nat.choose_eq_zero_iff, le_of_lt]

Premises used: Nat.choose_eq_zero_iff, le_of_lt, Ne, Polynomial.hasseDeriv_monomial, Polynomial.natDegree_monomial, ite_eq_right_iff, Polynomial.map_natDegree_eq_sub, nsmul_eq_mul, Polynomial.hasseDeriv_eq_zero_of_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f g : R[X]
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
Φ₁ :
  Eq (α := R[X])
    ((((AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ k,
        (((((AddMonoidHom.flip
                          (AddMonoidHom.comp compHom
                            ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                  (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                                (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                              (D ij.1))) :
                        (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                      (D ij.2) :
                    R[X] →+ R[X] →+ R[X]) :
                  (a : R[X]) → R[X] →+ R[X])
                f :
              R[X] →+ R[X]) :
            (a : R[X]) → R[X])
          g :
      R[X])
⊢ Eq (α := R[X]) ((hasseDeriv k : (a : R[X]) → R[X]) (f * g) : R[X])
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ k,
        HMul.hMul (α := R[X]) (β := R[X]) ((hasseDeriv ij.1 : (a : R[X]) → R[X]) f : R[X])
          ((hasseDeriv ij.2 : (a : R[X]) → R[X]) g : R[X]) :
      R[X])

Tactic:
change
    (compHom (D k)).comp Φ f g =
      ∑ ij ∈ antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g

Premises used: AddMonoidHom.compHom, AddMonoidHom.comp, DFunLike.coe, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f g : R[X]
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
simp :
  Eq (α := R[X])
    ((((AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])
    ((((∑ x ∈ @antidiagonal _ instAddMonoid _ k,
                  (AddMonoidHom.flip
                        (AddMonoidHom.comp compHom
                          ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                              (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                            (D x.1))) :
                      (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                    (D x.2) :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])
⊢ Eq (α := R[X])
    ((((AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])
    (∑ ij ∈ @antidiagonal _ instAddMonoid _ k,
        (((((AddMonoidHom.flip
                          (AddMonoidHom.comp compHom
                            ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                  (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                                (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                              (D ij.1))) :
                        (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                      (D ij.2) :
                    R[X] →+ R[X] →+ R[X]) :
                  (a : R[X]) → R[X] →+ R[X])
                f :
              R[X] →+ R[X]) :
            (a : R[X]) → R[X])
          g :
      R[X])

Tactic:
simp only [← finsetSum_apply]

Premises used: AddMonoidHom.finsetSum_apply
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
f g : R[X]
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
e_a :
  Eq (α := R[X] →+ R[X] →+ R[X])
    (AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
      (AddMonoidHom.flip
            (AddMonoidHom.comp compHom
              ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                    (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                  (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                (D x.1))) :
          (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
        (D x.2))
⊢ Eq (α := R[X])
    ((((AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])
    ((((∑ x ∈ @antidiagonal _ instAddMonoid _ k,
                  (AddMonoidHom.flip
                        (AddMonoidHom.comp compHom
                          ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                              (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                            (D x.1))) :
                      (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                    (D x.2) :
                (a : R[X]) → R[X] →+ R[X])
              f :
            R[X] →+ R[X]) :
          (a : R[X]) → R[X])
        g :
      R[X])

Tactic:
congr 2
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
e_a :
  ∀ (m : ℕ) (r : R) (n : ℕ) (s : R),
    Eq (α := R[X])
      ((AddMonoidHom.comp
              ((AddMonoidHom.comp
                    (AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ)
                    (LinearMap.toAddMonoidHom (monomial m)) :
                  (a : R) → R[X] →+ R[X])
                r)
              (LinearMap.toAddMonoidHom (monomial n)) :
            (a : R) → R[X])
          s :
        R[X])
      ((AddMonoidHom.comp
              ((AddMonoidHom.comp
                    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
                      (AddMonoidHom.flip
                            (AddMonoidHom.comp compHom
                              ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                    (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                                  (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                                (D x.1))) :
                          (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                        (D x.2))
                    (LinearMap.toAddMonoidHom (monomial m)) :
                  (a : R) → R[X] →+ R[X])
                r)
              (LinearMap.toAddMonoidHom (monomial n)) :
            (a : R) → R[X])
          s :
        R[X])
⊢ Eq (α := R[X] →+ R[X] →+ R[X])
    (AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
      (AddMonoidHom.flip
            (AddMonoidHom.comp compHom
              ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                    (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                  (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                (D x.1))) :
          (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
        (D x.2))

Tactic:
ext m r n s : 4
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
e_a :
  Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
      R[X])
⊢ Eq (α := R[X])
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp
                  (AddMonoidHom.comp ((compHom : (a : R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X]) (D k)) Φ)
                  (LinearMap.toAddMonoidHom (monomial m)) :
                (a : R) → R[X] →+ R[X])
              r)
            (LinearMap.toAddMonoidHom (monomial n)) :
          (a : R) → R[X])
        s :
      R[X])
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp
                  (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
                    (AddMonoidHom.flip
                          (AddMonoidHom.comp compHom
                            ((((compHom : (a : R[X] →+ R[X] →+ R[X]) → (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) Φ :
                                  (R[X] →+ R[X]) →+ R[X] →+ R[X] →+ R[X]) :
                                (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                              (D x.1))) :
                        (a : R[X] →+ R[X]) → R[X] →+ R[X] →+ R[X])
                      (D x.2))
                  (LinearMap.toAddMonoidHom (monomial m)) :
                (a : R) → R[X] →+ R[X])
              r)
            (LinearMap.toAddMonoidHom (monomial n)) :
          (a : R) → R[X])
        s :
      R[X])

Tactic:
simp only [Φ, D, finsetSum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply,
             hasseDeriv_monomial, LinearMap.toAddMonoidHom_coe, compHom_apply_apply,
             coe_mul, monomial_mul_monomial]

Premises used: LinearMap.toAddMonoidHom_coe, AddMonoidHom.flip_apply, AddMonoidHom.compHom_apply_apply, Polynomial.hasseDeriv_monomial, AddMonoidHom.finsetSum_apply, AddMonoidHom.coe_mul, AddMonoidHom.coe_comp, Function.comp_apply, AddMonoidHom.coe_mulLeft, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ instAddMonoid _ k
⊢ x.1 + x.2 = k

Tactic:
rw [mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.1 + x.2 = k
subst :
  Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - k) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
subst hx
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
pos :
  ∀ (hm : m < x.1),
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
neg :
  ∀ (hm : x.1 ≤ m),
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
by_cases! hm : m < x.1

Premises used: Prod.fst
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.1
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul,
                 monomial_zero_right]

Premises used: MulZeroClass.zero_mul, 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
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
pos :
  ∀ (hn : n < x.2),
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
neg :
  ∀ (hn : x.2 ≤ n),
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
by_cases! hn : n < x.2

Premises used: Prod.snd
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : n < x.2
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul,
                 mul_zero, monomial_zero_right]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, 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 : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])

Tactic:
have aux :
    ∀ x : ℕ × ℕ,
      x ∈ antidiagonal k →
        monomial (m - x.1 + (n - x.2)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
          monomial (m + n - k) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s)) := by
    intro x hx
    rw [mem_antidiagonal] at hx
    subst hx
    by_cases! hm : m < x.1
    · simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul,
                 monomial_zero_right]
    by_cases! hn : n < x.2
    · simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul,
                 mul_zero, monomial_zero_right]
    rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub,
      add_comm x.2 x.1, mul_assoc, ← mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
e_a :
  Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
      R[X])

Tactic:
rw [Finset.sum_congr rfl aux]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    Eq (α := R[X])
      ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) :
        R[X])
      ((monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
e_a :
  Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    ((monomial (m + n - k) : (a : R) → R[X])
        ((∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R)) *
          (r * s)) :
      R[X])
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
rw [← map_sum, ← Finset.sum_mul]

Premises used: map_sum, Finset.sum_mul