Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
⊢ ∑ d ∈ (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1).support,
      (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          (coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)) *
        ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    ∑ d ∈ p.support,
      (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ i ∈ d.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ d i
Tactic:
apply Finset.sum_congr
Proof state after:
case h.right.e_a.h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
⊢ (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1).support = p.support

case h.right.e_a.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
⊢ ∀ x ∈ p.support,
    (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          (coeff x (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)) *
        ∏ i ∈ x.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ x i =
      (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff x p) * ∏ i ∈ x.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ x i