awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (((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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (((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)
have 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)))
Tactic: rw [CoextendScalars.smul_apply, one_mul, ← map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ 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)))
have h : (f : (a : R) → S) r = HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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 (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1
have h : (f : (a : R) → S) r = HSMul.hSMul (α := S) (β := S) ((f : (a : R) → S) r : S) 1
Tactic: change f r = f r • (1 : S)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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
⊢ RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f
      (RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f g) =
    g
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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
⊢ RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁, u₂, v} f
      (RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁, u₂, v} f g) =
    g
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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
⊢ (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
have 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 := sorry,
                    right_inv := sorry } :
                (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: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (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)))
have rw : (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)))
    (HAdd.hAdd (α := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) (1 ⊗ₜ[R] x)
      (1 ⊗ₜ[R] 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: rw [tmul_add, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (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)))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (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)))
have 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)))
Tactic: rw [RestrictScalars.smul_def, ← LinearMap.map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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)))
        (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)))
have 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)))
Tactic: erw [tmul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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.{u_1, u₁} R
Y : ModuleCat.{u_1, u₂} S
s : S
g : X ⟶ (restrictScalars f).obj Y
x y : (↑X : Type u_1)
⊢ HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          (x + y) :
        (↑((restrictScalars f).obj Y) : Type u_1)) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                (CC := carrier) g :
              (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
            x :
          (↑((restrictScalars f).obj Y) : Type u_1)) +
      HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                (CC := carrier) g :
              (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
            y :
          (↑((restrictScalars f).obj Y) : Type u_1))
have rw : s •
    HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type u_1)) (β := (↑((restrictScalars f).obj Y) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          x :
        (↑((restrictScalars f).obj Y) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          y :
        (↑((restrictScalars f).obj Y) : Type u_1)) =
  HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          x :
        (↑((restrictScalars f).obj Y) : Type u_1)) +
    HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          y :
        (↑((restrictScalars f).obj Y) : Type u_1))
Tactic: rw [map_add, smul_add]