awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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))))
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))))
⊢ 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₂₃ M m
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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₄
rw :
  (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 ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            (extendScalars f₁₂).whiskerLeft (extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).inv ≫
              (extendScalarsComp.{u₁, u_1} f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))
⊢ (extendScalarsComp.{u₁, u_1} (f₂₃.comp f₁₂) f₃₄).hom ≫
      Functor.whiskerRight (extendScalarsComp.{u₁, u_1} f₁₂ f₂₃).hom (extendScalars f₃₄) ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
          (extendScalars f₁₂).whiskerLeft (extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).inv ≫
            (extendScalarsComp.{u₁, u_1} f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
rw [extendScalars_assoc_assoc]

Premises used: ModuleCat.extendScalars_assoc_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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₄
⊢ (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 ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            (extendScalars f₁₂).whiskerLeft (extendScalarsComp.{u₁, u_1} f₂₃ f₃₄).inv ≫
              (extendScalarsComp.{u₁, u_1} f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
simp only [Iso.inv_hom_id_assoc, ← Functor.whiskerLeft_comp_assoc, Iso.hom_inv_id,
    Functor.whiskerLeft_id', Category.id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.whiskerLeft_comp_assoc, CategoryTheory.Functor.whiskerLeft_id', CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
w :
  ∀ (M : ModuleCat R₁) (m : (↑M : Type (max u_1 u₁))),
    Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      ((@ConcreteCategory.hom _ (moduleCategory R₂)
              (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
              (fun (X Y : ModuleCat R₂) ↦
                (LinearMap.instFunLike :
                  FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                    (↑Y : Type (max u_1 u₁))))
              _ _ _
              ((Iso.hom (extendScalarsComp.{u₁, u_1} (RingHom.id R₁) f₁₂) ≫
                    Functor.whiskerRight (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) (extendScalars f₁₂) ≫
                      (extendScalars f₁₂).leftUnitor.hom).app
                M) :
            (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
        (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      ((@ConcreteCategory.hom _ (moduleCategory R₂)
              (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
              (fun (X Y : ModuleCat R₂) ↦
                (LinearMap.instFunLike :
                  FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                    (↑Y : Type (max u_1 u₁))))
              _ _ _ (NatTrans.app (𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))) M) :
            (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
        (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
⊢ Iso.hom (extendScalarsComp.{u₁, u_1} (RingHom.id R₁) f₁₂) ≫
      Functor.whiskerRight (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) (extendScalars f₁₂) ≫
        (extendScalars f₁₂).leftUnitor.hom =
    𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))

Tactic:
ext M m
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w :
  Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₁₂).map (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M)) :
          (a : (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsComp.{u₁, u_1} (RingHom.id R₁) f₁₂)) M) :
            (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _
            ((Iso.hom (extendScalarsComp.{u₁, u_1} (RingHom.id R₁) f₁₂) ≫
                  Functor.whiskerRight (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) (extendScalars f₁₂) ≫
                    (extendScalars f₁₂).leftUnitor.hom).app
              M) :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _ (NatTrans.app (𝟙 (extendScalars (f₁₂.comp (RingHom.id R₁)))) M) :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w :
  Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₁₂).map (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M)) :
          (a : (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₁₂).map (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M)) :
          (a : (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsComp.{u₁, u_1} (RingHom.id R₁) f₁₂)) M) :
            (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))

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

Premises used: ModuleCat.extendScalarsComp_hom_app_one_tmul, RingHom.id
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w :
  Eq (α := (↑((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)
              (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M) :
            (a : (↑((extendScalars (RingHom.id R₁)).obj M) : Type (max u_1 u₁))) → (↑M : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
      R₂ ⊗[R₁] (↑M : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom ((extendScalars f₁₂).map (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M)) :
          (a : (↑((extendScalars f₁₂).obj ((extendScalars (RingHom.id R₁)).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))

Tactic:
rw [ExtendScalars.map_tmul]

Premises used: ModuleCat.ExtendScalars.map_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w :
  Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁))) (1 ⊗ₜ[R₁] m)
    ((LinearMap.id :
        (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
          (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      (1 ⊗ₜ[R₁] m))
⊢ Eq (α := (↑((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)
              (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₁)) M) :
            (a : (↑((extendScalars (RingHom.id R₁)).obj M) : Type (max u_1 u₁))) → (↑M : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
      R₂ ⊗[R₁] (↑M : Type (max u_1 u₁)))
    ((LinearMap.id :
          (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))

Tactic:
erw [extendScalarsId_hom_app_one_tmul]

Premises used: ModuleCat.extendScalarsId_hom_app_one_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁))) (1 ⊗ₜ[R₁] m)
    ((LinearMap.id :
        (a : (↑((extendScalars (f₁₂.comp (RingHom.id R₁))).obj M) : Type (max u_1 u₁))) →
          (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      (1 ⊗ₜ[R₁] m))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
w :
  ∀ (M : ModuleCat R₁) (m : (↑M : Type (max u_1 u₁))),
    Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      ((@ConcreteCategory.hom _ (moduleCategory R₂)
              (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
              (fun (X Y : ModuleCat R₂) ↦
                (LinearMap.instFunLike :
                  FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                    (↑Y : Type (max u_1 u₁))))
              _ _ _
              (((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom ≫
                    (extendScalars f₁₂).whiskerLeft (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ≫
                      (extendScalars f₁₂).rightUnitor.hom).app
                M) :
            (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
        (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
      ((@ConcreteCategory.hom _ (moduleCategory R₂)
              (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
              (fun (X Y : ModuleCat R₂) ↦
                (LinearMap.instFunLike :
                  FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                    (↑Y : Type (max u_1 u₁))))
              _ _ _ (NatTrans.app (𝟙 (extendScalars (RingHom.comp (RingHom.id R₂) f₁₂))) M) :
            (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m) :
        (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
⊢ (extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom ≫
      (extendScalars f₁₂).whiskerLeft (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ≫ (extendScalars f₁₂).rightUnitor.hom =
    𝟙 (extendScalars (RingHom.comp (RingHom.id R₂) f₁₂))

Tactic:
ext M m
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w :
  Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ((extendScalars f₁₂).obj M)) :
          (a : (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        ((Hom.hom ((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom.app M) :
            (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    (1 ⊗ₜ[R₁] m :
      (↑((restrictScalars (RingHom.comp (RingHom.id R₂) f₁₂)).obj (of R₂ R₂)) : Type u₁) ⊗[R₁] (↑M : Type (max u_1 u₁)))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _
            (((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom ≫
                  (extendScalars f₁₂).whiskerLeft (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ≫
                    (extendScalars f₁₂).rightUnitor.hom).app
              M) :
          (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((@ConcreteCategory.hom _ (moduleCategory R₂)
            (fun (x1 x2 : ModuleCat R₂) ↦ (↑x1 : Type (max u_1 u₁)) →ₗ[R₂] (↑x2 : Type (max u_1 u₁))) carrier
            (fun (X Y : ModuleCat R₂) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u_1 u₁)) →ₗ[R₂] (↑Y : Type (max u_1 u₁))) (↑X : Type (max u_1 u₁))
                  (↑Y : Type (max u_1 u₁))))
            _ _ _ (NatTrans.app (𝟙 (extendScalars (RingHom.comp (RingHom.id R₂) f₁₂))) M) :
          (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        (1 ⊗ₜ[R₁] m) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
w : Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁))) (1 ⊗ₜ[R₁] m) (1 ⊗ₜ[R₁] m)
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R₂)) ((extendScalars f₁₂).obj M)) :
          (a : (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁))) →
            (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
        ((Hom.hom ((extendScalarsComp.{u₁, u_1} f₁₂ (RingHom.id R₂)).hom.app M) :
            (a : (↑((extendScalars ((RingHom.id R₂).comp f₁₂)).obj M) : Type (max u_1 u₁))) →
              (↑((extendScalars (RingHom.id R₂)).obj ((extendScalars f₁₂).obj M)) : Type (max u_1 u₁)))
          (1 ⊗ₜ[R₁] m)) :
      (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁)))
    (1 ⊗ₜ[R₁] m :
      (↑((restrictScalars (RingHom.comp (RingHom.id R₂) f₁₂)).obj (of R₂ R₂)) : Type u₁) ⊗[R₁] (↑M : Type (max u_1 u₁)))

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

Premises used: ModuleCat.extendScalarsId_hom_app_one_tmul, ModuleCat.extendScalarsComp_hom_app_one_tmul, RingHom.id
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
⊢ Eq (α := (↑((extendScalars f₁₂).obj M) : Type (max u_1 u₁))) (1 ⊗ₜ[R₁] m) (1 ⊗ₜ[R₁] m)

Tactic:
rfl