internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.zero
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
⊢ φ (if n = 0 then 1 else 0) = (dpScalarExtensionInv R S M) (if n = 0 then 1 else 0)
Tactic:
split_ifs
Proof state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : n = 0
⊢ φ 1 = (dpScalarExtensionInv R S M) 1

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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : ¬n = 0
⊢ φ 0 = (dpScalarExtensionInv R S M) 0
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case pos
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : n = 0
⊢ φ 1 = (dpScalarExtensionInv R S M) 1
Tactic:
simp only [_root_.map_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case neg
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
n : ℕ
h✝ : ¬n = 0
⊢ φ 0 = (dpScalarExtensionInv R S M) 0
Tactic:
simp only [_root_.map_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.tmul
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
s : S
m : M
n : ℕ
⊢ φ (dp S n (s ⊗ₜ[R] m)) = (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m))
Tactic:
rw [hφ, dpScalarExtensionInv_apply_dp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ φ (dp S n (x + y)) = (dpScalarExtensionInv R S M) (dp S n (x + y))
Tactic:
simp only [dp_add, map_sum, _root_.map_mul]
Proof state after:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n, φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    φ (dp S x_1.1 x) * φ (dp S x_1.2 y) =
      (dpScalarExtensionInv R S M) (dp S x_1.1 x) * (dpScalarExtensionInv R S M) (dp S x_1.2 y)
Tactic:
intro nn _hnn
Proof state after:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
nn : ℕ × ℕ
_hnn : nn ∈ Finset.antidiagonal n
⊢ φ (dp S nn.1 x) * φ (dp S nn.2 y) =
    (dpScalarExtensionInv R S M) (dp S nn.1 x) * (dpScalarExtensionInv R S M) (dp S nn.2 y)
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp.add
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
φ : DividedPowerAlgebra S (S ⊗[R] M) →ₐ[S] S ⊗[R] DividedPowerAlgebra R M
hφ : ∀ (n : ℕ) (s : S) (m : M), φ (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
f : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
x y : S ⊗[R] M
hx : ∀ (n : ℕ), φ (dp S n x) = (dpScalarExtensionInv R S M) (dp S n x)
hy : ∀ (n : ℕ), φ (dp S n y) = (dpScalarExtensionInv R S M) (dp S n y)
n : ℕ
nn : ℕ × ℕ
_hnn : nn ∈ Finset.antidiagonal n
⊢ φ (dp S nn.1 x) * φ (dp S nn.2 y) =
    (dpScalarExtensionInv R S M) (dp S nn.1 x) * (dpScalarExtensionInv R S M) (dp S nn.2 y)
Tactic:
rw [hx nn.1, hy nn.2]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coe_dpScalarExtensionEquiv
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
⊢ ⇑(dpScalarExtensionEquiv R S M) = ⇑(dpScalarExtension R S M)
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coe_dpScalarExtensionEquiv_symm
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
⊢ ⇑(dpScalarExtensionEquiv R S M).symm = ⇑(dpScalarExtensionInv R S M)
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
m : S ⊗[R] M
⊢ (LinearMap.rTensor (DividedPowerAlgebra R M) φ.toLinearMap) ((dpScalarExtensionEquiv R S M).symm (dp S n m)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) m))
Tactic:
rw [← coe_map_id₂]
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
m : S ⊗[R] M
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
      ((dpScalarExtensionEquiv R S M).symm (dp S n m)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) m))
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
m : S ⊗[R] M
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
      ((dpScalarExtensionEquiv R S M).symm (dp S n m)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) m))
Tactic:
induction m using TensorProduct.induction_on generalizing n with
| zero => simp only [Function.comp_apply, dp_null, RingHom.map_ite_one_zero, map_zero]
| tmul s m =>
  simp only [coe_dpScalarExtensionEquiv_symm, dpScalarExtensionInv_apply_dp, toLinearMap_apply,
    Algebra.TensorProduct.map_tmul, map_pow, coe_id, id_eq, LinearMap.rTensor_tmul ]
| add x y hx hy =>
  simp only [dp_add, _root_.map_sum, _root_.map_mul, map_add]
  apply Finset.sum_congr rfl
  rintro ⟨k, l⟩ _
  rw [hx, hy]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case zero
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
n : ℕ
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
      ((dpScalarExtensionEquiv R S M).symm (dp S n 0)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) 0))
Tactic:
simp only [Function.comp_apply, dp_null, RingHom.map_ite_one_zero, map_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case tmul
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
s : S
m : M
n : ℕ
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
      ((dpScalarExtensionEquiv R S M).symm (dp S n (s ⊗ₜ[R] m))) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) (s ⊗ₜ[R] m)))
Tactic:
simp only [coe_dpScalarExtensionEquiv_symm, dpScalarExtensionInv_apply_dp, toLinearMap_apply,
  Algebra.TensorProduct.map_tmul, map_pow, coe_id, id_eq, LinearMap.rTensor_tmul ]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case add
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n : ℕ
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
      ((dpScalarExtensionEquiv R S M).symm (dp S n (x + y))) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) (x + y)))
Tactic:
simp only [dp_add, _root_.map_sum, _root_.map_mul, map_add]
Proof state after:
case add
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n,
      (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.1 x)) *
        (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.2 y)) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
        (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.2 ((LinearMap.rTensor M φ.toLinearMap) y))
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case add
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n : ℕ
⊢ ∑ x_1 ∈ Finset.antidiagonal n,
      (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.1 x)) *
        (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.2 y)) =
    ∑ x_1 ∈ Finset.antidiagonal n,
      (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
        (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.2 ((LinearMap.rTensor M φ.toLinearMap) y))
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case add
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.1 x)) *
        (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.2 y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
        (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.2 ((LinearMap.rTensor M φ.toLinearMap) y))
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case add
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n : ℕ
⊢ ∀ x_1 ∈ Finset.antidiagonal n,
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.1 x)) *
        (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
          ((dpScalarExtensionEquiv R S M).symm (dp S x_1.2 y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
        (dpScalarExtensionEquiv R S' M).symm (dp S' x_1.2 ((LinearMap.rTensor M φ.toLinearMap) y))
Tactic:
rintro ⟨k, l⟩ _
Proof state after:
case add.mk
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n k l : ℕ
a✝ : (k, l) ∈ Finset.antidiagonal n
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S (k, l).1 x)) *
      (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S (k, l).2 y)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' (k, l).1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
      (dpScalarExtensionEquiv R S' M).symm (dp S' (k, l).2 ((LinearMap.rTensor M φ.toLinearMap) y))
Theorem: DividedPowerAlgebra.rTensor_comp_dpScalarExtensionEquiv_symm_eq
Proof state before:
case add.mk
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
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
S' : Type u_5
inst✝¹ : CommRing S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x y : S ⊗[R] M
hx :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n x)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) x))
hy :
  ∀ (n : ℕ),
    (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S n y)) =
      (dpScalarExtensionEquiv R S' M).symm (dp S' n ((LinearMap.rTensor M φ.toLinearMap) y))
n k l : ℕ
a✝ : (k, l) ∈ Finset.antidiagonal n
⊢ (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S (k, l).1 x)) *
      (Algebra.TensorProduct.map φ (AlgHom.id R (DividedPowerAlgebra R M)))
        ((dpScalarExtensionEquiv R S M).symm (dp S (k, l).2 y)) =
    (dpScalarExtensionEquiv R S' M).symm (dp S' (k, l).1 ((LinearMap.rTensor M φ.toLinearMap) x)) *
      (dpScalarExtensionEquiv R S' M).symm (dp S' (k, l).2 ((LinearMap.rTensor M φ.toLinearMap) y))
Tactic:
rw [hx, hy]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_mem_grade
Proof state before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hinj : Function.Injective ⇑(algebraMap R S)
a : DividedPowerAlgebra R M
n : ℕ
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]
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
⊢ ∃ p ∈ weightedHomogeneousSubmodule S Prod.fst n, mk p = (dpScalarExtension R S M) (s ⊗ₜ[R] a)