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 : 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]
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (HSMul.hSMul (β := PolynomialModule R R) r 0) =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
have zero : (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0 =
  r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
Tactic: rw [smul_zero, map_zero, mul_zero]
-- 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]
zero :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0 =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (HSMul.hSMul (β := PolynomialModule R R) r 0) =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
have zero₁ : 0 = r * 0
Tactic: rw [smul_zero, map_zero, mul_zero]
-- 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]
zero :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0 =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
zero₁ : 0 = r * 0
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (HSMul.hSMul (β := PolynomialModule R R) r 0) =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
have zero₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [smul_zero, map_zero, mul_zero]
-- 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]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add : (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]
-- 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]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add₁ : HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
    ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]
-- 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]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₁ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add₂ : HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
    ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
  r *
    HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]
-- 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]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₁ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₂ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    r *
      HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
        ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add₃ : HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
    ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]
-- 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]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₁ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₂ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    r *
      HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
        ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add₃ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add₄ : HAdd.hAdd (β := R[X])
    (HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]))
    ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]
-- 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]
n : ℕ
a : R
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
      (HSMul.hSMul (β := PolynomialModule R R) r
        ((single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)) =
    HMul.hMul (β := R[X]) r
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
          ((single R n : (a : R) → PolynomialModule R R) a) :
        R[X])
have single : ∀ (i : ℕ),
  coeff
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
        (HSMul.hSMul (β := PolynomialModule R R) r
          ((single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)))
      i =
    (HMul.hMul (β := R[X]) r
          ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
              ((single R n : (a : R) → PolynomialModule R R) a) :
            R[X])).coeff
      i
Tactic: ext i
-- 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]
n : ℕ
a : R
i : ℕ
⊢ coeff
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
        (HSMul.hSMul (β := PolynomialModule R R) r
          ((single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)))
      i =
    (HMul.hMul (β := R[X]) r
          ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
              ((single R n : (a : R) → PolynomialModule R R) a) :
            R[X])).coeff
      i
have single : (if n ≤ i then r.coeff (i - n) * a else 0) =
  ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
Tactic: simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply,
          smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero]
-- 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]
n : ℕ
a : R
i : ℕ
⊢ (if n ≤ i then r.coeff (i - n) * a else 0) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
have pos : ∀ (hn : n ≤ i),
  r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
Tactic: split_ifs with hn
-- 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]
n : ℕ
a : R
i : ℕ
pos :
  ∀ (hn : n ≤ i),
    r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
⊢ (if n ≤ i then r.coeff (i - n) * a else 0) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
have neg : ∀ (hn : ¬n ≤ i),
  Eq.{u_1 + 1} (α := R) 0 (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0)
Tactic: split_ifs with hn
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
have pos : r.coeff (i - n) * a = if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0
Tactic: rw [Finset.sum_eq_single (i - n, n)]
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
pos : r.coeff (i - n) * a = if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0
⊢ r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
have pos₁ : ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, b ≠ (i - n, n) → (if n = b.2 then r.coeff b.1 * a else 0) = 0
Tactic: rw [Finset.sum_eq_single (i - n, n)]
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
pos : r.coeff (i - n) * a = if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0
pos₁ : ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, b ≠ (i - n, n) → (if n = b.2 then r.coeff b.1 * a else 0) = 0
⊢ r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
have pos₂ : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i →
  (if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0) = 0
Tactic: rw [Finset.sum_eq_single (i - n, n)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (hypothesis)
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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).2 then r.coeff (p, q).1 * a else 0) = 0
have hpq1₁ : (p, q).1 + (p, q).2 = i
Tactic: rw [Finset.mem_antidiagonal] at hpq1
Cleared hypotheses: hpq1, hpq2
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).2 then r.coeff (p, q).1 * a else 0) = 0
have pos : ∀ (H : n = (p, q).2), r.coeff (p, q).1 * a = 0
Tactic: split_ifs with H
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
pos : ∀ (H : n = (p, q).2), r.coeff (p, q).1 * a = 0
⊢ (if n = (p, q).2 then r.coeff (p, q).1 * a else 0) = 0
have neg : ∀ (H : ¬n = (p, q).2), Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs with H
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ r.coeff (p, q).1 * a = 0
have pos : False
Tactic: exfalso
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ False
have pos : (p, q) = (i - n, n)
Tactic: apply hpq2
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = (i - n, n)
have pos : (p, q) = ((p, q).1 + (p, q).2 - q, q)
Tactic: rw [← hpq1, H]
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ (if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0) = 0
have pos : False
Tactic: exfalso
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ False
have pos : (i - n, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
Tactic: apply H
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ (i - n, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
have pos : (i - n, n).1 + (i - n, n).2 = i
Tactic: rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
-- 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]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
pos : (i - n, n).1 + (i - n, n).2 = i
⊢ (i - n, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
have pos₁ : i = i
Tactic: rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
-- 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]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ Eq.{u_1 + 1} (α := R) 0 (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0)
have neg : Eq.{u_1 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0) 0
Tactic: symm
-- 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]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0) 0
have neg : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, ¬n = x.2
Tactic: rw [Finset.sum_ite_of_false, Finset.sum_const_zero]