internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
d : ℕ × M →₀ ℕ
⊢ ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0 ↔ coeff d p = 0
Tactic:
refine ⟨fun hd => ?_, fun hd hd' => absurd hd hd'⟩
Proof state after:
case h.right.e_a.h.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
d : ℕ × M →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
⊢ coeff d p = 0
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
d : ℕ × M →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
⊢ coeff d p = 0
Tactic:
by_contra h0
Proof state after:
case h.right.e_a.h.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
d : ℕ × M →₀ ℕ
hd : ¬coeff d p = 0 → (algebraMap R S) (coeff d p) = 0
h0 : ¬coeff d p = 0
⊢ False
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
case h.right.e_a.h.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
s : S
f : R →ₐ[R] S :=
  let __src := algebraMap R S;
  { toRingHom := __src, commutes' := ⋯ }
hf :
  f =
    let __src := algebraMap R S;
    { toRingHom := __src, commutes' := ⋯ }
p : MvPolynomial (ℕ × M) R
hpa : (RingQuot.mkAlgHom R (Rel R M)) p = a
p' : MvPolynomial (ℕ × M) S := (baseChange f) p
hp' : p' = (baseChange f) p
h_eq : (algebraMap S (MvPolynomial (ℕ × M) S)).comp (algebraMap R S) = algebraMap R (MvPolynomial (ℕ × M) S)
h_eq' :
  (algebraMap S (DividedPowerAlgebra S (S ⊗[R] M))).comp (algebraMap R S) =
    algebraMap R (DividedPowerAlgebra S (S ⊗[R] M))
hpn : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree Prod.fst) d = n
h_sum :
  ∀ (d : ℕ × M →₀ ℕ),
    (algebraMap R S) (coeff d p) = coeff d (∑ x ∈ p.support, C ((algebraMap R S) (coeff x p)) * (monomial x) 1)
d : ℕ × M →₀ ℕ
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))
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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']
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof 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]
Proof state after:
no goals
Theorem: Subalgebra.fg_sup
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hA : A.FG
hB : B.FG
⊢ (A ⊔ B).FG
Tactic:
classical
obtain ⟨s, hs⟩ := hA
obtain ⟨t, ht⟩ := hB
rw [← hs, ← ht, ← Algebra.adjoin_union, ← Finset.coe_union]
exact ⟨s ∪ t, rfl⟩
Proof state after:
no goals
Theorem: Subalgebra.fg_sup
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hA : A.FG
hB : B.FG
⊢ (A ⊔ B).FG
Tactic:
obtain ⟨s, hs⟩ := hA
Proof state after:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hB : B.FG
s : Finset S
hs : Algebra.adjoin R ↑s = A
⊢ (A ⊔ B).FG
Theorem: Subalgebra.fg_sup
Proof state before:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
hB : B.FG
s : Finset S
hs : Algebra.adjoin R ↑s = A
⊢ (A ⊔ B).FG
Tactic:
obtain ⟨t, ht⟩ := hB
Proof state after:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (A ⊔ B).FG
Theorem: Subalgebra.fg_sup
Proof state before:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (A ⊔ B).FG
Tactic:
rw [← hs, ← ht, ← Algebra.adjoin_union, ← Finset.coe_union]
Proof state after:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (Algebra.adjoin R ↑(s ∪ t)).FG
Theorem: Subalgebra.fg_sup
Proof state before:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = A
t : Finset S
ht : Algebra.adjoin R ↑t = B
⊢ (Algebra.adjoin R ↑(s ∪ t)).FG
Tactic:
exact ⟨s ∪ t, rfl⟩
Proof state after:
no goals
Theorem: AlgHom.factor
Proof state before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ φ = φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))
Tactic:
ext
Proof state after:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ φ x✝ = (φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))) x✝
Theorem: AlgHom.factor
Proof state before:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ φ x✝ = (φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: AlgHom.comp_rangeRestrict
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ φ.range.val.comp φ.rangeRestrict = φ
Tactic:
ext
Proof state after:
case H
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ (φ.range.val.comp φ.rangeRestrict) x✝ = φ x✝
Theorem: AlgHom.comp_rangeRestrict
Proof state before:
case H
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ (φ.range.val.comp φ.rangeRestrict) x✝ = φ x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: AlgHom.quotientKerEquivRange_mk
Proof state before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)) = φ.rangeRestrict
Tactic:
ext s
Proof state after:
case H.a
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ↑(((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))) s) = ↑(φ.rangeRestrict s)