Theorem: TensorProduct.includeRight_lid (DividedPowers/PolynomialMap/Basic.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
m : R ⊗[R] M
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (rTensor M (algebraMap' R S).toLinearMap) m
Tactic:
suffices ∀ m, (rTensor M (algebraMap' R S).toLinearMap).comp
  (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
  simp only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.symm_apply_apply]
State after:
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
m : R ⊗[R] M
⊢ ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m

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
m : R ⊗[R] M
⊢ ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
Tactic:
intro z
State after:
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
m : R ⊗[R] M
z : M
⊢ (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) z = 1 ⊗ₜ[R] z

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
m : R ⊗[R] M
z : M
⊢ (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) z = 1 ⊗ₜ[R] z
Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lid_symm_apply, rTensor_tmul,
  AlgHom.toLinearMap_apply, _root_.map_one]
State after:
no goals

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
m : R ⊗[R] M
this : ∀ (m : M), (rTensor M (algebraMap' R S).toLinearMap ∘ₗ ↑(TensorProduct.lid R M).symm) m = 1 ⊗ₜ[R] m
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (rTensor M (algebraMap' R S).toLinearMap) m
Tactic:
simp only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.symm_apply_apply]
State after:
no goals