Theorem: PolynomialMap.generize_finsupp_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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
set m := Finset.sum univ (fun i => (X i : MvPolynomial ι R) ⊗ₜ[R] b i) with hm
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (generize ⇑b) (Finsupp.polynomialMap b h) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
rw [generize, coe_mk, AddHom.coe_mk, Finsupp.polynomialMap_toFun_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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
⊢ (h.sum fun k n =>
      (∏ i : ι, (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (∑ i : ι, X i ⊗ₜ[R] b i) ^ k i) ⊗ₜ[R] n) =
    h.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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n =>
      (∏ i : ι, (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (∑ i : ι, X i ⊗ₜ[R] b i) ^ k i) ⊗ₜ[R] n) =
    h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
simp only [this]
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n => (∏ x : ι, X x ^ k x) ⊗ₜ[R] n) = h.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 ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h✝ : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
h : (ι →₀ ℕ) →₀ N
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ (h.sum fun k n => (∏ x : ι, X x ^ k x) ⊗ₜ[R] n) = h.sum fun k n => (monomial k) 1 ⊗ₜ[R] n
Tactic:
apply Finsupp.sum_congr
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ ∀ x ∈ h.support, (∏ x_1 : ι, X x_1 ^ x x_1) ⊗ₜ[R] h x = (monomial x) 1 ⊗ₜ[R] h x

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
⊢ ∀ x ∈ h.support, (∏ x_1 : ι, X x_1 ^ x x_1) ⊗ₜ[R] h x = (monomial x) 1 ⊗ₜ[R] h x
Tactic:
intro k _
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ x : ι, X x ^ k x) ⊗ₜ[R] h k = (monomial k) 1 ⊗ₜ[R] h k

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ x : ι, X x ^ k x) ⊗ₜ[R] h k = (monomial k) 1 ⊗ₜ[R] h k
Tactic:
congr
State after:
case h.e_m
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, X x ^ k x = (monomial k) 1

State before:
case h.e_m
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ x : ι, X x ^ k x = (monomial k) 1
Tactic:
rw [← MvPolynomial.prod_X_pow_eq_monomial, ← prod_mul_prod_compl k.support]
State after:
case h.e_m
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ i ∈ k.support, X i ^ k i) * ∏ i ∈ k.supportᶜ, X i ^ k i = ∏ x ∈ k.support, X x ^ k x

State before:
case h.e_m
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ (∏ i ∈ k.support, X i ^ k i) * ∏ i ∈ k.supportᶜ, X i ^ k i = ∏ x ∈ k.support, X x ^ k x
Tactic:
convert mul_one _
State after:
case h.e'_2.h.e'_6
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ i ∈ k.supportᶜ, X i ^ k i = 1

State before:
case h.e'_2.h.e'_6
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∏ i ∈ k.supportᶜ, X i ^ k i = 1
Tactic:
apply prod_eq_one
State after:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ k.supportᶜ, X x ^ k x = 1

State before:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
⊢ ∀ x ∈ k.supportᶜ, X x ^ k x = 1
Tactic:
intro i hi
State after:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : i ∈ k.supportᶜ
⊢ X i ^ k i = 1

State before:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : i ∈ k.supportᶜ
⊢ X i ^ k i = 1
Tactic:
rw [mem_compl, Finsupp.mem_support_iff, ne_eq, not_not] at hi
State after:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : k i = 0
⊢ X i ^ k i = 1

State before:
case h.e'_2.h.e'_6.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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
this : ∀ (i : ι), (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
k : ι →₀ ℕ
a✝ : k ∈ h.support
i : ι
hi : k i = 0
⊢ X i ^ k i = 1
Tactic:
rw [hi, pow_zero]
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) m = X i
Tactic:
rw [hm, map_sum, sum_eq_single i, LinearForm.baseChange_apply_tmul, Basis.coord_apply,
  Basis.repr_self, Finsupp.single_eq_same, _root_.one_smul, mul_one]
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ ∀ b_1 ∈ univ, b_1 ≠ i → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X b_1 ⊗ₜ[R] b b_1) = 0

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ i ∉ univ → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ ∀ b_1 ∈ univ, b_1 ≠ i → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X b_1 ⊗ₜ[R] b b_1) = 0
Tactic:
intro j _ hj
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X j ⊗ₜ[R] b j) = 0

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i j : ι
a✝ : j ∈ univ
hj : j ≠ i
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X j ⊗ₜ[R] b j) = 0
Tactic:
rw [LinearForm.baseChange_apply_tmul, Basis.coord_apply,
  Basis.repr_self, Algebra.mul_smul_comm, mul_one, Finsupp.single_smul,
  _root_.one_smul, Finsupp.single_eq_of_ne hj]
State after:
no goals

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
⊢ i ∉ univ → (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Tactic:
intro hi
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ (LinearForm.baseChange R (MvPolynomial ι R) M (b.coord i)) (X i ⊗ₜ[R] b i) = 0
Tactic:
exfalso
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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ False

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
m : MvPolynomial ι R ⊗[R] M := ∑ i : ι, X i ⊗ₜ[R] b i
hm : m = ∑ i : ι, X i ⊗ₜ[R] b i
i : ι
hi : i ∉ univ
⊢ False
Tactic:
exact hi (mem_univ _)
State after:
no goals