internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
⊢ ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
Tactic:
intro d
Proof state after:
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
d : ℕ × M →₀ ℕ
⊢ (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
d : ℕ × M →₀ ℕ
⊢ (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
Tactic:
conv_lhs => rw [MvPolynomial.as_sum (p := p)]
Proof state after:
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
d : ℕ × M →₀ ℕ
⊢ (algebraMap R S) (coeff d (∑ v ∈ p.support, (monomial v) (coeff v p))) =
    coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
d : ℕ × M →₀ ℕ
⊢ (algebraMap R S) (coeff d (∑ v ∈ p.support, (monomial v) (coeff v p))) =
    coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
Tactic:
simp only [coeff_sum, coeff_C_mul, _root_.map_sum, coeff_monomial, mul_ite, mul_one, mul_zero]
Proof state after:
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
d : ℕ × M →₀ ℕ
⊢ ∑ x ∈ p.support, (algebraMap R S) (if x = d then coeff x p else 0) =
    ∑ x ∈ p.support, if x = d then (algebraMap R S) (coeff x p) else 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
d : ℕ × M →₀ ℕ
⊢ ∑ x ∈ p.support, (algebraMap R S) (if x = d then coeff x p else 0) =
    ∑ x ∈ p.support, if x = d then (algebraMap R S) (coeff x p) else 0
Tactic:
refine Finset.sum_congr rfl (fun x _hx => ?_)
Proof state after:
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
⊢ (algebraMap R S) (if x = d then coeff x p else 0) = if x = d then (algebraMap R S) (coeff x p) else 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
⊢ (algebraMap R S) (if x = d then coeff x p else 0) = if x = d then (algebraMap R S) (coeff x p) else 0
Tactic:
split_ifs
Proof state after:
case pos
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
h✝ : x = d
⊢ (algebraMap R S) (coeff x p) = (algebraMap R S) (coeff x p)

case neg
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
h✝ : ¬x = d
⊢ (algebraMap R S) 0 = 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case pos
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
h✝ : x = d
⊢ (algebraMap R S) (coeff x p) = (algebraMap R S) (coeff x p)
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case neg
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
d x : ℕ × M →₀ ℕ
_hx : x ∈ p.support
h✝ : ¬x = d
⊢ (algebraMap R S) 0 = 0
Tactic:
rw [map_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
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
Tactic:
ext d
Proof state after:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ d ∈ (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1).support ↔ d ∈ p.support
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ d ∈ (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1).support ↔ d ∈ p.support
Tactic:
simp only [mem_support_iff, ne_eq, not_iff_not]
Proof state after:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1) = 0 ↔ coeff d p = 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1) = 0 ↔ coeff d p = 0
Tactic:
conv_rhs => rw [MvPolynomial.as_sum (p := p)]
Proof state after:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1) = 0 ↔
    coeff d (∑ v ∈ p.support, (monomial v) (coeff v p)) = 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1) = 0 ↔
    coeff d (∑ v ∈ p.support, (monomial v) (coeff v p)) = 0
Tactic:
simp only [coeff_sum, coeff_C_mul, coeff_monomial, mul_ite, mul_one, mul_zero,
  Finset.sum_ite_eq', mem_support_iff, ne_eq, ite_not, ite_eq_left_iff,
  support_sum_monomial_coeff]
Proof state after:
case h.right.e_a.h.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 : ℕ × M →₀ ℕ
⊢ ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0 ↔ coeff d p = 0