awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
add :
  ((if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0) +
      if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0) =
    if i ≤ n then
      HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
    else 0
⊢ (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) (p + q) : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p + q : (a : ℕ) → M) (n - i) : M) else 0

Tactic:
simp only [smul_add, add_apply, hp, hq]

Premises used: PolynomialModule.add_apply, smul_add
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
pos :
  i ≤ n →
    HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) =
      HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
neg : ¬i ≤ n → HAdd.hAdd (α := M) 0 0 = 0
⊢ ((if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0) +
      if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0) =
    if i ≤ n then
      HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
    else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
h : i ≤ n
⊢ HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) =
    HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
h : ¬i ≤ n
⊢ HAdd.hAdd (α := M) 0 0 = 0

Tactic:
zero_add 0

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
h : i ≤ n
⊢ HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) =
    HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)

Tactic:
exacts [rfl, zero_add 0]

Premises used: zero_add, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n a : ℕ
b : M
single : (if i + a = n then r • b else 0) = if i ≤ n ∧ a = n - i then r • b else 0
⊢ (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
          ((PolynomialModule.single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then
      HSMul.hSMul (β := M) r
        ((((PolynomialModule.single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) : (a : ℕ) → M)
            (n - i) :
          M)
    else 0

Tactic:
rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]

Premises used: PolynomialModule.monomial_smul_single, smul_zero, PolynomialModule.single_apply, smul_ite, ite_and
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
n a : ℕ
b : M
⊢ (if i + a = n then r • b else 0) = if i ≤ n ∧ a = n - i then r • b else 0

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
r : R
g : PolynomialModule R M
n : ℕ
zero :
  (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X]) 0 : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((0 : (a : ℕ) → M) (n - i) : M) else 0
add :
  ∀ (p q : PolynomialModule R M)
    (hp :
      (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
        if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0)
    (hq :
      (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
        if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0),
    (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) (p + q) : (a : ℕ) → M) n =
      if i ≤ n then HSMul.hSMul (β := M) r ((p + q : (a : ℕ) → M) (n - i) : M) else 0
single :
  ∀ (a : ℕ) (b : M),
    (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
            ((PolynomialModule.single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) :
          (a : ℕ) → M)
        n =
      if i ≤ n then
        HSMul.hSMul (β := M) r
          ((((PolynomialModule.single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) : (a : ℕ) → M)
              (n - i) :
            M)
      else 0
⊢ (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) g : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((g : (a : ℕ) → M) (n - i) : M) else 0

Tactic:
induction g using PolynomialModule.induction_linear with
  | zero => simp only [smul_zero, zero_apply, ite_self]
  | add p q hp hq =>
    simp only [smul_add, add_apply, hp, hq]
    split_ifs
    exacts [rfl, zero_add 0]
  | single =>
    rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
    grind

Premises used: PolynomialModule.add_apply, PolynomialModule.monomial_smul_single, ite_self, smul_zero, PolynomialModule.single_apply, PolynomialModule.single, PolynomialModule.zero_apply, zero_add, smul_ite, ite_and, OfNat.ofNat, smul_add, rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp :
  (HSMul.hSMul (β := PolynomialModule R M) p ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then p.coeff (n - i) • m else 0
hq :
  (HSMul.hSMul (β := PolynomialModule R M) q ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then q.coeff (n - i) • m else 0
add :
  ((if i ≤ n then p.coeff (n - i) • m else 0) + if i ≤ n then q.coeff (n - i) • m else 0) =
    if i ≤ n then p.coeff (n - i) • m + q.coeff (n - i) • m else 0
⊢ (HSMul.hSMul (β := PolynomialModule R M) (p + q)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then (p + q).coeff (n - i) • m else 0

Tactic:
rw [add_smul, add_apply, hp, hq, coeff_add, add_smul]

Premises used: PolynomialModule.add_apply, Polynomial.coeff_add, add_smul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp :
  (HSMul.hSMul (β := PolynomialModule R M) p ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then p.coeff (n - i) • m else 0
hq :
  (HSMul.hSMul (β := PolynomialModule R M) q ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then q.coeff (n - i) • m else 0
pos : i ≤ n → p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m
neg : ¬i ≤ n → HAdd.hAdd (α := M) 0 0 = 0
⊢ ((if i ≤ n then p.coeff (n - i) • m else 0) + if i ≤ n then q.coeff (n - i) • m else 0) =
    if i ≤ n then p.coeff (n - i) • m + q.coeff (n - i) • m else 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp :
  (HSMul.hSMul (β := PolynomialModule R M) p ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then p.coeff (n - i) • m else 0
hq :
  (HSMul.hSMul (β := PolynomialModule R M) q ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then q.coeff (n - i) • m else 0
h : i ≤ n
⊢ p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp :
  (HSMul.hSMul (β := PolynomialModule R M) p ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then p.coeff (n - i) • m else 0
hq :
  (HSMul.hSMul (β := PolynomialModule R M) q ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then q.coeff (n - i) • m else 0
h : ¬i ≤ n
⊢ HAdd.hAdd (α := M) 0 0 = 0

Tactic:
zero_add 0

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp :
  (HSMul.hSMul (β := PolynomialModule R M) p ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then p.coeff (n - i) • m else 0
hq :
  (HSMul.hSMul (β := PolynomialModule R M) q ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then q.coeff (n - i) • m else 0
h : i ≤ n
⊢ p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m

Tactic:
exacts [rfl, zero_add 0]

Premises used: zero_add, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
m : M
n n_1 : ℕ
a : R
⊢ (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial n_1 : (a : R) → R[X]) a : R[X])
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then HSMul.hSMul.{u_1, u_2, u_2} (α := R) (coeff ((monomial n_1 : (a : R) → R[X]) a) (n - i)) m else 0

Tactic:
grind [monomial_smul_single, single_apply, coeff_monomial, zero_smul]

Premises used: PolynomialModule.monomial_smul_single, PolynomialModule.single_apply, Polynomial.coeff_monomial, zero_smul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
i : ℕ
f : R[X]
m : M
n : ℕ
add :
  ∀ (p q : R[X])
    (hp :
      (HSMul.hSMul (β := PolynomialModule R M) p
              ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
            (a : ℕ) → M)
          n =
        if i ≤ n then p.coeff (n - i) • m else 0)
    (hq :
      (HSMul.hSMul (β := PolynomialModule R M) q
              ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
            (a : ℕ) → M)
          n =
        if i ≤ n then q.coeff (n - i) • m else 0),
    (HSMul.hSMul (β := PolynomialModule R M) (p + q)
            ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          (a : ℕ) → M)
        n =
      if i ≤ n then (p + q).coeff (n - i) • m else 0
monomial :
  ∀ (n_1 : ℕ) (a : R),
    (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((Polynomial.monomial n_1 : (a : R) → R[X]) a : R[X])
            ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          (a : ℕ) → M)
        n =
      if i ≤ n then
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (coeff ((Polynomial.monomial n_1 : (a : R) → R[X]) a) (n - i)) m
      else 0
⊢ (HSMul.hSMul (β := PolynomialModule R M) f ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then f.coeff (n - i) • m else 0

Tactic:
induction f using Polynomial.induction_on' with
  | add p q hp hq =>
    rw [add_smul, add_apply, hp, hq, coeff_add, add_smul]
    split_ifs
    exacts [rfl, zero_add 0]
  | monomial => grind [monomial_smul_single, single_apply, coeff_monomial, zero_smul]

Premises used: PolynomialModule.add_apply, PolynomialModule.monomial_smul_single, PolynomialModule.single_apply, Polynomial.monomial, Polynomial.coeff_monomial, Polynomial.coeff_add, zero_add, zero_smul, add_smul, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp :
  Eq (α := M) ((p • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
hq :
  Eq (α := M) ((q • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
add :
  Eq.{u_2 + 1} (α := M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      (HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M)))
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M))
⊢ Eq (α := M) (((p + q) • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)

Tactic:
rw [add_smul, add_apply, hp, hq, ← Finset.sum_add_distrib]

Premises used: PolynomialModule.add_apply, Finset.sum_add_distrib, add_smul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp :
  Eq (α := M) ((p • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
hq :
  Eq (α := M) ((q • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
add :
  Eq.{u_2 + 1} (α := ℕ × ℕ → M)
    (fun (x : ℕ × ℕ) ↦
      HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M))
    fun (x : ℕ × ℕ) ↦ HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M)
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      (HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M)))
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M))

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp :
  Eq (α := M) ((p • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
hq :
  Eq (α := M) ((q • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
add :
  ∀ (x : ℕ × ℕ),
    HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) =
      HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M)
⊢ Eq.{u_2 + 1} (α := ℕ × ℕ → M)
    (fun (x : ℕ × ℕ) ↦
      HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M))
    fun (x : ℕ × ℕ) ↦ HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp :
  Eq (α := M) ((p • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
hq :
  Eq (α := M) ((q • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)
x : ℕ × ℕ
add :
  HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
      HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) =
    HSMul.hSMul (β := M) (p.coeff x.1 + q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M)
add₁ add₂ :
  HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
      HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) =
    HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
      HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M)
⊢ HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) +
      HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) =
    HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M)

Tactic:
rw [coeff_add, add_smul]

Premises used: Polynomial.coeff_add, add_smul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
monomial :
  (if f_n ≤ n then HSMul.hSMul (β := M) f_a ((g : (a : ℕ) → M) (n - f_n) : M) else 0) =
    ∑ k ∈ Finset.range n.succ,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (coeff ((Polynomial.monomial f_n : (a : R) → R[X]) f_a) k)
        ((g : (a : ℕ) → M) (n - k) : M)
⊢ Eq (α := M) ((HSMul.hSMul (α := R[X]) ((Polynomial.monomial f_n : (a : R) → R[X]) f_a : R[X]) g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (coeff ((Polynomial.monomial f_n : (a : R) → R[X]) f_a) x.1)
          ((g : (a : ℕ) → M) x.2 : M) :
      M)

Tactic:
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j,
      monomial_smul_apply]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Polynomial.monomial, Polynomial.coeff, HSMul.hSMul, PolynomialModule.monomial_smul_apply, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
monomial :
  (if f_n ∈ Finset.range n.succ then HSMul.hSMul (β := M) f_a ((g : (a : ℕ) → M) (n - f_n) : M) else 0) =
    ∑ x ∈ Finset.range n.succ, HSMul.hSMul (β := M) (if f_n = x then f_a else 0) ((g : (a : ℕ) → M) (n - x) : M)
⊢ (if f_n ≤ n then HSMul.hSMul (β := M) f_a ((g : (a : ℕ) → M) (n - f_n) : M) else 0) =
    ∑ k ∈ Finset.range n.succ,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (coeff ((Polynomial.monomial f_n : (a : R) → R[X]) f_a) k)
        ((g : (a : ℕ) → M) (n - k) : M)

Tactic:
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]

Premises used: Finset.mem_range_succ_iff, Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ∈ Finset.range n.succ then HSMul.hSMul (β := M) f_a ((g : (a : ℕ) → M) (n - f_n) : M) else 0) =
    ∑ x ∈ Finset.range n.succ, HSMul.hSMul (β := M) (if f_n = x then f_a else 0) ((g : (a : ℕ) → M) (n - x) : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R[X]
g : PolynomialModule R M
n : ℕ
add :
  ∀ (p q : R[X])
    (hp :
      Eq (α := M) ((p • g : (a : ℕ) → M) n : M)
        (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
            HSMul.hSMul (β := M) (p.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
          M))
    (hq :
      Eq (α := M) ((q • g : (a : ℕ) → M) n : M)
        (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
            HSMul.hSMul (β := M) (q.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
          M)),
    Eq (α := M) (((p + q) • g : (a : ℕ) → M) n : M)
      (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
          HSMul.hSMul (β := M) ((p + q).coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
        M)
monomial :
  ∀ (f_n : ℕ) (f_a : R),
    Eq (α := M)
      ((HSMul.hSMul (α := R[X]) ((Polynomial.monomial f_n : (a : R) → R[X]) f_a : R[X]) g : (a : ℕ) → M) n : M)
      (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (coeff ((Polynomial.monomial f_n : (a : R) → R[X]) f_a) x.1)
            ((g : (a : ℕ) → M) x.2 : M) :
        M)
⊢ Eq (α := M) ((f • g : (a : ℕ) → M) n : M)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (f.coeff x.1) ((g : (a : ℕ) → M) x.2 : M) :
      M)

Tactic:
induction f using Polynomial.induction_on' with
  | add p q hp hq =>
    rw [add_smul, add_apply, hp, hq, ← Finset.sum_add_distrib]
    congr
    ext
    rw [coeff_add, add_smul]
  | monomial f_n f_a =>
    rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j,
      monomial_smul_apply]
    simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
    simp

Premises used: PolynomialModule.add_apply, Finset.sum_add_distrib, Finset.mem_range_succ_iff, Polynomial.monomial, Polynomial.coeff_monomial, Polynomial.coeff_add, add_smul, PolynomialModule.monomial_smul_apply