awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₁)))
    ((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₁)))
have 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₁)))
Tactic: rw [extendRestrictScalarsAdj_homEquiv_apply, ← extendScalarsId_inv_app_apply, ← comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
m : (↑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.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
have 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
Tactic: rw [← extendRestrictScalarsAdj_homEquiv_apply,
    homEquiv_extendScalarsId]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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)
            ((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))))
have 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))))
Tactic: rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp]
-- 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₄
⊢ (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
have 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₁)))
Tactic: ext M m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (hypothesis)
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₁₂ ⋙ 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₁)))
have 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))))
Tactic: have h₁ := extendScalarsComp_hom_app_one_tmul (f₂₃.comp f₁₂) f₃₄ M m
-- 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₄
⊢ (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₁₂)))
have 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₁₂)))
Tactic: rw [extendScalars_assoc_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ 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₁)))
have 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₁)))
Tactic: ext M m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₁)))
    ((@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₁)))
have 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₁)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₁)))
    ((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₁)))
have 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₁)))
Tactic: erw [extendScalarsComp_hom_app_one_tmul (RingHom.id R₁) f₁₂ M m]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₁)))
    ((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₁)))
have 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₁)))
Tactic: rw [ExtendScalars.map_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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₁]
        (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₁)))
have 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))
Tactic: erw [extendScalarsId_hom_app_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R₁ R₂ : Type u₁
inst : CommRing R₁
inst_1 : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (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₁₂))
have 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₁)))
Tactic: ext M m