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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
s : S
y : (↑Y : Type (max u₂ u_1))
t : S
⊢ 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)))
              (((CoextendScalars.equiv f X).symm :
                  (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) →
                    (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                {
                  toFun := fun (s_1 : S) ↦
                    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type (max u₂ u_1)) →ₗ[R] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                        (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                      (s_1 • s • y),
                  map_add' := ⋯, map_smul' := ⋯ }) :
            (↑((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)))
        t :
      (↑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)))
              (HSMul.hSMul (α := S) (β :=
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)))
                ((RingHom.id S : (a : S) → S) s : S)
                (((CoextendScalars.equiv f X).symm :
                      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) →
                        (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                    {
                      toFun := fun (s : S) ↦
                        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type (max u₂ u_1)) →ₗ[R] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                            (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                          (s • y),
                      map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))) :
            (↑((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)))
        t :
      (↑X : Type (max u₂ u_1)))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
s : S
⊢ 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)))
              ((Hom.hom (fromRestriction.{u₁, u₂, u_1} f g) :
                  (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                y) :
            (↑((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)))
        s :
      (↑X : 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) g :
          (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
        (s • y) :
      (↑X : Type (max u₂ u_1)))

Tactic:
rfl

Premises used: rfl
-- 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
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
x y : (↑((restrictScalars f).obj Y) : 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)))
            ((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 : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
              (x + y)) :
          (↑((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)))
      1 =
    HAdd.hAdd (α := (↑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)))
              ((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 : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                x) :
            (↑((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)))
        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)))
              ((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 : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                y) :
            (↑((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)))
        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 R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
r : R
y : (↑Y : Type (max u₂ u_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)))
              ((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 : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                (r • y)) :
            (↑((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)))
        1 :
      (↑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)))
              ((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 : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                y) :
            (↑((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)))
        (HMul.hMul (α := S) (β := S)
          (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) ((RingHom.id R : (a : R) → R) r : R) : S) (1 : S)) :
      (↑X : Type (max u₂ u_1)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
y : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))
⊢ Eq (α := (↑X : Type (max u₂ u_1)))
    ((Hom.hom (toRestriction.{u₁, u₂, u_1} f g) :
          (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
        y :
      (↑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)))
              ((Hom.hom g : (a : (↑Y : Type (max u₂ u_1))) → (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) y) :
            (↑((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)))
        1 :
      (↑X : Type (max u₂ u_1)))

Tactic:
rfl

Premises used: rfl
-- 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
Y : ModuleCat.{u_1, u₂} S
y : (↑Y : Type u_1)
r : R
s : S
erw :
  HMul.hMul (α := S) (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) r : S) s • y =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)
⊢ (r • s) • y = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)

Tactic:
erw [smul_eq_mul]

Premises used: smul_eq_mul
-- 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
Y : ModuleCat.{u_1, u₂} S
y : (↑Y : Type u_1)
r : R
s : S
⊢ HMul.hMul (α := S) (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) r : S) s • y =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_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 : Ring R
inst_3 : Ring S
f : R →+* S
Y : ModuleCat.{u_1, u₂} S
s : S
y : (↑Y : Type u_1)
t : S
⊢ Eq.{u_1 + 1} (α := (↑((restrictScalars f).obj Y) : Type u_1))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y) :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1))
              ((LinearEquiv.symm (CoextendScalars.equiv f ((restrictScalars f).obj Y)) :
                  (a :
                      (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1)) →
                    (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                { toFun := fun (s_1 : S) ↦ s_1 • s • y, map_add' := ⋯, map_smul' := ⋯ }) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑((restrictScalars f).obj Y) : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y) : Type u_1))
        t :
      (↑((restrictScalars f).obj Y) : Type u_1))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y) :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1))
              (HSMul.hSMul (α := S) (β := (↑((restrictScalars f ⋙ coextendScalars f).obj Y) : Type (max u₂ u_1)))
                ((RingHom.id S : (a : S) → S) s : S)
                ((LinearEquiv.symm (CoextendScalars.equiv f ((restrictScalars f).obj Y)) :
                      (a :
                          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                            (↑((restrictScalars f).obj Y) : Type u_1)) →
                        (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                    { toFun := fun (s : S) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑((restrictScalars f).obj Y) : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y) : Type u_1))
        t :
      (↑((restrictScalars f).obj Y) : Type u_1))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_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 : Ring R
inst_3 : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : (↑Y : Type (max u₂ u_1))
s : S
change :
  HSMul.hSMul (β := (↑Y' : Type (max u₂ u_1))) 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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
          y :
        (↑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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
      (s • y)
⊢ Eq (α := (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
              ((Hom.hom (↟(app' f Y')) ∘ₗ Hom.hom g :
                  (a : (↑Y : Type (max u₂ u_1))) →
                    (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
        s :
      (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
              ((Hom.hom ((coextendScalars f).map ((restrictScalars f).map g)) ∘ₗ Hom.hom (↟(app' f Y)) :
                  (a : (↑Y : Type (max u₂ u_1))) →
                    (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
        s :
      (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))

Tactic:
change s • (g y) = g (s • y)

Premises used: CategoryTheory.ConcreteCategory.hom, HSMul.hSMul, 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : (↑Y : Type (max u₂ u_1))
s : S
rw rw₁ :
  HSMul.hSMul (β := (↑Y' : Type (max u₂ u_1))) 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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
          y :
        (↑Y' : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑Y' : Type (max u₂ u_1))) 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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
          y :
        (↑Y' : Type (max u₂ u_1)))
⊢ HSMul.hSMul (β := (↑Y' : Type (max u₂ u_1))) 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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
          y :
        (↑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 : (↑Y : Type (max u₂ u_1))) → (↑Y' : Type (max u₂ u_1)))
      (s • y)

Tactic:
rw [map_smul]

Premises used: map_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 : Ring R
inst_3 : Ring S
f : R →+* S
X : ModuleCat R
x1 x2 : (↑((restrictScalars f).obj ((coextendScalars f).obj 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)))
            (x1 + x2) :
          (↑((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)))
      1 =
    HAdd.hAdd (α := (↑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)))
              x1 :
            (↑((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)))
        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)))
              x2 :
            (↑((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)))
        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 R
r : R
g : (↑((restrictScalars f).obj ((coextendScalars f).obj X)) : Type (max u₂ u_1))
dsimp :
  (((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)))
            (HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) 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)))
      1 =
    HSMul.hSMul (β := (↑X : Type (max u₂ u_1))) r
      ((((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)))
        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)))
            (r • 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)))
      1 =
    HSMul.hSMul (α := R) (β := (↑X : Type (max u₂ u_1))) ((RingHom.id R : (a : R) → R) r : R)
      ((((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)))
        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 : 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))
rw :
  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)))
⊢ (((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)))
            (HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) 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)))
      1 =
    HSMul.hSMul (β := (↑X : Type (max u₂ u_1))) r
      ((((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)))
        1)

Tactic:
rw [CoextendScalars.smul_apply, one_mul, ← map_smul]

Premises used: ModuleCat.CoextendScalars.smul_apply, one_mul, map_smul