internlm/Lean-Github huggingface dataset:
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ φ 0 • s ⊗ₜ[R] n = (φ 0 * s) ⊗ₜ[R] n

case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0

case tmul.h_C.h₁
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0
Tactic:
rw [TensorProduct.smul_tmul', smul_eq_mul]
Proof state after:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0

case tmul.h_C.h₁
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0 → b ≠ 0 → φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0
Tactic:
intro b _ hb
Proof state after:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
b : ℕ
a✝ : ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ 0
⊢ φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
b : ℕ
a✝ : ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ 0
⊢ φ b • ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b = 0
Tactic:
simp only [rTensor_apply, rTensor_tmul, coe_restrictScalars, lcoeff_apply]
Proof state after:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
b : ℕ
a✝ : ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ 0
⊢ φ b • (C s).coeff b ⊗ₜ[R] n = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
b : ℕ
a✝ : ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ 0
⊢ φ b • (C s).coeff b ⊗ₜ[R] n = 0
Tactic:
rw [Polynomial.coeff_C, if_neg hb, zero_tmul, smul_zero]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_C.h₁
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
⊢ ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0 → φ 0 • 0 = 0
Tactic:
exact fun _ => by rw [smul_zero]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
s : S
x✝ : ((Polynomial.rTensor R N S) (C s ⊗ₜ[R] n)) 0 = 0
⊢ φ 0 • 0 = 0
Tactic:
rw [smul_zero]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ (((Polynomial.rTensor R N S) ((p + q) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((p + q) ⊗ₜ[R] n)
Tactic:
simp only [add_tmul, LinearEquiv.map_add]
Proof state after:
case tmul.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n) + (Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n + q ⊗ₜ[R] n)
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n) + (Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n + q ⊗ₜ[R] n)
Tactic:
rw [Finsupp.sum_add_index, hp, hq, LinearMap.map_add]
Proof state after:
case tmul.h_add.h_zero
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support, φ a • 0 = 0

case tmul.h_add.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support,
    ∀ (b₁ b₂ : S ⊗[R] N), φ a • (b₁ + b₂) = φ a • b₁ + φ a • b₂
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add.h_zero
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support, φ a • 0 = 0
Tactic:
intro x _
Proof state after:
case tmul.h_add.h_zero
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support
⊢ φ x • 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add.h_zero
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support
⊢ φ x • 0 = 0
Tactic:
apply smul_zero
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
⊢ ∀ a ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support,
    ∀ (b₁ b₂ : S ⊗[R] N), φ a • (b₁ + b₂) = φ a • b₁ + φ a • b₂
Tactic:
intro x _
Proof state after:
case tmul.h_add.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support
⊢ ∀ (b₁ b₂ : S ⊗[R] N), φ x • (b₁ + b₂) = φ x • b₁ + φ x • b₂
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_add.h_add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p q : S[X]
hp :
  (((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p ⊗ₜ[R] n)
hq :
  (((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (q ⊗ₜ[R] n)
x : ℕ
a✝ : x ∈ ((Polynomial.rTensor R N S) (p ⊗ₜ[R] n)).support ∪ ((Polynomial.rTensor R N S) (q ⊗ₜ[R] n)).support
⊢ ∀ (b₁ b₂ : S ⊗[R] N), φ x • (b₁ + b₂) = φ x • b₁ + φ x • b₂
Tactic:
apply smul_add
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ (((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)
Tactic:
rw [Finsupp.sum_eq_single (p + 1), rTensor_apply, rTensor_tmul]
Proof state after:
case tmul.h_monomial
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) • (↑R (lcoeff S (p + 1))) (C s * X ^ (p + 1)) ⊗ₜ[R] n =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)

case tmul.h_monomial.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b ≠ 0 →
      b ≠ p + 1 → φ b • ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b = 0

case tmul.h_monomial.h₁
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) (p + 1) = 0 → φ (p + 1) • 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) • (↑R (lcoeff S (p + 1))) (C s * X ^ (p + 1)) ⊗ₜ[R] n =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)
Tactic:
simp only [coe_restrictScalars, lcoeff_apply, coeff_C_mul, coeff_X_pow,
  ↓reduceIte, mul_one, rTensor_tmul, Polynomial.lsum_apply,
  lsmul_apply, smul_eq_mul]
Proof state after:
case tmul.h_monomial
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) • s ⊗ₜ[R] n = ((C s * X ^ (p + 1)).sum fun x x_1 => φ x * x_1) ⊗ₜ[R] n
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) • s ⊗ₜ[R] n = ((C s * X ^ (p + 1)).sum fun x x_1 => φ x * x_1) ⊗ₜ[R] n
Tactic:
rw [C_mul_X_pow_eq_monomial, sum_monomial_index, smul_tmul', smul_eq_mul]
Proof state after:
case tmul.h_monomial.hf
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) * 0 = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial.hf
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ φ (p + 1) * 0 = 0
Tactic:
rw [mul_zero]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ ∀ (b : ℕ),
    ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b ≠ 0 →
      b ≠ p + 1 → φ b • ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b = 0
Tactic:
intro b  _ hb
Proof state after:
case tmul.h_monomial.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝¹ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
b : ℕ
a✝ : ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ p + 1
⊢ φ b • ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b = 0
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial.h₀
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝¹ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
b : ℕ
a✝ : ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b ≠ 0
hb : b ≠ p + 1
⊢ φ b • ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) b = 0
Tactic:
simp only [rTensor_apply, rTensor_tmul, coe_restrictScalars, lcoeff_apply, coeff_C_mul,
  coeff_X_pow, mul_ite, mul_one, mul_zero, if_neg hb, zero_tmul, smul_zero]
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case tmul.h_monomial.h₁
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
n : N
p : ℕ
s : S
a✝ :
  (((Polynomial.rTensor R N S) ((C s * X ^ p) ⊗ₜ[R] n)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) ((C s * X ^ p) ⊗ₜ[R] n)
⊢ ((Polynomial.rTensor R N S) ((C s * X ^ (p + 1)) ⊗ₜ[R] n)) (p + 1) = 0 → φ (p + 1) • 0 = 0
Tactic:
exact fun _ ↦ smul_zero _
Proof state after:
no goals
Theorem: Polynomial.rTensor'_sum
Proof state before:
case add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ (((Polynomial.rTensor R N S) (p + q)).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p + q)
Tactic:
simp only [add_tmul, LinearEquiv.map_add]
Proof state after:
case add
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₚ[R] N
p✝ : ℕ
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
φ : ℕ → S
p q : S[X] ⊗[R] N
hp :
  (((Polynomial.rTensor R N S) p).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) p
hq :
  (((Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) q
⊢ (((Polynomial.rTensor R N S) p + (Polynomial.rTensor R N S) q).sum fun p sn => φ p • sn) =
    (LinearMap.rTensor N (Polynomial.lsum fun n => ↑R ((lsmul S S) (φ n)))) (p + q)