Theorem: PolynomialMap.coeff_of_finsupp_polynomialMap (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b h) = h
Tactic:
simp only [coeff, coe_mk, AddHom.coe_mk, coe_comp, LinearEquiv.coe_coe, Function.comp_apply]
State after:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h)) = h

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h)) = h
Tactic:
ext d
State after:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
⊢ (scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h))) d = h d

State before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
⊢ (scalarRTensor ((generize ⇑b) (Finsupp.polynomialMap b h))) d = h d
Tactic:
rw [scalarRTensor_apply, eq_comm, ← LinearEquiv.symm_apply_eq, TensorProduct.lid_symm_apply,
  generize_finsupp_eq, map_finsupp_sum, Finsupp.sum_eq_single d
  (fun b _ hb => by rw [rTensor_tmul, lcoeff_apply, coeff_monomial, if_neg hb, zero_tmul])
  (fun _ => by rw [tmul_zero, map_zero]), rTensor_tmul, lcoeff_apply, coeff_monomial, if_pos rfl]
State after:
no goals

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝¹ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d b : ι →₀ ℕ
x✝ : h b ≠ 0
hb : b ≠ d
⊢ (LinearMap.rTensor N (lcoeff R d)) ((monomial b) 1 ⊗ₜ[R] h b) = 0
Tactic:
rw [rTensor_tmul, lcoeff_apply, coeff_monomial, if_neg hb, zero_tmul]
State after:
no goals

State before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
d : ι →₀ ℕ
x✝ : h d = 0
⊢ (LinearMap.rTensor N (lcoeff R d)) ((monomial d) 1 ⊗ₜ[R] 0) = 0
Tactic:
rw [tmul_zero, map_zero]
State after:
no goals