Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade (DividedPowers/DPAlgebra/BaseChange.lean)

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 : ℕ
ha : a ∈ grade R M n
s : S
⊢ (dpScalarExtension R S M) (s ⊗ₜ[R] a) ∈ grade S (S ⊗[R] M) n
Tactic:
rw [mem_grade_iff]
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 : ℕ
ha : a ∈ grade R M n
s : S
⊢ ∃ p ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)

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 : ℕ
ha : a ∈ grade R M n
s : S
⊢ ∃ p ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
set f : R →ₐ[R] S := { (algebraMap R S) with
  commutes' := fun r => rfl } with hf
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 : ℕ
ha : a ∈ grade 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 ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)

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 : ℕ
ha : a ∈ grade 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 ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
obtain ⟨p, hpn, hpa⟩ := ha
State after:
case intro.intro
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 ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)

State before:
case intro.intro
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 ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
set p' : MvPolynomial (ℕ × M) S := MvPolynomial.baseChange f p with hp'
State after:
case intro.intro
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
⊢ ∃ p ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)

State before:
case intro.intro
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
⊢ ∃ p ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
use s • rename (Prod.map id (fun m => 1 ⊗ₜ m)) p'
State after:
case 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
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
⊢ s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p' ∈ weightedHomogeneousSubmodule S Prod.fst n ∧
    mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)

State before:
case 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
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
⊢ s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p' ∈ weightedHomogeneousSubmodule S Prod.fst n ∧
    mk (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') = (dpScalarExtension R S M) (s ⊗ₜ[R] a)
Tactic:
constructor
State after:
case h.left
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
⊢ s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p' ∈ weightedHomogeneousSubmodule S Prod.fst n

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)

State before:
case h.left
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
⊢ s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p' ∈ weightedHomogeneousSubmodule S Prod.fst n
Tactic:
simp only [SetLike.mem_coe, mem_weightedHomogeneousSubmodule, IsWeightedHomogeneous] at hpn ⊢
State after:
case h.left
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 →₀ ℕ⦄,
    coeff d (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0 → (weightedDegree Prod.fst) d = n

State before:
case h.left
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 →₀ ℕ⦄,
    coeff d (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0 → (weightedDegree Prod.fst) d = n
Tactic:
intro d' hd'
State after:
case h.left
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' : coeff d' (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
⊢ (weightedDegree Prod.fst) d' = n

State before:
case h.left
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' : coeff d' (s • (rename (Prod.map id fun m => 1 ⊗ₜ[R] m)) p') ≠ 0
⊢ (weightedDegree Prod.fst) d' = n
Tactic:
simp only [coeff_smul, smul_eq_mul] at hd'
State after:
case h.left
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
⊢ (weightedDegree Prod.fst) d' = n

State before:
case h.left
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
⊢ (weightedDegree Prod.fst) d' = n
Tactic:
obtain ⟨d, hdd', hd0⟩ := coeff_rename_ne_zero _ _ _ (right_ne_zero_of_mul hd')
State after:
case h.left.intro.intro
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 : coeff d p' ≠ 0
⊢ (weightedDegree Prod.fst) d' = n

State before:
case h.left.intro.intro
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 : coeff d p' ≠ 0
⊢ (weightedDegree Prod.fst) d' = n
Tactic:
rw [← hdd']
State after:
case h.left.intro.intro
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 : coeff d p' ≠ 0
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = n

State before:
case h.left.intro.intro
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 : coeff d p' ≠ 0
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = n
Tactic:
simp only [hp', hf, coeff_baseChange_apply, coe_mk] at hd0
State after:
case h.left.intro.intro
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
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = n

State before:
case h.left.intro.intro
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
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = n
Tactic:
have hd0' : coeff d p ≠ 0 := by
  intro h
  simp only [h, map_zero, ne_eq, not_true_eq_false] at hd0
State after:
case h.left.intro.intro
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) = n

State before:
case h.left.intro.intro
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) = n
Tactic:
convert hpn hd0'
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
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = (weightedDegree Prod.fst) d

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 => ?_)
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

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

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

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

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

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

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

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

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 p = 0 → (algebraMap R S) (coeff d p) = 0 ↔ coeff d p = 0
Tactic:
refine ⟨fun hd => ?_, fun hd hd' => absurd hd hd'⟩
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 →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
⊢ coeff d p = 0

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 →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
⊢ coeff d p = 0
Tactic:
by_contra h0
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 →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
h0 : ¬coeff d p = 0
⊢ False

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 →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
h0 : ¬coeff d p = 0
⊢ False
Tactic:
exact h0 (hinj (map_zero (f := algebraMap R S) ▸ hd h0))
State after:
no goals

State before:
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
Tactic:
intro d _hd
State after:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.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 =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ i ∈ d.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ d i

State before:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.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 =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ i ∈ d.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ d i
Tactic:
rw [← algebraMap_eq, coeff_sum]
State after:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
        (∑ x ∈ p.support,
          coeff d ((algebraMap S (MvPolynomial (ℕ × M) S)) ((algebraMap R S) (coeff x p)) * (monomial x) 1)) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ i ∈ d.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ d i

State before:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
        (∑ x ∈ p.support,
          coeff d ((algebraMap S (MvPolynomial (ℕ × M) S)) ((algebraMap R S) (coeff x p)) * (monomial x) 1)) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ i ∈ d.support, dp S i.1 (1 ⊗ₜ[R] i.2) ^ d i
Tactic:
simp only [MvPolynomial.algebraMap_apply, coeff_C_mul, map_sum, dp_def']
State after:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          ((algebraMap S S) ((algebraMap R S) (coeff x p)) * coeff d ((monomial x) 1))) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ x ∈ d.support, mk (X (x.1, 1 ⊗ₜ[R] x.2)) ^ d x

State before:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          ((algebraMap S S) ((algebraMap R S) (coeff x p)) * coeff d ((monomial x) 1))) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))) (coeff d p) * ∏ x ∈ d.support, mk (X (x.1, 1 ⊗ₜ[R] x.2)) ^ d x
Tactic:
rw [← h_eq', RingHom.coe_comp, Function.comp_apply, h_sum d, coeff_sum, map_sum]
State after:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          ((algebraMap S S) ((algebraMap R S) (coeff x p)) * coeff d ((monomial x) 1))) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          (coeff d (C ((algebraMap R S) (coeff x p)) * (monomial x) 1))) *
      ∏ x ∈ d.support, mk (X (x.1, 1 ⊗ₜ[R] x.2)) ^ d x

State before:
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)
d : ℕ × M →₀ ℕ
_hd : d ∈ p.support
⊢ (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          ((algebraMap S S) ((algebraMap R S) (coeff x p)) * coeff d ((monomial x) 1))) *
      ∏ i ∈ d.support, mk (X (i.1, 1 ⊗ₜ[R] i.2)) ^ d i =
    (∑ x ∈ p.support,
        (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M)))
          (coeff d (C ((algebraMap R S) (coeff x p)) * (monomial x) 1))) *
      ∏ x ∈ d.support, mk (X (x.1, 1 ⊗ₜ[R] x.2)) ^ d x
Tactic:
simp only [Algebra.id.map_eq_id, RingHomCompTriple.comp_apply, _root_.map_mul, coeff_C_mul]
State after:
no goals