[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ ⦃I : Ideal R⦄, Ideal.FG I → Injective ↑(lift (comp (lsmul R R) (Submodule.subtype I)))
[PROOFSTEP]
intro I _
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ Injective ↑(lift (comp (lsmul R R) (Submodule.subtype I)))
[PROOFSTEP]
rw [← Equiv.injective_comp (TensorProduct.rid R I).symm.toEquiv]
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ Injective
    (↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
      ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))))
[PROOFSTEP]
convert Subtype.coe_injective using 1
[GOAL]
case h.e'_3
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
⊢ ↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
      ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))) =
    fun a => ↑a
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : Ideal.FG I
x : { x // x ∈ I }
⊢ (↑(lift (comp (lsmul R R) (Submodule.subtype I))) ∘
        ↑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.rid R { x // x ∈ I }))))
      x =
    ↑x
[PROOFSTEP]
simp only [Function.comp_apply, LinearEquiv.coe_toEquiv, rid_symm_apply, comp_apply, mul_one, lift.tmul,
  Submodule.subtype_apply, Algebra.id.smul_eq_mul, lsmul_apply]
