internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.e'_2
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
hd0' : coeff d p ≠ 0
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = (weightedDegree Prod.fst) d
Tactic:
simp only [weightedDegree, LinearMap.toAddMonoidHom_coe, Finsupp.total_mapDomain]
Proof state after:
case h.e'_2
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
hd0' : coeff d p ≠ 0
⊢ (Finsupp.total (ℕ × M) ℕ ℕ (Prod.fst ∘ Prod.map id fun m => 1 ⊗ₜ[R] m)) d = (Finsupp.total (ℕ × M) ℕ ℕ Prod.fst) d
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.e'_2
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
hd0' : coeff d p ≠ 0
⊢ (Finsupp.total (ℕ × M) ℕ ℕ (Prod.fst ∘ Prod.map id fun m => 1 ⊗ₜ[R] m)) d = (Finsupp.total (ℕ × M) ℕ ℕ Prod.fst) d
Tactic:
rfl
Proof state after:
no goals
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
⊢ coeff d p ≠ 0
Tactic:
intro h
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
h : coeff d p = 0
⊢ False
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
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
d' : ℕ × S ⊗[R] M →₀ ℕ
hd' : s * coeff d' ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
d : ℕ × M →₀ ℕ
hdd' : Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d = d'
hd0 : (algebraMap R S) (coeff d p) ≠ 0
h : coeff d p = 0
⊢ False
Tactic:
simp only [h, map_zero, ne_eq, not_true_eq_false] at hd0
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
⊢ mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
have h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) =
  (algebraMap R (MvPolynomial (ℕ × M) S)) := rfl
Proof state after:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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)
⊢ mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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)
⊢ mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
have h_eq' : (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
  (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) := rfl
Proof state after:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
rw [LinearMapClass.map_smul, dpScalarExtension_tmul]
Proof state after:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ s • mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = s • (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ s • mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = s • (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
Tactic:
congr 1
Proof state after:
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
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
hpn : p ∈ ↑(weightedHomogeneousSubmodule R Prod.fst n)
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))
⊢ mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
Tactic:
simp only [SetLike.mem_coe, mem_weightedHomogeneousSubmodule, IsWeightedHomogeneous] at hpn
Proof state after:
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
⊢ mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
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
⊢ mk ((rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (1 ⊗ₜ[R] a)
Tactic:
simp only [hp', baseChange, hf, coe_ringHom_mk, coe_mk, coe_eval₂RingHom, ← hpa,
  MvPolynomial.rename, ← algebraMap_eq, h_eq, dpScalarExtension, AlgHom.baseChange,
  toRingHom_eq_coe, coe_mk, RingHom.coe_coe, productMap_apply_tmul,
  _root_.map_one, one_mul, lift', RingQuot.liftAlgHom_mkAlgHom_apply, coe_eval₂AlgHom,
  Function.comp_def, Prod_map, id_eq, baseChange, hf, coe_ringHom_mk, coe_mk,
  coe_eval₂RingHom]
Proof state after:
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
⊢ mk ((aeval fun x => X (x.1, 1 ⊗ₜ[R] x.2)) (eval₂ (algebraMap R (MvPolynomial (ℕ × M) S)) X p)) =
    eval₂ (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (fun nm => dp S nm.1 (1 ⊗ₜ[R] nm.2)) p
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
⊢ mk ((aeval fun x => X (x.1, 1 ⊗ₜ[R] x.2)) (eval₂ (algebraMap R (MvPolynomial (ℕ × M) S)) X p)) =
    eval₂ (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (fun nm => dp S nm.1 (1 ⊗ₜ[R] nm.2)) p
Tactic:
rw [← AlgHom.comp_apply, MvPolynomial.comp_aeval, aeval_def]
Proof state after:
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
⊢ eval₂ (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))) (fun i => mk (X (i.1, 1 ⊗ₜ[R] i.2)))
      (eval₂ (algebraMap R (MvPolynomial (ℕ × M) S)) X p) =
    eval₂ (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (fun nm => dp S nm.1 (1 ⊗ₜ[R] nm.2)) p
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
⊢ eval₂ (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))) (fun i => mk (X (i.1, 1 ⊗ₜ[R] i.2)))
      (eval₂ (algebraMap R (MvPolynomial (ℕ × M) S)) X p) =
    eval₂ (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (fun nm => dp S nm.1 (1 ⊗ₜ[R] nm.2)) p
Tactic:
simp only [eval₂_eq, MvPolynomial.algebraMap_apply, prod_X_pow_eq_monomial, RingHom.coe_comp,
  Function.comp_apply]
Proof state after:
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
⊢ ∑ 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