Theorem: PolynomialMap.ofLinearMap_coeff_single (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ((coeff m) (ofLinearMap u)) (Finsupp.single i 1) = u (m i)
Tactic:
rw [coeff, generize, coe_comp, LinearEquiv.coe_coe, coe_mk, AddHom.coe_mk, Function.comp_apply]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (scalarRTensor ((ofLinearMap u).toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i))) (Finsupp.single i 1) = u (m i)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (scalarRTensor ((ofLinearMap u).toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i))) (Finsupp.single i 1) = u (m i)
Tactic:
simp only [ofLinearMap_toFun, map_sum, LinearMap.baseChange_tmul]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (∑ x : ι, scalarRTensor (X x ⊗ₜ[R] u (m x))) (Finsupp.single i 1) = u (m i)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ (∑ x : ι, scalarRTensor (X x ⊗ₜ[R] u (m x))) (Finsupp.single i 1) = u (m i)
Tactic:
rw [Finsupp.coe_finset_sum, Finset.sum_apply, Finset.sum_eq_single i _ (fun hi => by
  simp only [mem_univ, not_true_eq_false] at hi), scalarRTensor_apply_tmul_apply,
    coeff_X, _root_.one_smul]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ∀ b ∈ univ, b ≠ i → (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
hi : i ∉ univ
⊢ (scalarRTensor (X i ⊗ₜ[R] u (m i))) (Finsupp.single i 1) = 0
Tactic:
simp only [mem_univ, not_true_eq_false] at hi
State after:
no goals

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i : ι
⊢ ∀ b ∈ univ, b ≠ i → (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
intro b _ hb
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
have hb' : ¬ Finsupp.single b 1 = Finsupp.single i 1 := by
  rwa [Finsupp.single_left_inj]; norm_num
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
hb' : ¬Finsupp.single b 1 = Finsupp.single i 1
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
hb' : ¬Finsupp.single b 1 = Finsupp.single i 1
⊢ (scalarRTensor (X b ⊗ₜ[R] u (m b))) (Finsupp.single i 1) = 0
Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_X', if_neg hb', _root_.zero_smul]
State after:
no goals

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ ¬Finsupp.single b 1 = Finsupp.single i 1
Tactic:
rwa [Finsupp.single_left_inj]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ 1 ≠ 0

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
u : M →ₗ[R] N
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : ι → M
i b : ι
a✝ : b ∈ univ
hb : b ≠ i
⊢ 1 ≠ 0
Tactic:
norm_num
State after:
no goals