internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
⊢ ∀ x ∈ Finset.antidiagonal m,
    coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
intro x _
Proof state after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ coeff x.1 (eval₂ (C.comp ↑φ) X p) * coeff x.2 (X s) = φ (coeff x.1 p) * φ (coeff x.2 (X s))
Tactic:
simp only [h x.1, coeff_X']
Proof state after:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ (φ (coeff x.1 p) * if Finsupp.single s 1 = x.2 then 1 else 0) =
    φ (coeff x.1 p) * φ (if Finsupp.single s 1 = x.2 then 1 else 0)
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case h_X
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
⊢ (φ (coeff x.1 p) * if Finsupp.single s 1 = x.2 then 1 else 0) =
    φ (coeff x.1 p) * φ (if Finsupp.single s 1 = x.2 then 1 else 0)
Tactic:
split_ifs
Proof state after:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 1 = φ (coeff x.1 p) * φ 1

case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : ¬Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 0 = φ (coeff x.1 p) * φ 0
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case pos
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 1 = φ (coeff x.1 p) * φ 1
Tactic:
rw [_root_.map_one]
Proof state after:
no goals
Theorem: MvPolynomial.coeff_baseChange_apply
Proof state before:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
p : MvPolynomial σ S
s : σ
h : ∀ (m : σ →₀ ℕ), coeff m (eval₂ (C.comp ↑φ) X p) = φ (coeff m p)
m : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
a✝ : x ∈ Finset.antidiagonal m
h✝ : ¬Finsupp.single s 1 = x.2
⊢ φ (coeff x.1 p) * 0 = φ (coeff x.1 p) * φ 0
Tactic:
rw [_root_.map_zero]
Proof state after:
no goals
Theorem: MvPolynomial.lcoeff_comp_baseChange_eq
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
⊢ φ.toLinearMap ∘ₗ ↑R (lcoeff S m) = ↑R (lcoeff S' m) ∘ₗ (baseChange φ).toLinearMap
Tactic:
ext f
Proof state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
f : MvPolynomial σ S
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S m)) f = (↑R (lcoeff S' m) ∘ₗ (baseChange φ).toLinearMap) f
Theorem: MvPolynomial.lcoeff_comp_baseChange_eq
Proof state before:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
f : MvPolynomial σ S
⊢ (φ.toLinearMap ∘ₗ ↑R (lcoeff S m)) f = (↑R (lcoeff S' m) ∘ₗ (baseChange φ).toLinearMap) f
Tactic:
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, lcoeff_apply,
  AlgHom.toLinearMap_apply, coeff_baseChange_apply]
Proof state after:
no goals
Theorem: MvPolynomial.baseChange_monomial
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (baseChange φ) ((monomial m) a) = (monomial m) (φ a)
Tactic:
simp only [baseChange, coe_mk, coe_eval₂RingHom, eval₂_monomial, RingHom.coe_comp,
  RingHom.coe_coe, Function.comp_apply]
Proof state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (C (φ a) * m.prod fun n e => X n ^ e) = (monomial m) (φ a)
Theorem: MvPolynomial.baseChange_monomial
Proof state before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u_2
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
σ : Type u_3
φ : S →ₐ[R] S'
m : σ →₀ ℕ
a : S
⊢ (C (φ a) * m.prod fun n e => X n ^ e) = (monomial m) (φ a)
Tactic:
rw [monomial_eq]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.AlgHom.baseChange_tmul
Proof state before:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
φ : B →ₐ[R] C
a : A
b : B
⊢ (baseChange φ) (a ⊗ₜ[R] b) = a • φ b
Tactic:
simp only [baseChange, toRingHom_eq_coe, coe_mk, RingHom.coe_coe, productMap_apply_tmul,
  IsScalarTower.coe_toAlgHom', ← smul_eq_mul, algebraMap_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_apply_dp
Proof state before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
r : R
n : ℕ
m : M
⊢ (dpScalarExtension A R M) ((r ^ n) ⊗ₜ[A] dp A n m) = dp R n (r ⊗ₜ[A] m)
Tactic:
rw [dpScalarExtension, AlgHom.baseChange_tmul, lift'AlgHom_apply_dp, ← dp_smul, smul_tmul',
  smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_apply_one_dp
Proof state before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
n : ℕ
m : M
⊢ (dpScalarExtension A R M) (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
Tactic:
rw [← one_pow n, dpScalarExtension_apply_dp, one_pow]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_tmul
Proof state before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
r : R
m : DividedPowerAlgebra A M
⊢ (dpScalarExtension A R M) (r ⊗ₜ[A] m) = r • (dpScalarExtension A R M) (1 ⊗ₜ[A] m)
Tactic:
simp only [dpScalarExtension, AlgHom.baseChange_tmul, one_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
⊢ φ = dpScalarExtension A R M
Tactic:
apply AlgHom.ext
Proof state after:
case H
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
⊢ ∀ (x : R ⊗[A] DividedPowerAlgebra A M), φ x = (dpScalarExtension A R M) x
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
⊢ ∀ (x : R ⊗[A] DividedPowerAlgebra A M), φ x = (dpScalarExtension A R M) x
Tactic:
intro x
Proof state after:
case H
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
x : R ⊗[A] DividedPowerAlgebra A M
⊢ φ x = (dpScalarExtension A R M) x
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
x : R ⊗[A] DividedPowerAlgebra A M
⊢ φ x = (dpScalarExtension A R M) x
Tactic:
induction x using TensorProduct.induction_on with
| zero => simp only [map_zero]
| tmul s x =>
  induction x using DividedPowerAlgebra.induction_on with
  | h_C a =>
    rw [mk_C, Algebra.algebraMap_eq_smul_one, tmul_smul, smul_tmul', ← mul_one s, ← smul_eq_mul,
      ← smul_assoc, ← smul_tmul', map_smul,map_smul, ← Algebra.TensorProduct.one_def,
      _root_.map_one, _root_.map_one]
  | h_add f g hf hg => simp only [tmul_add, map_add, hf, hg]
  | h_dp f n m hf =>
      rw [← mul_one s, ← tmul_mul_tmul, _root_.map_mul, _root_.map_mul, hf, hφ n m,
        dpScalarExtension_apply_one_dp]
| add x y hx hy => simp only [map_add, hx, hy]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.zero
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
⊢ φ 0 = (dpScalarExtension A R M) 0
Tactic:
simp only [map_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.tmul
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
s : R
x : DividedPowerAlgebra A M
⊢ φ (s ⊗ₜ[A] x) = (dpScalarExtension A R M) (s ⊗ₜ[A] x)
Tactic:
induction x using DividedPowerAlgebra.induction_on with
| h_C a =>
  rw [mk_C, Algebra.algebraMap_eq_smul_one, tmul_smul, smul_tmul', ← mul_one s, ← smul_eq_mul,
    ← smul_assoc, ← smul_tmul', map_smul,map_smul, ← Algebra.TensorProduct.one_def,
    _root_.map_one, _root_.map_one]
| h_add f g hf hg => simp only [tmul_add, map_add, hf, hg]
| h_dp f n m hf =>
    rw [← mul_one s, ← tmul_mul_tmul, _root_.map_mul, _root_.map_mul, hf, hφ n m,
      dpScalarExtension_apply_one_dp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.tmul.h_C
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
s : R
a : A
⊢ φ (s ⊗ₜ[A] mk (MvPolynomial.C a)) = (dpScalarExtension A R M) (s ⊗ₜ[A] mk (MvPolynomial.C a))
Tactic:
rw [mk_C, Algebra.algebraMap_eq_smul_one, tmul_smul, smul_tmul', ← mul_one s, ← smul_eq_mul,
  ← smul_assoc, ← smul_tmul', map_smul,map_smul, ← Algebra.TensorProduct.one_def,
  _root_.map_one, _root_.map_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.tmul.h_add
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
s : R
f g : DividedPowerAlgebra A M
hf : φ (s ⊗ₜ[A] f) = (dpScalarExtension A R M) (s ⊗ₜ[A] f)
hg : φ (s ⊗ₜ[A] g) = (dpScalarExtension A R M) (s ⊗ₜ[A] g)
⊢ φ (s ⊗ₜ[A] (f + g)) = (dpScalarExtension A R M) (s ⊗ₜ[A] (f + g))
Tactic:
simp only [tmul_add, map_add, hf, hg]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.tmul.h_dp
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
s : R
f : DividedPowerAlgebra A M
n : ℕ
m : M
hf : φ (s ⊗ₜ[A] f) = (dpScalarExtension A R M) (s ⊗ₜ[A] f)
⊢ φ (s ⊗ₜ[A] (f * dp A n m)) = (dpScalarExtension A R M) (s ⊗ₜ[A] (f * dp A n m))
Tactic:
rw [← mul_one s, ← tmul_mul_tmul, _root_.map_mul, _root_.map_mul, hf, hφ n m,
  dpScalarExtension_apply_one_dp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtension_unique
Proof state before:
case H.add
A : Type u_1
inst✝⁴ : CommSemiring A
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : Algebra A R
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
φ : R ⊗[A] DividedPowerAlgebra A M →ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
hφ : ∀ (n : ℕ) (m : M), φ (1 ⊗ₜ[A] dp A n m) = dp R n (1 ⊗ₜ[A] m)
x y : R ⊗[A] DividedPowerAlgebra A M
hx : φ x = (dpScalarExtension A R M) x
hy : φ y = (dpScalarExtension A R M) y
⊢ φ (x + y) = (dpScalarExtension A R M) (x + y)
Tactic:
simp only [map_add, hx, hy]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_apply_dp
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
n : ℕ
s : S
m : M
⊢ (dpScalarExtensionInv R S M) (dp S n (s ⊗ₜ[R] m)) = (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
rw [dpScalarExtensionInv, dividedPowerAlgebra_exponentialModule_equiv_symm_apply]
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
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n) ↑((dpScalarExtensionExp R S M) (s ⊗ₜ[R] m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_apply_dp
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
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n) ↑((dpScalarExtensionExp R S M) (s ⊗ₜ[R] m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
simp only [dpScalarExtensionExp, LinearMap.baseChangeEquiv, LinearEquiv.coe_symm_mk,
  AlgebraTensorModule.lift_apply, lift.tmul, LinearMap.coe_restrictScalars, LinearMap.flip_apply,
  LinearMap.lsmul_apply, LinearMap.smul_apply, LinearMap.coe_comp, Function.comp_apply]
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
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n)
      ↑(s • (ExponentialModule.linearMap Algebra.TensorProduct.includeRight) ((exp_LinearMap R M) m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_apply_dp
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
n : ℕ
s : S
m : M
⊢ (PowerSeries.coeff (S ⊗[R] DividedPowerAlgebra R M) n)
      ↑(s • (ExponentialModule.linearMap Algebra.TensorProduct.includeRight) ((exp_LinearMap R M) m)) =
    (s ^ n) ⊗ₜ[R] dp R n m
Tactic:
rw [ExponentialModule.coe_smul, PowerSeries.coeff_scale, ExponentialModule.coeff_linearMap,
  Algebra.TensorProduct.includeRight, coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,
  OneHom.coe_mk, coeff_exp_LinearMap, smul_tmul', smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
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
φ : 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
⊢ φ = dpScalarExtensionInv R S M
Tactic:
apply AlgHom.ext
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
φ : 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
⊢ ∀ (x : DividedPowerAlgebra S (S ⊗[R] M)), φ x = (dpScalarExtensionInv R S M) x
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
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
φ : 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
⊢ ∀ (x : DividedPowerAlgebra S (S ⊗[R] M)), φ x = (dpScalarExtensionInv R S M) x
Tactic:
intro x
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
φ : 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
x : DividedPowerAlgebra S (S ⊗[R] M)
⊢ φ x = (dpScalarExtensionInv R S M) x
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_C
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
a : S
⊢ φ (mk (MvPolynomial.C a)) = (dpScalarExtensionInv R S M) (mk (MvPolynomial.C a))
Tactic:
rw [mk_C, Algebra.algebraMap_eq_smul_one, map_smul, _root_.map_one, map_smul, _root_.map_one]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_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 g : DividedPowerAlgebra S (S ⊗[R] M)
hf : φ f = (dpScalarExtensionInv R S M) f
hg : φ g = (dpScalarExtensionInv R S M) g
⊢ φ (f + g) = (dpScalarExtensionInv R S M) (f + g)
Tactic:
simp only [map_add, hf, hg]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
Proof state before:
case H.h_dp
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)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
⊢ φ (f * dp S n sm) = (dpScalarExtensionInv R S M) (f * dp S n sm)
Tactic:
suffices h_eq : φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm) by
  rw [_root_.map_mul, _root_.map_mul, hf, h_eq]
Proof state after:
case H.h_dp
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)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
⊢ φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm)
Theorem: DividedPowerAlgebra.dpScalarExtensionInv_unique
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
φ : 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)
n : ℕ
sm : S ⊗[R] M
hf : φ f = (dpScalarExtensionInv R S M) f
h_eq : φ (dp S n sm) = (dpScalarExtensionInv R S M) (dp S n sm)
⊢ φ (f * dp S n sm) = (dpScalarExtensionInv R S M) (f * dp S n sm)
Tactic:
rw [_root_.map_mul, _root_.map_mul, hf, h_eq]
Proof state after:
no goals
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 : ℕ
⊢ φ (dp S n 0) = (dpScalarExtensionInv R S M) (dp S n 0)
Tactic:
rw [dp_null]
Proof state after:
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)