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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
s : S
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
x y : S
rw :
  (g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (x * s + y * s) =
    HAdd.hAdd (α := M) (β := M) ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (x * s) : M)
      ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (y * s) : M)
rw₁ rw₂ :
  HAdd.hAdd (α := M) (β := M) ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (x * s) : M)
      ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (y * s) : M) =
    HAdd.hAdd (α := M) (β := M) ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (x * s) : M)
      ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (y * s) : M)
⊢ (g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) ((x + y) * s) =
    HAdd.hAdd (α := M) (β := M) ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (x * s) : M)
      ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (y * s) : M)

Tactic:
rw [add_mul, map_add]

Premises used: add_mul, map_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 : Ring R
inst_3 : Ring S
f : R →+* S
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
s : S
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
r : R
t : S
⊢ (g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (r • t * s) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (t * s) : M)

Tactic:
simp [← map_smul, ModuleCat.restrictScalars.smul_def (M := ModuleCat.of _ S), mul_assoc]

Premises used: mul_assoc, ModuleCat.restrictScalars.smul_def, map_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
s : S
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
s' : S
⊢ Eq.{v + 1} (α := M) ((s • g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) s' : M)
    ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) (s' * s) : M)

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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
s t : S
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
x : S
⊢ Eq.{v + 1} (α := M) (((s * t) • g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)
    ((s • t • g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
s : S
⊢ Eq.{v + 1} (α := M) ((HSMul.hSMul (α := S) 1 g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) s : M)
    ((g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) s : M)

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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
x x_1 : S
⊢ Eq.{v + 1} (α := M)
    ((HSMul.hSMul (β := LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M) x
            0 :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M)
        x_1 :
      M)
    ((0 : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x_1 : M)

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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
s : S
g h : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
x : S
⊢ Eq.{v + 1} (α := M) ((s • (g + h) : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)
    ((s • g + s • h : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)

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
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
s1 s2 : S
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
x : S
⊢ Eq.{v + 1} (α := M) (((s1 + s2) • g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)
    ((s1 • g + s2 • g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)

Tactic:
simp [mul_add, map_add]

Premises used: map_add, mul_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 : Ring R
inst_3 : Ring S
f : R →+* S
M : Type v
inst_4 : AddCommMonoid M
inst_5 : Module R M
g : LinearMap.{u₁, u₁, u₂, v} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) M
x : S
⊢ Eq.{v + 1} (α := M) ((HSMul.hSMul (α := S) 0 g : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)
    ((0 : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → M) x : M)

Tactic:
simp [map_zero]

Premises used: map_zero
-- 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
M_1 : ModuleCat.{v, u₁} R
M M' : ModuleCat.{u_1, u₁} R
g : M ⟶ M'
s : S
h : LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type u_1)
h₁ :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)),
    Eq.{u_1 + 1} (α := (↑M' : Type u_1))
      ((Hom.hom g ∘ₗ (s • h) : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M' : Type u_1)) x :
        (↑M' : Type u_1))
      ((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (Hom.hom g ∘ₗ h) :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M' : Type u_1))
          x :
        (↑M' : Type u_1))
⊢ Hom.hom g ∘ₗ (s • h) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (Hom.hom g ∘ₗ h)

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
M_1 : ModuleCat.{v, u₁} R
M M' : ModuleCat.{u_1, u₁} R
g : M ⟶ M'
s : S
h : LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type u_1)
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
⊢ Eq.{u_1 + 1} (α := (↑M' : Type u_1))
    ((Hom.hom g ∘ₗ (s • h) : (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M' : Type u_1)) x :
      (↑M' : Type u_1))
    ((HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (Hom.hom g ∘ₗ h) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M' : Type u_1))
        x :
      (↑M' : Type u_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.{u_1, u₁} R
hf :
  ∀ (x_1 : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))),
    Eq (α := (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
      ((Hom.hom (CoextendScalars.map' f (𝟙 x)) :
            (a : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
          x_1 :
        (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
      ((Hom.hom (𝟙 (CoextendScalars.obj' f x)) :
            (a : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
          x_1 :
        (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
⊢ CoextendScalars.map' f (𝟙 x) = 𝟙 (CoextendScalars.obj' f x)

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.{u_1, u₁} R
x_1 : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))
⊢ Eq (α := (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
    ((Hom.hom (CoextendScalars.map' f (𝟙 x)) :
          (a : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
        x_1 :
      (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
    ((Hom.hom (𝟙 (CoextendScalars.obj' f x)) :
          (a : (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))
        x_1 :
      (↑(CoextendScalars.obj' f x) : Type (max u₂ u_1)))

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 : Ring R
inst_3 : Ring S
f : R →+* S
X Y Z : ModuleCat.{u_1, u₁} R
x : X ⟶ Y
x_1 : Y ⟶ Z
hf :
  ∀ (x_2 : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))),
    Eq (α := (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
      ((Hom.hom (CoextendScalars.map' f (x ≫ x_1)) :
            (a : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
          x_2 :
        (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
      ((Hom.hom (CoextendScalars.map' f x ≫ CoextendScalars.map' f x_1) :
            (a : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
          x_2 :
        (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
⊢ CoextendScalars.map' f (x ≫ x_1) = CoextendScalars.map' f x ≫ CoextendScalars.map' f x_1

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 Y Z : ModuleCat.{u_1, u₁} R
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))
⊢ Eq (α := (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
    ((Hom.hom (CoextendScalars.map' f (x ≫ x_1)) :
          (a : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
        x_2 :
      (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
    ((Hom.hom (CoextendScalars.map' f x ≫ CoextendScalars.map' f x_1) :
          (a : (↑(CoextendScalars.obj' f X) : Type (max u₂ u_1))) → (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))
        x_2 :
      (↑(CoextendScalars.obj' f Z) : Type (max u₂ u_1)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
g g' : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))
h :
  Eq (α := LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type u_1))
    ((equiv f M :
          (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M : Type u_1))
        g :
      LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type u_1))
    ((equiv f M :
          (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M : Type u_1))
        g' :
      LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂) (↑M : Type u_1))
⊢ g = g'

Tactic:
(CoextendScalars.equiv f M).injective h

Premises used: ModuleCat.CoextendScalars.equiv, LinearEquiv.injective
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
g : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))
s s' : S
⊢ Eq.{u_1 + 1} (α := (↑M : Type u_1))
    ((((equiv f M :
                (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M : Type u_1))
              (s • g) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑M : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M : Type u_1))
        s' :
      (↑M : Type u_1))
    ((((equiv f M :
                (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M : Type u_1))
              g :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑M : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M : Type u_1))
        (s' * s) :
      (↑M : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M M' : ModuleCat.{u_1, u₁} R
g : M ⟶ M'
x : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))
s : S
⊢ Eq.{u_1 + 1} (α := (↑M' : Type u_1))
    ((((equiv f M' :
                (a : (↑((coextendScalars f).obj M') : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M' : Type 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)
                    ((coextendScalars f).map g) :
                  (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
                    (↑((coextendScalars f).obj M') : Type (max u₂ u_1)))
                x) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑M' : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M' : Type u_1))
        s :
      (↑M' : 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 : (↑M : Type u_1)) → (↑M' : Type u_1))
        ((((equiv f M :
                    (a : (↑((coextendScalars f).obj M) : Type (max u₂ u_1))) →
                      (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑M : Type u_1))
                  x :
                LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
                  (↑M : Type u_1)) :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑M : Type u_1))
            s :
          (↑M : Type u_1)) :
      (↑M' : Type 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 : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
s1 s2 : 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)))
      ((s1 + s2) • y) =
    HAdd.hAdd (α := (↑X : Type (max u₂ u_1))) (β := (↑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)))
          (s1 • y) :
        (↑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)))
          (s2 • y) :
        (↑X : Type (max u₂ u_1)))

Tactic:
simp [add_smul]

Premises used: add_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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
r : R
s : S
dsimp :
  (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)))
      ((r • s) • y) =
    HSMul.hSMul (β := (↑X : Type (max u₂ u_1))) r
      ((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)))
⊢ (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)))
      ((r • s) • y) =
    HSMul.hSMul (α := R) (β := (↑X : Type (max u₂ u_1))) ((RingHom.id R : (a : R) → R) r : R)
      ((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:
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
r : R
s : S
rw :
  Eq (α := (↑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)))
        ((r • s) • y) :
      (↑X : Type (max u₂ u_1)))
    ((Hom.hom g : (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1))) (r • s • y) :
      (↑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)))
      ((r • s) • y) =
    HSMul.hSMul (β := (↑X : Type (max u₂ u_1))) r
      ((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:
rw [← g.hom.map_smul]

Premises used: LinearMap.map_smul, ModuleCat.Hom.hom
-- 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
y : (↑Y : Type (max u₂ u_1))
r : R
s : S
erw :
  Eq (α := (↑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)))
        (HMul.hMul (α := S) (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) r : S) s • y) :
      (↑X : Type (max u₂ u_1)))
    ((Hom.hom g : (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1))) (r • s • y) :
      (↑X : Type (max u₂ u_1)))
⊢ Eq (α := (↑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)))
        ((r • s) • y) :
      (↑X : Type (max u₂ u_1)))
    ((Hom.hom g : (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1))) (r • s • y) :
      (↑X : Type (max u₂ u_1)))

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
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
r : R
s : S
⊢ Eq (α := (↑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)))
        (HMul.hMul (α := S) (((↑f.toMonoidWithZeroHom : ZeroHom R S) : (a : R) → S) r : S) s • y) :
      (↑X : Type (max u₂ u_1)))
    ((Hom.hom g : (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1))) (r • s • y) :
      (↑X : Type (max u₂ u_1)))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul