-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (hypothesis)
Goal:
R₁ R₂ R₃ R₄ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : CommRing R₃
inst_3 : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
h₁ :
  Eq (α := (↑((extendScalars (f₂₃.comp f₁₂) ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R₄) ↦
            (↑x1 : Type (max u₁ u_1)) →ₗ[R₄] (↑x2 : Type (max u₁ u_1))) (CC := carrier)
            ((extendScalarsComp.{u₁, u_1} (f₂₃.comp f₁₂) f₃₄).hom.app M) :
          (a : (↑((extendScalars (f₃₄.comp (f₂₃.comp f₁₂))).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars (f₂₃.comp f₁₂) ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars (f₂₃.comp f₁₂) ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
    (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m) : R₄ ⊗[R₃] (R₃ ⊗[R₁] (↑M : Type (max u₁ u_1))))
h₂ :
  Eq (α := (↑((extendScalars f₁₂ ⋙ extendScalars (f₃₄.comp f₂₃)).obj M) : Type (max u₁ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R₄) ↦
            (↑x1 : Type (max u₁ u_1)) →ₗ[R₄] (↑x2 : Type (max u₁ u_1))) (CC := carrier)
            ((extendScalarsComp.{u₁, u_1} f₁₂ (f₃₄.comp f₂₃)).hom.app M) :
          (a : (↑((extendScalars ((f₃₄.comp f₂₃).comp f₁₂)).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars f₁₂ ⋙ extendScalars (f₃₄.comp f₂₃)).obj M) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂ ⋙ extendScalars (f₃₄.comp f₂₃)).obj M) : Type (max u₁ u_1)))
    (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m) : R₄ ⊗[R₂] (R₂ ⊗[R₁] (↑M : Type (max u₁ u_1))))
⊢ Eq (α := (↑(((extendScalars f₁₂ ⋙ extendScalars f₂₃) ⋙ extendScalars f₃₄).obj M) : Type (max u_1 u₁)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R₄) ↦
            (↑x1 : Type (max u_1 u₁)) →ₗ[R₄] (↑x2 : Type (max u_1 u₁))) (CC := carrier)
            (((extendScalarsComp.{u₁, u_1} (f₂₃.comp f₁₂) f₃₄).hom ≫
                  Functor.whiskerRight (extendScalarsComp.{u₁, u_1} f₁₂ f₂₃).hom (extendScalars f₃₄)).app
              M) :
          (a : (↑((extendScalars (f₃₄.comp (f₂₃.comp f₁₂))).obj M) : Type (max u_1 u₁))) →
            (↑(((extendScalars f₁₂ ⋙ extendScalars f₂₃) ⋙ extendScalars f₃₄).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑(((extendScalars f₁₂ ⋙ extendScalars f₂₃) ⋙ extendScalars f₃₄).obj M) : Type (max u_1 u₁)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R₄) ↦
            (↑x1 : Type (max u_1 u₁)) →ₗ[R₄] (↑x2 : Type (max u_1 u₁))) (CC := carrier)
            (((extendScalarsComp.{u₁, u_1} f₁₂ (f₃₄.comp f₂₃)).hom ≫
                  (extendScalars f₁₂).whiskerLeft (extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).hom ≫
                    ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
              M) :
          (a : (↑((extendScalars (f₃₄.comp (f₂₃.comp f₁₂))).obj M) : Type (max u_1 u₁))) →
            (↑(((extendScalars f₁₂ ⋙ extendScalars f₂₃) ⋙ extendScalars f₃₄).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑(((extendScalars f₁₂ ⋙ extendScalars f₂₃) ⋙ extendScalars f₃₄).obj M) : Type (max u_1 u₁)))
have h₃ : ∀ (M : ModuleCat R₂) (m : (↑M : Type (max u₁ u_1))),
  Eq (α := (↑((extendScalars f₂₃ ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R₄) ↦
            (↑x1 : Type (max u₁ u_1)) →ₗ[R₄] (↑x2 : Type (max u₁ u_1))) (CC := carrier)
            ((extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).hom.app M) :
          (a : (↑((extendScalars (f₃₄.comp f₂₃)).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars f₂₃ ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₂] m) :
      (↑((extendScalars f₂₃ ⋙ extendScalars f₃₄).obj M) : Type (max u₁ u_1)))
    (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m) : R₄ ⊗[R₃] (R₃ ⊗[R₂] (↑M : Type (max u₁ u_1))))
Tactic: have h₃ := extendScalarsComp_hom_app_one_tmul f₂₃ f₃₄