Theorem: Polynomial.scalarRTensor_apply_tmul (DividedPowers/ForMathlib/RingTheory/TensorProduct/Polynomial.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
⊢ (scalarRTensor R N) (p ⊗ₜ[R] n) = p.sum fun i r => Finsupp.single i (r • n)
Tactic:
ext i
State after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = (p.sum fun i r => Finsupp.single i (r • n)) i

State before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ((scalarRTensor R N) (p ⊗ₜ[R] n)) i = (p.sum fun i r => Finsupp.single i (r • n)) i
Tactic:
rw [scalarRTensor_apply_tmul_apply]
State after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (p.sum fun i r => Finsupp.single i (r • n)) i

State before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (p.sum fun i r => Finsupp.single i (r • n)) i
Tactic:
rw [sum_def]
State after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (∑ n_1 ∈ p.support, Finsupp.single n_1 (p.coeff n_1 • n)) i

State before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (∑ n_1 ∈ p.support, Finsupp.single n_1 (p.coeff n_1 • n)) i
Tactic:
rw [Finset.sum_apply']
State after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = ∑ k ∈ p.support, (Finsupp.single k (p.coeff k • n)) i

State before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = ∑ k ∈ p.support, (Finsupp.single k (p.coeff k • n)) i
Tactic:
rw [Finset.sum_eq_single i]
State after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (Finsupp.single i (p.coeff i • n)) i

case h.h₀
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ∀ b ∈ p.support, b ≠ i → (Finsupp.single b (p.coeff b • n)) i = 0

case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ i ∉ p.support → (Finsupp.single i (p.coeff i • n)) i = 0

State before:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ p.coeff i • n = (Finsupp.single i (p.coeff i • n)) i
Tactic:
simp only [Finsupp.single_eq_same]
State after:
no goals

State before:
case h.h₀
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ ∀ b ∈ p.support, b ≠ i → (Finsupp.single b (p.coeff b • n)) i = 0
Tactic:
exact fun _ _ => Finsupp.single_eq_of_ne
State after:
no goals

State before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
⊢ i ∉ p.support → (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
intro h
State after:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : i ∉ p.support
⊢ (Finsupp.single i (p.coeff i • n)) i = 0

State before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : i ∉ p.support
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
simp only [mem_support_iff, ne_eq, not_not] at h
State after:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : p.coeff i = 0
⊢ (Finsupp.single i (p.coeff i • n)) i = 0

State before:
case h.h₁
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : R[X]
n : N
i : ℕ
h : p.coeff i = 0
⊢ (Finsupp.single i (p.coeff i • n)) i = 0
Tactic:
rw [h, zero_smul, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]
State after:
no goals