internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
case neg.hnc
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this✝ : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h✝ : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : Finsupp.equivMapDomain e p = Finsupp.equivMapDomain e k
⊢ p = k
Tactic:
simp only [DFunLike.ext_iff] at h'
Proof state after:
case neg.hnc
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this✝ : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h✝ : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
⊢ p = k
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
case neg.hnc
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this✝ : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h✝ : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
⊢ p = k
Tactic:
ext i
Proof state after:
case neg.hnc.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 ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this✝ : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h✝ : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
i : ι
⊢ p i = k i
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
case neg.hnc.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 ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this✝ : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h✝ : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
this : ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
h : ¬p = k
h' : ∀ (x : κ), (Finsupp.equivMapDomain e p) x = (Finsupp.equivMapDomain e k) x
i : ι
⊢ p i = k i
Tactic:
simpa only [Finsupp.equivMapDomain_apply, Equiv.symm_apply_apply] using h' (e i)
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
Proof state before:
case e_a.e_f.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 ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
this : f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
hf :
  (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap) (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
    (generize m) f
g : MvPolynomial ι R ⊗[R] N
h : f.toFun (MvPolynomial ι R) (∑ x : ι, X x ⊗ₜ[R] m (e x)) = g
p : ι →₀ ℕ
⊢ ∏ x : ι, X (e x) ^ p x = (monomial (Finsupp.equivMapDomain e p)) 1
Tactic:
simp only [monomial_eq, _root_.map_one, Finsupp.prod_pow, Finsupp.equivMapDomain_apply,
  _root_.one_mul, prod_congr_equiv e, map_univ_equiv, Function.comp_apply,
   Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = (generize m) f
Tactic:
rw [generize, coe_mk, AddHom.coe_mk]
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)
Theorem: PolynomialMap.coeff_comp_equiv
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 ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ f.toFun (MvPolynomial κ R) (∑ x : ι, X (e x) ⊗ₜ[R] m (e x)) = f.toFun (MvPolynomial κ R) (∑ i : κ, X i ⊗ₜ[R] m i)
Tactic:
apply congr_arg
Proof 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 ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ ∑ x : ι, X (e x) ⊗ₜ[R] m (e x) = ∑ i : κ, X i ⊗ₜ[R] m i
Theorem: PolynomialMap.coeff_comp_equiv
Proof 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 ι✝
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_2
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : ι →₀ ℕ
f : M →ₚ[R] N
hf : (LinearMap.rTensor N (aeval fun i => X (e i)).toLinearMap)
    (f.toFun (MvPolynomial ι R) (∑ i : ι, X i ⊗ₜ[R] m (e i))) =
  f.toFun (MvPolynomial κ R)
    ((LinearMap.rTensor M (aeval fun i => X (e i)).toLinearMap) (∑ i : ι, X i ⊗ₜ[R] m (e i))) :=
  isCompat_apply f (aeval fun i => X (e i)) (∑ i : ι, X i ⊗ₜ[R] m (e i))
⊢ ∑ x : ι, X (e x) ⊗ₜ[R] m (e x) = ∑ i : κ, X i ⊗ₜ[R] m i
Tactic:
simp only [sum_congr_equiv e, map_univ_equiv, Function.comp_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: PolynomialMap.coeff_comp_equiv'
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 κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff (m ∘ ⇑e)) f) (Finsupp.equivMapDomain e.symm k)
Tactic:
rw [coeff_comp_equiv]
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 κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff ((m ∘ ⇑e) ∘ ⇑e.symm)) f) k
Theorem: PolynomialMap.coeff_comp_equiv'
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 κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ ((coeff m) f) k = ((coeff ((m ∘ ⇑e) ∘ ⇑e.symm)) f) k
Tactic:
congr
Proof state after:
case e_a.e_a.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ m = (m ∘ ⇑e) ∘ ⇑e.symm
Theorem: PolynomialMap.coeff_comp_equiv'
Proof state before:
case e_a.e_a.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k : κ →₀ ℕ
f : M →ₚ[R] N
⊢ m = (m ∘ ⇑e) ∘ ⇑e.symm
Tactic:
ext k
Proof state after:
case e_a.e_a.e_m.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k✝ : κ →₀ ℕ
f : M →ₚ[R] N
k : κ
⊢ m k = ((m ∘ ⇑e) ∘ ⇑e.symm) k
Theorem: PolynomialMap.coeff_comp_equiv'
Proof state before:
case e_a.e_a.e_m.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 ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
e : ι ≃ κ
m : κ → M
k✝ : κ →₀ ℕ
f : M →ₚ[R] N
k : κ
⊢ m k = ((m ∘ ⇑e) ∘ ⇑e.symm) k
Tactic:
simp only [Function.comp_apply, Equiv.apply_symm_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 ι
m : ι → M
f : M →ₚ[R] N
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : ι → S
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
have this := congr_fun (f.isCompat (MvPolynomial.aeval r))
  (univ.sum fun i => MvPolynomial.X i ⊗ₜ[R] 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 ι
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 ∘ ⇑(LinearMap.rTensor M (aeval r).toLinearMap)) (∑ i : ι, X i ⊗ₜ[R] m i)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
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 ∘ ⇑(LinearMap.rTensor M (aeval r).toLinearMap)) (∑ i : ι, X i ⊗ₜ[R] m i)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
simp only [Function.comp_apply, map_sum, LinearMap.rTensor_tmul,
  AlgHom.toLinearMap_apply, MvPolynomial.aeval_X] at this
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)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
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)
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
let h := generize_eq m f
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 : (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n := generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
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 : (generize m) f = ((coeff m) f).sum fun k n => (monomial k) 1 ⊗ₜ[R] n := generize_eq m f
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
simp only [generize, coe_mk, AddHom.coe_mk] at h
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
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
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
⊢ f.toFun S (∑ i : ι, r i ⊗ₜ[R] m i) = ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
rw [← this, h, Finsupp.sum, _root_.map_sum]
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
⊢ ∑ x ∈ ((coeff m) f).support, (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
    ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
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
⊢ ∑ x ∈ ((coeff m) f).support, (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
    ((coeff m) f).sum fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n
Tactic:
apply sum_congr 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
⊢ ∀ x ∈ ((coeff m) f).support,
    (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
      (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) x (((coeff m) f) x)
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
⊢ ∀ x ∈ ((coeff m) f).support,
    (LinearMap.rTensor N (aeval r).toLinearMap) ((monomial x) 1 ⊗ₜ[R] ((coeff m) f) x) =
      (fun k n => (∏ i : ι, r i ^ k i) ⊗ₜ[R] n) x (((coeff m) f) x)
Tactic:
intro k _
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
⊢ (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)