Theorem: PolynomialMap.generize_eq (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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
dsimp only [coeff, 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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = (scalarRTensor ((generize m) f)).sum fun k n => (monomial k) 1 ⊗ₜ[R] n

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 ι
m : ι → M
f : M →ₚ[R] N
⊢ (generize m) f = (scalarRTensor ((generize m) f)).sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
generalize h : scalarRTensor (generize m f) = p
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor ((generize m) f) = p
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n

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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor ((generize m) f) = p
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [eq_comm, ← LinearEquiv.symm_apply_eq] at h
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n

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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ (generize m) f = p.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [← h, LinearEquiv.symm_apply_eq, map_finsupp_sum]
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ p = p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)

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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
⊢ p = p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)
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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = (p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)) 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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = (p.sum fun a b => scalarRTensor ((monomial a) 1 ⊗ₜ[R] b)) d
Tactic:
rw [Finsupp.sum_apply, Finsupp.sum_eq_single d, scalarRTensor_apply_tmul_apply,
  coeff_monomial, if_pos rfl, _root_.one_smul]
State after:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ ∀ (b : ι →₀ ℕ), p b ≠ 0 → b ≠ d → (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0

case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = 0 → (scalarRTensor ((monomial d) 1 ⊗ₜ[R] 0)) d = 0

State before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ ∀ (b : ι →₀ ℕ), p b ≠ 0 → b ≠ d → (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0
Tactic:
intro b _ hb
State after:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d b : ι →₀ ℕ
a✝ : p b ≠ 0
hb : b ≠ d
⊢ (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0

State before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d b : ι →₀ ℕ
a✝ : p b ≠ 0
hb : b ≠ d
⊢ (scalarRTensor ((monomial b) 1 ⊗ₜ[R] p b)) d = 0
Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_monomial, if_neg hb, _root_.zero_smul]
State after:
no goals

State before:
case h.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 ι
m : ι → M
f : M →ₚ[R] N
p : (ι →₀ ℕ) →₀ N
h : scalarRTensor.symm p = (generize m) f
d : ι →₀ ℕ
⊢ p d = 0 → (scalarRTensor ((monomial d) 1 ⊗ₜ[R] 0)) d = 0
Tactic:
simp only [tmul_zero, map_zero, Finsupp.coe_zero, Pi.zero_apply, implies_true]
State after:
no goals