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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : (↑((restrictScalars f).obj ((coextendScalars f).obj X)) : Type (max u₂ u_1))
h : (f : (a : R) → S) r = HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1
⊢ Eq (α := (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              g :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        ((f : (a : R) → S) r) :
      (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              g :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1) :
      (↑X : Type (max u₂ u_1)))

Tactic:
congr
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : (↑((restrictScalars f).obj ((coextendScalars f).obj X)) : Type (max u₂ u_1))
h : (f : (a : R) → S) r = HSMul.hSMul (α := S) (β := S) ((f : (a : R) → S) r : S) 1
⊢ (f : (a : R) → S) r = HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1

Tactic:
change f r = f r • (1 : S)

Premises used: OfNat.ofNat, DFunLike.coe
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : (↑((restrictScalars f).obj ((coextendScalars f).obj X)) : Type (max u₂ u_1))
⊢ (f : (a : R) → S) r = HSMul.hSMul (α := S) (β := S) ((f : (a : R) → S) r : S) 1

Tactic:
simp
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
hf :
  ∀ (x : (↑((restrictScalars f).obj X) : Type (max u₂ v))),
    Eq (α := (↑Y : Type (max u₂ v)))
      ((Hom.hom
              (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f
                (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f g)) :
            (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          x :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom g : (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) x :
        (↑Y : Type (max u₂ v)))
⊢ RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f
      (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f g) =
    g

Tactic:
ext
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
x : (↑((restrictScalars f).obj X) : Type (max u₂ v))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f
              (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f g)) :
          (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) x :
      (↑Y : Type (max u₂ v)))

Tactic:
simp
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
hf :
  ∀ (x : (↑X : Type (max u₂ v))) (x_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂)),
    Eq (α := (↑Y : Type (max u₂ v)))
      ((((CoextendScalars.equiv f Y :
                  (a : (↑((coextendScalars f).obj Y) : Type (max u₂ v))) →
                    (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v)))
                ((Hom.hom
                      (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f
                        (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f g)) :
                    (a : (↑X : Type (max u₂ v))) → (↑((coextendScalars f).obj Y) : Type (max u₂ v)))
                  x) :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v))) :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑Y : Type (max u₂ v)))
          x_1 :
        (↑Y : Type (max u₂ v)))
      ((((CoextendScalars.equiv f Y :
                  (a : (↑((coextendScalars f).obj Y) : Type (max u₂ v))) →
                    (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v)))
                ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((coextendScalars f).obj Y) : Type (max u₂ v))) x) :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v))) :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑Y : Type (max u₂ v)))
          x_1 :
        (↑Y : Type (max u₂ v)))
⊢ RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f
      (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f g) =
    g

Tactic:
ext
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x : (↑X : Type (max u₂ v))
x_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂)
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((((CoextendScalars.equiv f Y :
                (a : (↑((coextendScalars f).obj Y) : Type (max u₂ v))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v)))
              ((Hom.hom
                    (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f
                      (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f g)) :
                  (a : (↑X : Type (max u₂ v))) → (↑((coextendScalars f).obj Y) : Type (max u₂ v)))
                x) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑Y : Type (max u₂ v)))
        x_1 :
      (↑Y : Type (max u₂ v)))
    ((((CoextendScalars.equiv f Y :
                (a : (↑((coextendScalars f).obj Y) : Type (max u₂ v))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v)))
              ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((coextendScalars f).obj Y) : Type (max u₂ v))) x) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑Y : Type (max u₂ v)))
        x_1 :
      (↑Y : Type (max u₂ v)))

Tactic:
simp
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
hf :
  ∀ (x : (↑((restrictScalars f).obj X) : Type (max u₂ v))),
    Eq (α := (↑Y : Type (max u₂ v)))
      ((Hom.hom
              ((Equiv.symm
                    { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f,
                      invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f, left_inv := ⋯,
                      right_inv := ⋯ } :
                  (a : X ⟶ (coextendScalars f).obj Y) → (restrictScalars f).obj X ⟶ Y)
                g) :
            (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          x :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom ((restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit'.{u₁, u₂, v} f).app Y) :
            (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          x :
        (↑Y : Type (max u₂ v)))
⊢ (Equiv.symm
          { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f,
            invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f, left_inv := ⋯, right_inv := ⋯ } :
        (a : X ⟶ (coextendScalars f).obj Y) → (restrictScalars f).obj X ⟶ Y)
      g =
    (restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit'.{u₁, u₂, v} f).app Y

Tactic:
ext
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x : (↑((restrictScalars f).obj X) : Type (max u₂ v))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm
                  { toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f,
                    invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f, left_inv := ⋯,
                    right_inv := ⋯ } :
                (a : X ⟶ (coextendScalars f).obj Y) → (restrictScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((restrictScalars f).map g ≫ (RestrictionCoextensionAdj.counit'.{u₁, u₂, v} f).app Y) :
          (a : (↑((restrictScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))

Tactic:
simp [RestrictionCoextensionAdj.counit']

Premises used: ModuleCat.RestrictionCoextensionAdj.counit'
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
⊢ (restrictScalars f).IsLeftAdjoint

Tactic:
(restrictCoextendScalarsAdj f).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, ModuleCat.restrictCoextendScalarsAdj
-- 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₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
⊢ (coextendScalars f).IsRightAdjoint

Tactic:
(restrictCoextendScalarsAdj f).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, ModuleCat.restrictCoextendScalarsAdj
-- 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₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x x_1 : (↑X : Type (max u₂ u_1))
dsimp :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (x + x_1)) =
    HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (β :=
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x) :
        (↑Y : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x_1) :
        (↑Y : Type (max u₂ u_1)))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (x + x_1)) =
    HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (β :=
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x) :
        (↑Y : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x_1) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
dsimp
-- 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₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : (↑X : Type (max u₂ u_1))
dsimp :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (r • s)) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ u_1)))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (r • s)) =
    HSMul.hSMul (α := R) (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) ((RingHom.id R : (a : R) → R) r : R)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
dsimp
-- 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₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : (↑X : Type (max u₂ u_1))
rw :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R]
          (AddEquiv.symm (RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1))) :
              (a : (↑X : Type (max u₂ u_1))) → RestrictScalars R R (↑X : Type (max u₂ u_1)))
            (HSMul.hSMul (α := R) (β := (↑X : Type (max u₂ u_1))) ((algebraMap R R : (a : R) → R) r : R)
              ((RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1)) :
                    (a : RestrictScalars R R (↑X : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                  s :
                (↑X : Type (max u₂ u_1))))) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := S) (β := (↑((extendScalars f).obj X) : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
          (1 ⊗ₜ[R] s)) :
      (↑Y : Type (max u₂ u_1)))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (r • s)) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
rw [RestrictScalars.smul_def, ← LinearMap.map_smul]

Premises used: LinearMap.map_smul, RestrictScalars.smul_def
-- 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₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : (↑X : Type (max u₂ u_1))
erw :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := R) (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂)))
          ((algebraMap R R : (a : R) → R) r : R)
          (1 ⊗ₜ[R]
              (RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1)) :
                  (a : RestrictScalars R R (↑X : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                s :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂)))) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := S) (β := (↑((extendScalars f).obj X) : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
          (1 ⊗ₜ[R] s)) :
      (↑Y : Type (max u₂ u_1)))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R]
          (AddEquiv.symm (RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1))) :
              (a : (↑X : Type (max u₂ u_1))) → RestrictScalars R R (↑X : Type (max u₂ u_1)))
            (HSMul.hSMul (α := R) (β := (↑X : Type (max u₂ u_1))) ((algebraMap R R : (a : R) → R) r : R)
              ((RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1)) :
                    (a : RestrictScalars R R (↑X : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                  s :
                (↑X : Type (max u₂ u_1))))) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := S) (β := (↑((extendScalars f).obj X) : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
          (1 ⊗ₜ[R] s)) :
      (↑Y : Type (max u₂ u_1)))

Tactic:
erw [tmul_smul]

Premises used: TensorProduct.tmul_smul
-- 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₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
r : R
s : (↑X : Type (max u₂ u_1))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := R) (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂)))
          ((algebraMap R R : (a : R) → R) r : R)
          (1 ⊗ₜ[R]
              (RestrictScalars.addEquiv R R (↑X : Type (max u₂ u_1)) :
                  (a : RestrictScalars R R (↑X : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                s :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂)))) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (α := S) (β := (↑((extendScalars f).obj X) : Type (max u₂ u_1))) ((f : (a : R) → S) r : S)
          (1 ⊗ₜ[R] s)) :
      (↑Y : Type (max u₂ u_1)))

Tactic:
congr