awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have rw₅ : Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff f.natDegree) : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ Eq (α := R[X]) ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
have 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])
Tactic: rw [eq_C_of_natDegree_le_zero this, hasseDeriv_coeff, zero_add, Nat.choose_self,
    Nat.cast_one, one_mul, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
have 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
Tactic: refine map_natDegree_eq_sub (fun h => hasseDeriv_eq_zero_of_lt_natDegree _ _) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
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
have simp : ∀ (n_1 : ℕ) (c : R), ¬c = 0 → (↑(n_1.choose n) : R) * c = 0 → 0 = n_1 - n
Tactic: simp only [Ne, hasseDeriv_monomial, natDegree_monomial, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
have refine₁ : ∀ (n_1 : ℕ) (c : R), ¬c = 0 → (↑(n_1.choose n) : R) * c = 0 → 0 = n_1 - 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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]) ((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])
have Φ₁ : 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: change
    (compHom (D k)).comp Φ f g =
      ∑ ij ∈ antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
have 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])
Tactic: simp only [← finsetSum_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
    ((((∑ 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])
have 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))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ 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))
have 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])
Tactic: ext m r n s : 4
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
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
⊢ 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])
have hx₁ : x.1 + x.2 = k
Tactic: rw [mem_antidiagonal] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ 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])
have 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])
Tactic: subst hx
Cleared hypotheses: k, hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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 : ℕ × ℕ
⊢ 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])
have 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])
Tactic: by_cases! hm : m < x.1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
Tactic: by_cases! hm : m < x.1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ 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])
have 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])
Tactic: by_cases! hn : n < x.2