-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@[reassoc]
lemma extendScalars_id_comp :
    (extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫ whiskerRight (extendScalarsId R₁).hom _ ≫
      (Functor.leftUnitor _).hom = 𝟙 _

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M))) (1 ⊗ₜ[R₁] 1 ⊗ₜ[R₁] m) = LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
rw [ExtendScalars.map_tmul]

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] (ConcreteCategory.hom ((extendScalarsId R₁).hom.app M)) (1 ⊗ₜ[R₁] m) = LinearMap.id (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] (ConcreteCategory.hom ((extendScalarsId R₁).hom.app M)) (1 ⊗ₜ[R₁] m) = LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
erw [extendScalarsId_hom_app_one_tmul]

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = LinearMap.id (1 ⊗ₜ[R₁] m)

Proof state:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
      whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫ (extendScalars f₁₂).leftUnitor.hom =
    𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))

Tactic:
ext M m

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
              whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫ (extendScalars f₁₂).leftUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))).app M)) (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
rfl

Result:
no goals

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M)))
      ((Hom.hom ((extendScalarsComp (RingHom.id R₁) f₁₂).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
erw [extendScalarsComp_hom_app_one_tmul (RingHom.id R₁) f₁₂ M m]

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M))) (1 ⊗ₜ[R₁] 1 ⊗ₜ[R₁] m) = LinearMap.id (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (RingHom.id R₁) f₁₂).hom ≫
              whiskerRight (extendScalarsId R₁).hom (extendScalars f₁₂) ≫ (extendScalars f₁₂).leftUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))).app M)) (1 ⊗ₜ[R₁] m)

Tactic:
dsimp

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalars f₁₂).map ((extendScalarsId R₁).hom.app M)))
      ((Hom.hom ((extendScalarsComp (RingHom.id R₁) f₁₂).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)