Theorem: PolynomialMap.image_eq_coeff_finset_sum (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 ι✝
ι : 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
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

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
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

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'
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

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]
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

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]
State after:
no goals

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]
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

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]
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

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
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

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 _
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

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]
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

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
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

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]
State after:
no goals