awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ ((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
have neg : ¬i ≤ n → HAdd.hAdd (α := M) 0 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
          ((single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then
      HSMul.hSMul (β := M) r
        ((((single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) : (a : ℕ) → M) (n - i) : M)
    else 0
have single : (if i + a = n then r • b else 0) = if i ≤ n ∧ a = n - i then r • b else 0
Tactic: rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ
⊢ (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
have 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
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
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (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
have 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
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
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (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
have single : ∀ (a : ℕ) (b : M),
  (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
          ((single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) :
        (a : ℕ) → M)
      n =
    if i ≤ n then
      HSMul.hSMul (β := M) r
        ((((single R a : (a : M) → PolynomialModule R M) b : PolynomialModule R M) : (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
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (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
have 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
Tactic: rw [add_smul, add_apply, hp, hq, coeff_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ ((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
have pos : i ≤ n → p.coeff (n - i) • m + q.coeff (n - i) • m = p.coeff (n - i) • m + q.coeff (n - i) • m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ ((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
have neg : ¬i ≤ n → HAdd.hAdd (α := M) 0 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ
⊢ (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
have 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
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (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
have monomial : ∀ (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: 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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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)
have 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))
Tactic: rw [add_smul, add_apply, hp, hq, ← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ × ℕ
⊢ 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)
have 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)
Tactic: rw [coeff_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [coeff_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ Eq (α := M) ((HSMul.hSMul (α := R[X]) ((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 ((monomial f_n : (a : R) → R[X]) f_a) x.1)
          ((g : (a : ℕ) → M) x.2 : M) :
      M)
have 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 ((monomial f_n : (a : R) → R[X]) f_a) k)
      ((g : (a : ℕ) → M) (n - k) : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 ≤ 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 ((monomial f_n : (a : R) → R[X]) f_a) k)
        ((g : (a : ℕ) → M) (n - k) : M)
have 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)
Tactic: simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ
⊢ 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)
have 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)
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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)
have monomial : ∀ (f_n : ℕ) (f_a : R),
  Eq (α := M) ((HSMul.hSMul (α := R[X]) ((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 ((monomial f_n : (a : R) → R[X]) f_a) 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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
x : PolynomialModule R R
⊢ Equiv.toFun (RingEquiv.toEquiv (RingEquiv.symm (toFinsuppIso R))) (r • x) =
    HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) r : R[X])
      (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.symm (toFinsuppIso R))) x)
have dsimp : (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • x) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) x : R[X])
Tactic: dsimp only [RingEquiv.toEquiv_eq_coe, RingEquiv.coe_toEquiv_symm, Equiv.toFun_as_coe,
        RingHom.id_apply, smul_eq_mul, RingEquiv.coe_coe_toEquiv_symm]