-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@[reassoc]
lemma extendScalars_assoc :
    (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫ whiskerRight (extendScalarsComp f₁₂ f₂₃).hom _ =
      (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫ whiskerLeft _ (extendScalarsComp f₂₃ f₃₄).hom ≫
        (Functor.associator _ _ _).inv

Proof state:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Tactic:
have h₃ := extendScalarsComp_hom_app_one_tmul f₂₃ f₃₄

Result:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Tactic:
have h₄ := extendScalarsComp_hom_app_one_tmul f₁₂ f₂₃ M m

Result:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] 1 ⊗ₜ[R₂] m
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m
⊢ (Hom.hom ((extendScalars f₃₄).map ((extendScalarsComp f₁₂ f₂₃).hom.app M))) (1 ⊗ₜ[R₃] 1 ⊗ₜ[R₁] m) =
    (Hom.hom ((extendScalarsComp f₂₃ f₃₄).hom.app ((extendScalars f₁₂).obj M))) (1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m)

Tactic:
rw [h₃, ExtendScalars.map_tmul, h₄]

Result:
no goals

Proof state:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫ whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄) =
    (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv

Tactic:
ext M m

Result:
case w.h.h
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)