internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.image_eq_coeff_sum
Proof 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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial k) 1 ⊗ₜ[R] ((coeff m) f) k) =
    (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) k (((coeff m) f) k)
Tactic:
simp only [LinearMap.rTensor_tmul, AlgHom.toLinearMap_apply]
Proof 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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) ⊗ₜ[R] ((coeff m) f) k = (∏ i : ι, r i ^ k i) ⊗ₜ[R] ((coeff m) f) k
Theorem: PolynomialMap.image_eq_coeff_sum
Proof 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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) ⊗ₜ[R] ((coeff m) f) k = (∏ i : ι, r i ^ k i) ⊗ₜ[R] ((coeff m) f) k
Tactic:
apply congr_arg₂ _ _ rfl
Proof 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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) = ∏ i : ι, r i ^ k i
Theorem: PolynomialMap.image_eq_coeff_sum
Proof 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
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
this :
  (LinearMap.rTensor N (aeval r).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i)) =
    f.toFun S (∑ x : ι, r x ⊗ₜ[R] m x)
h : f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n :=
  generize_eq m f
k : ι →₀ ℕ
a✝ : k ∈ ((coeff m) f).support
⊢ (aeval r) ((monomial k) 1) = ∏ i : ι, r i ^ k i
Tactic:
simp only [aeval_monomial, _root_.map_one, Finsupp.prod_pow, one_mul]
Proof state after:
no goals
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
⊢ f.toFun S (∑ i ∈ s, r i ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Tactic:
let m' : s → M := fun i => m i
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
⊢ f.toFun S (∑ i ∈ s, r i ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
⊢ f.toFun S (∑ i ∈ s, r i ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Tactic:
let r' : s → S := fun i => r i
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ f.toFun S (∑ i ∈ s, r i ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ f.toFun S (∑ i ∈ s, r i ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Tactic:
convert image_eq_coeff_sum m' f S r'
Proof state after:
case h.e'_2.h.e'_13
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ ∑ i ∈ s, r i ⊗ₜ[R] m i = ∑ i : { x // x ∈ s }, r' i ⊗ₜ[R] m' i

case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) i = ∏ i : { x // x ∈ s }, r' i ^ x✝¹ i
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_2.h.e'_13
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ ∑ i ∈ s, r i ⊗ₜ[R] m i = ∑ i : { x // x ∈ s }, r' i ⊗ₜ[R] m' i
Tactic:
simp only [univ_eq_attach, Finsupp.coe_mk]
Proof state after:
case h.e'_2.h.e'_13
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ ∑ i ∈ s, r i ⊗ₜ[R] m i = ∑ i ∈ s.attach, r' i ⊗ₜ[R] m' i
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_2.h.e'_13
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
⊢ ∑ i ∈ s, r i ⊗ₜ[R] m i = ∑ i ∈ s.attach, r' i ⊗ₜ[R] m' i
Tactic:
rw [← sum_attach]
Proof state after:
no goals
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) i = ∏ i : { x // x ∈ s }, r' i ^ x✝¹ i
Tactic:
simp only [univ_eq_attach, Finsupp.coe_mk]
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) i = ∏ i ∈ s.attach, r' i ^ x✝¹ i
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ i ∈ s, r i ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) i = ∏ i ∈ s.attach, r' i ^ x✝¹ i
Tactic:
rw [← prod_attach]
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ x ∈ s.attach, r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = ∏ i ∈ s.attach, r' i ^ x✝¹ i
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∏ x ∈ s.attach, r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = ∏ i ∈ s.attach, r' i ^ x✝¹ i
Tactic:
apply prod_congr rfl
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∀ x ∈ s.attach, r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = r' x ^ x✝¹ x
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
⊢ ∀ x ∈ s.attach, r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = r' x ^ x✝¹ x
Tactic:
intro x _
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = r' x ^ x✝¹ x
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) (const ι 0) ↑x = r' x ^ x✝¹ x
Tactic:
simp only [const_zero, exists_apply_eq_apply, not_true]
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) 0 ↑x = r' x ^ x✝¹ x
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ r ↑x ^ extend (fun x => ↑x) (⇑x✝¹) 0 ↑x = r' x ^ x✝¹ x
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ extend (fun x => ↑x) (⇑x✝¹) 0 ↑x = x✝¹ x
Theorem: PolynomialMap.image_eq_coeff_finset_sum
Proof state before:
case h.e'_3.h.e'_7.h.h.h.e'_9
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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
s : Finset ι
m' : { x // x ∈ s } → M := fun i => m ↑i
r' : { x // x ∈ s } → S := fun i => r ↑i
x✝¹ : { x // x ∈ s } →₀ ℕ
x✝ : N
x : { x // x ∈ s }
a✝ : x ∈ s.attach
⊢ extend (fun x => ↑x) (⇑x✝¹) 0 ↑x = x✝¹ x
Tactic:
rw [Subtype.coe_injective.extend_apply]
Proof state after:
no goals
Theorem: PolynomialMap.image_eq_coeff_sum'
Proof 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 ι✝
ι : Type u_1
inst✝² : DecidableEq ι
m : ι → M
f : M →ₚ[R] N
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι →₀ S
⊢ f.toFun S (r.sum fun i a => a ⊗ₜ[R] m i) =
    ((coeff fun i => m ↑i) f).sum fun k n => (∏ i ∈ r.support, r i ^ extend (fun x => ↑x) (⇑k) (const ι 0) i) ⊗ₜ[R] n
Tactic:
rw [Finsupp.sum, image_eq_coeff_finset_sum]
Proof state after:
no goals
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof 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
r : ι → R
⊢ f.ground (∑ i : ι, r i • m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n
Tactic:
apply (TensorProduct.lid R N).symm.injective
Proof state after:
case a
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
r : ι → R
⊢ (TensorProduct.lid R N).symm (f.ground (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof state before:
case a
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
r : ι → R
⊢ (TensorProduct.lid R N).symm (f.ground (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Tactic:
rw [TensorProduct.lid_symm_apply, isCompat_apply_ground, ← TensorProduct.lid_symm_apply]
Proof state after:
case a
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
r : ι → R
⊢ f.toFun R ((TensorProduct.lid R M).symm (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof state before:
case a
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
r : ι → R
⊢ f.toFun R ((TensorProduct.lid R M).symm (∑ i : ι, r i • m i)) =
    (TensorProduct.lid R N).symm (((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n)
Tactic:
simp only [map_sum, TensorProduct.lid_symm_apply, ← TensorProduct.smul_tmul, smul_eq_mul, mul_one]
Proof state after:
case a
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
r : ι → R
⊢ f.toFun R (∑ x : ι, r x ⊗ₜ[R] m x) = 1 ⊗ₜ[R] ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof state before:
case a
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
r : ι → R
⊢ f.toFun R (∑ x : ι, r x ⊗ₜ[R] m x) = 1 ⊗ₜ[R] ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) • n
Tactic:
rw [image_eq_coeff_sum, ← TensorProduct.lid_symm_apply, map_finsupp_sum]
Proof state after:
case a
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
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => (TensorProduct.lid R N).symm ((∏ i : ι, r i ^ a i) • b)
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof state before:
case a
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
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => (TensorProduct.lid R N).symm ((∏ i : ι, r i ^ a i) • b)
Tactic:
simp only [map_finsupp_sum, TensorProduct.lid_symm_apply]
Proof state after:
case a
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
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => 1 ⊗ₜ[R] ((∏ i : ι, r i ^ a i) • b)
Theorem: PolynomialMap.ground_image_eq_coeff_sum
Proof state before:
case a
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
r : ι → R
⊢ (((coeff fun x => m x) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) =
    ((coeff m) f).sum fun a b => 1 ⊗ₜ[R] ((∏ i : ι, r i ^ a i) • b)
Tactic:
exact Finsupp.sum_congr (fun d _ => by rw [← TensorProduct.smul_tmul, smul_eq_mul, mul_one])
Proof state after:
no goals