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 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
s : (↑X : Type (max v u₂))
hf :
  ∀ (x : S),
    Eq (α := (↑Y : Type (max u₂ v)))
      (((({
                    toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                      HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                    map_add' := ⋯ } :
                  (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                    (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
                x :
              (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
            (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
          s :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    (((({
                  toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                    HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              x :
            (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        s :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s) :
      (↑Y : Type (max u₂ v)))

Tactic:
change S at x
-- 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
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
s : (↑X : Type (max v u₂))
x : S
hf :
  HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (1 ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ v))) =
    (Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s)
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    (((({
                  toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                    HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              x :
            (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        s :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s) :
      (↑Y : Type (max u₂ v)))

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
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
s : (↑X : Type (max v u₂))
x : S
hf :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        (x ⊗ₜ[R] s) :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s) :
      (↑Y : Type (max u₂ v)))
⊢ HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (1 ⊗ₜ[R] s) :
        (↑Y : Type (max u₂ v))) =
    (Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s)

Tactic:
erw [← map_smul, ExtendScalars.smul_tmul, mul_one x]

Premises used: ModuleCat.ExtendScalars.smul_tmul, mul_one, 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
s : (↑X : Type (max v u₂))
x : S
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        (x ⊗ₜ[R] s) :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) (x ⊗ₜ[R] s) :
      (↑Y : Type (max u₂ v)))

Tactic:
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 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
hf :
  ∀ (x : (↑X : Type (max u₂ v))),
    Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
      ((Hom.hom (HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g)) :
            (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
      ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
⊢ HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) = g

Tactic:
ext x
-- 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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑X : Type (max u₂ v))
hf :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom (HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g)) :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))

Tactic:
rw [HomEquiv.toRestrictScalars_hom_apply]

Premises used: ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply
-- 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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑X : Type (max u₂ v))
hf :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ HomEquiv.evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))

Tactic:
erw [HomEquiv.fromExtendScalars_hom_apply]

Premises used: ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply
-- 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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑X : Type (max u₂ v))
hf :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({ toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ HomEquiv.evalAt f s g,
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              1) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ HomEquiv.evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))

Tactic:
rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]

Premises used: LinearMap.coe_mk, TensorProduct.lift.tmul
-- 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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑X : Type (max u₂ v))
hf :
  HSMul.hSMul (α := S) (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) 1
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ v))) =
    (Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({ toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ HomEquiv.evalAt f s g,
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              1) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))

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 : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
x : (↑X : Type (max u₂ v))
hf hf₁ :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v)))
            (CC := carrier) g :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
⊢ HSMul.hSMul (α := S) (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) 1
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ v))) =
    (Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x

Tactic:
rw [one_smul]

Premises used: one_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
x x' : (↑X : Type (max u₂ u_1))
rw rw₁ :
  HAdd.hAdd (α := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u₂ u_1))) (1 ⊗ₜ[R] x)
      (1 ⊗ₜ[R] x') =
    HAdd.hAdd (α := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x')
⊢ 1 ⊗ₜ[R] (x + x') =
    HAdd.hAdd (α := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x')

Tactic:
rw [TensorProduct.tmul_add]

Premises used: TensorProduct.tmul_add
-- 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
r : R
x : (↑X : Type (max u₂ u_1))
m1 : Module R S := Module.compHom S f
dsimp :
  1 ⊗ₜ[R] (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)
⊢ 1 ⊗ₜ[R] (r • x) =
    HSMul.hSMul (α := R) (β := (↑((extendScalars f ⋙ restrictScalars f).obj X) : Type (max u₂ u_1)))
      ((RingHom.id R : (a : R) → R) r : R) (1 ⊗ₜ[R] x)

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
r : R
x : (↑X : Type (max u₂ u_1))
m1 : Module R S := Module.compHom S f
rw :
  HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1 ⊗ₜ[R] x =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)
rw₁ rw₂ :
  Eq (α := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1)))
    (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1 ⊗ₜ[R] x)
    (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂)) r 1 ⊗ₜ[R] x)
⊢ 1 ⊗ₜ[R] (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)

Tactic:
rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul, TensorProduct.smul_tmul'
-- 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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
r : R
y : (↑Y : Type (max u₂ u_1))
change : s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
⊢ s • r • y = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)

Tactic:
change s • f r • y = f r • s • y

Premises used: 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
r : R
y : (↑Y : Type (max u₂ u_1))
rw : HMul.hMul (β := S) s ((f : (a : R) → S) r : S) • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
rw₁ : HMul.hMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
rw₂ rw₃ :
  HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
⊢ s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)

Tactic:
rw [← mul_smul, mul_comm, mul_smul]

Premises used: mul_comm, 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s₁ s₂ : S
h :
  ∀ (y : (↑Y : Type (max u₂ u_1))),
    Eq (α := (↑Y : Type (max u₂ u_1)))
      (({ toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (s₁ + s₂) • y, map_add' := ⋯, map_smul' := ⋯ } :
            (a : (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          y :
        (↑Y : Type (max u₂ u_1)))
      ((HAdd.hAdd (α := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₁ • y, map_add' := ⋯, map_smul' := ⋯ :
                (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) }
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₂ • y, map_add' := ⋯, map_smul' := ⋯ :
                (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          y :
        (↑Y : Type (max u₂ u_1)))
⊢ { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (s₁ + s₂) • y, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
      { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₁ • y, map_add' := ⋯, map_smul' := ⋯ :
        (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) }
      { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₂ • y, map_add' := ⋯, map_smul' := ⋯ :
        (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) }

Tactic:
ext y
-- 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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s₁ s₂ : S
y : (↑Y : Type (max u₂ u_1))
h : (s₁ + s₂) • y = s₁ • y + s₂ • y
⊢ Eq (α := (↑Y : Type (max u₂ u_1)))
    (({ toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (s₁ + s₂) • y, map_add' := ⋯, map_smul' := ⋯ } :
          (a : (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        y :
      (↑Y : Type (max u₂ u_1)))
    ((HAdd.hAdd (α := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
            { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₁ • y, map_add' := ⋯, map_smul' := ⋯ :
              (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) }
            { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s₂ • y, map_add' := ⋯, map_smul' := ⋯ :
              (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        y :
      (↑Y : Type (max u₂ u_1)))

Tactic:
change (s₁ + s₂) • y = s₁ • y + s₂ • y

Premises used: HAdd.hAdd
-- 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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s₁ s₂ : S
y : (↑Y : Type (max u₂ u_1))
h h₁ : s₁ • y + s₂ • y = s₁ • y + s₂ • y
⊢ (s₁ + s₂) • y = s₁ • y + s₂ • y

Tactic:
rw [add_smul]

Premises used: add_smul