awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
this :
  HasColimit
    ((F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
t : IsColimit (HasColimit.colimitCocone F)
⊢ IsColimit (F :=
    (F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCocone
      (forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      ((restrictScalars f).mapCocone (HasColimit.colimitCocone F)))

Tactic:
apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGrpCat.{v})
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
this :
  HasColimit
    ((F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
⊢ IsColimit (HasColimit.colimitCocone F)

Tactic:
exact HasColimit.isColimitColimitCocone F

Premises used: ModuleCat.HasColimit.isColimitColimitCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑M : Type (max u₁ u_1))
⊢ Eq (α := (↑(Functor.obj (extendScalars (RingHom.id R)) 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) (NatTrans.app (Iso.inv (extendScalarsId.{u₁, u_1} R)) M) :
          (a : (↑((𝟭 (ModuleCat R)).obj M) : Type (max u₁ u_1))) →
            (↑((extendScalars (RingHom.id R)).obj M) : Type (max u₁ u_1)))
        m :
      (↑(Functor.obj (extendScalars (RingHom.id R)) M) : Type (max u₁ u_1)))
    (1 ⊗ₜ[R] m : R ⊗[R] (↑M : Type (max u₁ u_1)))

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
hf :
  ∀ (m : (↑M : Type (max u_1 u₁))),
    Eq (α := (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
      ((Hom.hom
              ((Adjunction.homEquiv (extendRestrictScalarsAdj.{u_1, u₁, u₁} (RingHom.id R)) M
                    (Functor.obj (𝟭 (ModuleCat R)) M) :
                  (a : (extendScalars (RingHom.id R)).obj M ⟶ (𝟭 (ModuleCat R)).obj M) →
                    M ⟶ (restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M))
                (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M)) :
            (a : (↑M : Type (max u_1 u₁))) →
              (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
          m :
        (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
      ((Hom.hom (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
            (a : (↑M : Type (max u_1 u₁))) →
              (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
          m :
        (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
⊢ (Adjunction.homEquiv (extendRestrictScalarsAdj.{u_1, u₁, u₁} (RingHom.id R)) M (Functor.obj (𝟭 (ModuleCat R)) M) :
        (a : (extendScalars (RingHom.id R)).obj M ⟶ (𝟭 (ModuleCat R)).obj M) →
          M ⟶ (restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M))
      (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M) =
    NatTrans.app (Iso.inv (restrictScalarsId R)) M

Tactic:
ext m
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑M : Type (max u_1 u₁))
hf :
  Eq (α := (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) 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 (Iso.inv (extendScalarsId.{u₁, u_1} R)) M ≫
              NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M) :
          (a : (↑((𝟭 (ModuleCat R)).obj M) : Type (max u_1 u₁))) → (↑((𝟭 (ModuleCat R)).obj M) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (𝟭 (ModuleCat R)) M) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
⊢ Eq (α := (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
    ((Hom.hom
            ((Adjunction.homEquiv (extendRestrictScalarsAdj.{u_1, u₁, u₁} (RingHom.id R)) M
                  (Functor.obj (𝟭 (ModuleCat R)) M) :
                (a : (extendScalars (RingHom.id R)).obj M ⟶ (𝟭 (ModuleCat R)).obj M) →
                  M ⟶ (restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M))
              (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M)) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))

Tactic:
rw [extendRestrictScalarsAdj_homEquiv_apply, ← extendScalarsId_inv_app_apply, ← comp_apply]

Premises used: ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, ModuleCat.comp_apply, ModuleCat.extendScalarsId_inv_app_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑M : Type (max u_1 u₁))
⊢ Eq (α := (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) 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 (Iso.inv (extendScalarsId.{u₁, u_1} R)) M ≫
              NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M) :
          (a : (↑((𝟭 (ModuleCat R)).obj M) : Type (max u_1 u₁))) → (↑((𝟭 (ModuleCat R)).obj M) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (𝟭 (ModuleCat R)) M) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑M : Type (max u₁ u_1))
rw :
  (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₁ u_1)) →ₗ[R] (↑x2 : Type (max u₁ u_1))) carrier
          (fun (X Y : ModuleCat R) ↦
            (LinearMap.instFunLike :
              FunLike ((↑X : Type (max u₁ u_1)) →ₗ[R] (↑Y : Type (max u₁ u_1))) (↑X : Type (max u₁ u_1))
                (↑Y : Type (max u₁ u_1))))
          _ _ _ (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
        (a : (↑M : Type (max u₁ u_1))) →
          (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u₁ u_1)))
      m =
    m
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₁ u_1)) →ₗ[R] (↑x2 : Type (max u₁ u_1)))
          (CC := carrier) (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M) :
        (a : (↑((extendScalars (RingHom.id R)).obj M) : Type (max u₁ u_1))) →
          (↑((𝟭 (ModuleCat R)).obj M) : Type (max u₁ u_1)))
      (1 ⊗ₜ[R] m) =
    m

Tactic:
rw [← extendRestrictScalarsAdj_homEquiv_apply,
    homEquiv_extendScalarsId]

Premises used: ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, ModuleCat.homEquiv_extendScalarsId
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑M : Type (max u₁ u_1))
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₁ u_1)) →ₗ[R] (↑x2 : Type (max u₁ u_1))) carrier
          (fun (X Y : ModuleCat R) ↦
            (LinearMap.instFunLike :
              FunLike ((↑X : Type (max u₁ u_1)) →ₗ[R] (↑Y : Type (max u₁ u_1))) (↑X : Type (max u₁ u_1))
                (↑Y : Type (max u₁ u_1))))
          _ _ _ (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
        (a : (↑M : Type (max u₁ u_1))) →
          (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u₁ u_1)))
      m =
    m

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ R₃ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : (↑M : Type (max u₁ u_1))
rw :
  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)
            ((extendRestrictScalarsAdj.{u_1, u₁, u₁} f₁₂).unit.app M ≫
              (restrictScalars f₁₂).map
                  ((extendRestrictScalarsAdj.{u_1, u₁, u₁} f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
                (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))) :
          (a : (↑M : Type (max u₁ u_1))) →
            (↑((restrictScalars (f₂₃.comp f₁₂)).obj ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M)) :
              Type (max u₁ u_1)))
        m :
      (↑((restrictScalars (f₂₃.comp f₁₂)).obj ((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:
rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp]

Premises used: ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, ModuleCat.homEquiv_extendScalarsComp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ R₂ R₃ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
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)
            ((extendRestrictScalarsAdj.{u_1, u₁, u₁} f₁₂).unit.app M ≫
              (restrictScalars f₁₂).map
                  ((extendRestrictScalarsAdj.{u_1, u₁, u₁} f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
                (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))) :
          (a : (↑M : Type (max u₁ u_1))) →
            (↑((restrictScalars (f₂₃.comp f₁₂)).obj ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M)) :
              Type (max u₁ u_1)))
        m :
      (↑((restrictScalars (f₂₃.comp f₁₂)).obj ((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:
rfl
-- 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₄
w :
  ∀ (M : ModuleCat R₁) (m : (↑M : Type (max u_1 u₁))),
    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₁)))
⊢ (extendScalarsComp.{u₁, u_1} (f₂₃.comp f₁₂) f₃₄).hom ≫
      Functor.whiskerRight (extendScalarsComp.{u₁, u_1} f₁₂ f₂₃).hom (extendScalars f₃₄) =
    (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

Tactic:
ext 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₄
M : ModuleCat R₁
m : (↑M : Type (max u_1 u₁))
⊢ 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))))

Tactic:
have h₁ := extendScalarsComp_hom_app_one_tmul (f₂₃.comp 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₄
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))))
⊢ 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))))

Tactic:
have h₂ := extendScalarsComp_hom_app_one_tmul f₁₂ (f₃₄.comp 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₄
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))))
⊢ ∀ (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₃₄