internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
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
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 : ℕ
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)
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 : ℕ
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
Proof 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)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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'
Proof 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)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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'
Proof 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)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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 ⊢
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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'
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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'
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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')
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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']
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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'
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
⊢ (weightedDegree Prod.fst) (Finsupp.mapDomain (Prod.map id fun m => 1 ⊗ₜ[R] m) d) = (weightedDegree Prod.fst) d