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

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₂]
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))

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

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

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

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

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

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⟩ _
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))

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