Theorem: PolynomialMap.ground_image_eq_coeff_sum_one (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 ι
m : M
f : M →ₚ[R] N
r : R
⊢ f.ground (r • m) = ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
suffices r • m = univ.sum fun i ↦ (const Unit r) i • (const Unit m i) by
  rw [this, ground_image_eq_coeff_sum]
  exact sum_congr rfl (fun i _ => by simp only [univ_unique, const_apply, prod_singleton]; rfl)
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
r : R
⊢ r • m = ∑ i : Unit, const Unit r i • const Unit m i

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
⊢ r • m = ∑ i : Unit, const Unit r i • const Unit m i
Tactic:
simp only [univ_unique, const_apply, sum_const, card_singleton, _root_.one_smul]
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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ f.ground (r • m) = ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
rw [this, ground_image_eq_coeff_sum]
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
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ (((coeff fun i => const Unit m i) f).sum fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) =
    ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • 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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
⊢ (((coeff fun i => const Unit m i) f).sum fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) =
    ((coeff (const Unit m)) f).sum fun k n => r ^ k 0 • n
Tactic:
exact sum_congr rfl (fun i _ => by simp only [univ_unique, const_apply, prod_singleton]; rfl)
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 ι
m : M
f : M →ₚ[R] N
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ (fun k n => (∏ i : Unit, const Unit r i ^ k i) • n) i (((coeff fun i => const Unit m i) f) i) =
    (fun k n => r ^ k 0 • n) i (((coeff (const Unit m)) f) i)
Tactic:
simp only [univ_unique, const_apply, prod_singleton]
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
r : R
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ r ^ i default • ((coeff fun i => m) f) i = r ^ i 0 • ((coeff (const Unit m)) f) i

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
this : r • m = ∑ i : Unit, const Unit r i • const Unit m i
i : Unit →₀ ℕ
x✝ : i ∈ ((coeff (const Unit m)) f).support
⊢ r ^ i default • ((coeff fun i => m) f) i = r ^ i 0 • ((coeff (const Unit m)) f) i
Tactic:
rfl
State after:
no goals