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

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

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

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

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

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

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

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

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

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