-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₃₄).obj ((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₂₃.comp f₁₂) f₃₄).hom.app M) :
          (a : (↑((extendScalars (f₃₄.comp (f₂₃.comp f₁₂))).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars f₃₄).obj ((extendScalars (f₂₃.comp f₁₂)).obj M)) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₃₄).obj ((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))))
h₂ :
  Eq (α := (↑((extendScalars (f₃₄.comp f₂₃)).obj ((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₃₄.comp f₂₃)).hom.app M) :
          (a : (↑((extendScalars ((f₃₄.comp f₂₃).comp f₁₂)).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars (f₃₄.comp f₂₃)).obj ((extendScalars f₁₂).obj M)) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars (f₃₄.comp f₂₃)).obj ((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₃ :
  ∀ (M : ModuleCat R₂) (m : (↑M : Type (max u₁ u_1))),
    Eq (α := (↑((extendScalars f₃₄).obj ((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₃₄).obj ((extendScalars f₂₃).obj M)) : Type (max u₁ u_1)))
          (1 ⊗ₜ[R₂] m) :
        (↑((extendScalars f₃₄).obj ((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₂₃).obj ((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₂₃).obj ((extendScalars f₁₂).obj M)) : Type (max u₁ u_1)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)) : Type (max u₁ u_1)))
    (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m) : R₃ ⊗[R₂] (R₂ ⊗[R₁] (↑M : Type (max u₁ u_1))))
w :
  Eq (α := (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp.{u₁, u_1} f₁₂ f₂₃).hom.app M)) :
          (a : (↑((extendScalars f₃₄).obj ((extendScalars (f₂₃.comp f₁₂)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
    (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)) : R₄ ⊗[R₃] (R₃ ⊗[R₂] (↑((extendScalars f₁₂).obj M) : Type (max u₁ u_1))))
⊢ Eq (α := (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp.{u₁, u_1} f₁₂ f₂₃).hom.app M)) :
          (a : (↑((extendScalars f₃₄).obj ((extendScalars (f₂₃.comp f₁₂)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M)) :
          (a : (↑((extendScalars (f₃₄.comp f₂₃)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
have w₁ : Eq (α := (↑((extendScalars f₃₄).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) : Type (max u_1 u₁)))
  (1 ⊗ₜ[R₃]
      (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₂₃).hom.app M) :
          (a : (↑((extendScalars (f₂₃.comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
    R₄ ⊗[R₃] (↑((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
  (1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)) : R₄ ⊗[R₃] (R₃ ⊗[R₂] (↑((extendScalars f₁₂).obj M) : Type (max u₁ u_1))))
Tactic: rw [h₃, ExtendScalars.map_tmul, h₄]