Theorem: LinearForm.baseChange_compat_apply (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
m : S ⊗[R] M
⊢ φ ((baseChange R S M f) m) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) m)
Tactic:
induction' m using TensorProduct.induction_on with r m x y hx hy
State after:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
⊢ φ ((baseChange R S M f) 0) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) 0)

case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
r : S
m : M
⊢ φ ((baseChange R S M f) (r ⊗ₜ[R] m)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (r ⊗ₜ[R] m))

case add
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
x y : S ⊗[R] M
hx : φ ((baseChange R S M f) x) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) x)
hy : φ ((baseChange R S M f) y) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) y)
⊢ φ ((baseChange R S M f) (x + y)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (x + y))

State before:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
⊢ φ ((baseChange R S M f) 0) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) 0)
Tactic:
simp only [map_zero]
State after:
no goals

State before:
case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
r : S
m : M
⊢ φ ((baseChange R S M f) (r ⊗ₜ[R] m)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (r ⊗ₜ[R] m))
Tactic:
simp only [baseChange, coe_comp, Function.comp_apply, baseChange_tmul,
  AlgHom.toLinearMap_apply, rid'_tmul, map_smul, rTensor_tmul]
State after:
no goals

State before:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S' : Type u_4
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
f : M →ₗ[R] R
x y : S ⊗[R] M
hx : φ ((baseChange R S M f) x) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) x)
hy : φ ((baseChange R S M f) y) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) y)
⊢ φ ((baseChange R S M f) (x + y)) = (baseChange R S' M f) ((LinearMap.rTensor M φ.toLinearMap) (x + y))
Tactic:
simp only [map_add, hx, hy]
State after:
no goals