-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Module (goal)
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x : (↑(of R (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(of R (↑A : Type u)) : Type u))
    (((((compr₂ₛₗ (R₄ := R) (M := (↑(of R (↑A : Type u)) : Type u)) (N :=
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) (P :=
                    (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                    (Q := (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
                    RingHom.id R)
                    (TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                    (Hom.hom
                      (CategoryStruct.comp (Y :=
                        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
                          (of R (↑A : Type u)))
                        (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
                        (↟(mul' R (↑A : Type u))))) :
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                      (↑(of R (↑A : Type u)) : Type u)) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
              x :
            (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
              (↑(of R (↑A : Type u)) : Type u)) :
          (a : R) → (↑(of R (↑A : Type u)) : Type u))
        1 :
      (↑(of R (↑A : Type u)) : Type u))
    (((((compr₂ₛₗ (R₄ := R) (M := (↑(of R (↑A : Type u)) : Type u)) (N :=
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) (P :=
                    (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                    (Q := (↑(of R (↑A : Type u)) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
                    RingHom.id R)
                    (TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u))
                    (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u))))) :
                  (↑(of R (↑A : Type u)) : Type u) →ₗ[R]
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                      (↑(of R (↑A : Type u)) : Type u)) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R] (↑(of R (↑A : Type u)) : Type u))
              x :
            (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
              (↑(of R (↑A : Type u)) : Type u)) :
          (a : R) → (↑(of R (↑A : Type u)) : Type u))
        1 :
      (↑(of R (↑A : Type u)) : Type u))
have hf : Eq (α := (↑(of R (↑A : Type u)) : Type u))
  ((((LinearMap.id :
              (a :
                  (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                      (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R]
                    (↑(of R (↑A : Type u)) : Type u)) →
                (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                    (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u) →ₗ[R]
                  (↑(of R (↑A : Type u)) : Type u))
            (Hom.hom
              (CategoryStruct.comp (Y :=
                MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
                (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
                (↟(mul' R (↑A : Type u))))) :
          (↑(of R (↑A : Type u)) : Type u) ⊗[R]
              (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
            (↑(of R (↑A : Type u)) : Type u)) :
        (a : (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) →
          (↑(of R (↑A : Type u)) : Type u))
      ((((TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  R →ₗ[R]
                    (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
              x :
            R →ₗ[R]
              (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
          (a : R) → (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
        1) :
    (↑(of R (↑A : Type u)) : Type u))
  ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u)))) :
        (a : (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) →
          (↑(of R (↑A : Type u)) : Type u))
      ((((TensorProduct.mk R (↑(of R (↑A : Type u)) : Type u)
                  (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) :
                (a : (↑(of R (↑A : Type u)) : Type u)) →
                  R →ₗ[R]
                    (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
              x :
            R →ₗ[R]
              (↑(of R (↑A : Type u)) : Type u) ⊗[R]
                (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u)) :
          (a : R) → (↑(of R (↑A : Type u)) : Type u) ⊗[R] (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u))
        1) :
    (↑(of R (↑A : Type u)) : Type u))
Tactic: erw [compr₂_apply, compr₂ₛₗ_apply]