awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
⊢ (restrictScalars f).map α = (restrictScalars f).map β
have a : Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)
have a : ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑M : Type u_1)),
  Eq (α := (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map α) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (x ⊗ₜ[R] y) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map β) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (x ⊗ₜ[R] y) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
⊢ Eq (α := (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map α) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
    ((Hom.hom ((restrictScalars f).map β) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑M : Type u_1)) →
            (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑((restrictScalars f).obj N) : Type (max u_1 u₂)))
have a : Eq (α := (↑N : Type (max u_1 u₂)))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
          (CC := carrier) α :
        (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
      (s ⊗ₜ[R] m) :
    (↑N : Type (max u_1 u₂)))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
          (CC := carrier) β :
        (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
      (s ⊗ₜ[R] m) :
    (↑N : Type (max u_1 u₂)))
Tactic: change α (s ⊗ₜ m) = β (s ⊗ₜ m)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
⊢ s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)
have rw : Eq (α := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) (s ⊗ₜ[R] m) ((s * 1) ⊗ₜ[R] m)
Tactic: rw [ExtendScalars.smul_tmul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
rw : Eq (α := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) (s ⊗ₜ[R] m) ((s * 1) ⊗ₜ[R] m)
⊢ s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)
have rw₁ : Eq (α := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) (s ⊗ₜ[R] m) (s ⊗ₜ[R] m)
Tactic: rw [ExtendScalars.smul_tmul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (hypothesis)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat.{u_1, u₁} R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h :
  ∀ (m : (↑M : Type u_1)),
    Eq (α := (↑N : 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) α :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : 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) β :
            (a : (↑((extendScalars f).obj M) : Type (max u₂ u_1))) → (↑N : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] m) :
        (↑N : Type (max u₂ u_1)))
this : Algebra R S := f.toAlgebra
s : S
m : (↑M : Type u_1)
⊢ Eq (α := (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) α :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u_1 u₂)) →ₗ[S] (↑x2 : Type (max u_1 u₂)))
            (CC := carrier) β :
          (a : (↑((extendScalars f).obj M) : Type (max u_1 u₂))) → (↑N : Type (max u_1 u₂)))
        (s ⊗ₜ[R] m) :
      (↑N : Type (max u_1 u₂)))
have this₁ : s ⊗ₜ[R] m = HSMul.hSMul (β := TensorProduct.{u₁, u₂, u_1} R S (↑M : Type u_1)) s (1 ⊗ₜ[R] m)
Tactic: have : s ⊗ₜ[R] (m : M) = s • (1 : S) ⊗ₜ[R] m := by
    rw [ExtendScalars.smul_tmul, mul_one]
-- 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
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
⊢ (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)
have 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)
Tactic: rw [add_mul, 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 : 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)
⊢ (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)
have 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)
Tactic: rw [add_mul, 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 : 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)
⊢ Hom.hom g ∘ₗ (s • h) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S) (Hom.hom g ∘ₗ h)
have 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))
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.{u_1, u₁} R
⊢ CoextendScalars.map' f (𝟙 x) = 𝟙 (CoextendScalars.obj' f x)
have 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)))
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 Y Z : ModuleCat.{u_1, u₁} R
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ CoextendScalars.map' f (x ≫ x_1) = CoextendScalars.map' f x ≫ CoextendScalars.map' f x_1
have 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)))
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 R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
r : R
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)))
      ((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)))
have 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)))
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
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y : (↑Y : Type (max u₂ u_1))
r : R
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)))
      ((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)))
have 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)))
Tactic: rw [← g.hom.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
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)))
        ((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)))
have 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)))
Tactic: erw [smul_eq_mul]
-- 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
Y : ModuleCat.{u_1, u₂} S
y : (↑Y : Type u_1)
r : R
s : S
⊢ (r • s) • y = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)
have 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)
Tactic: erw [smul_eq_mul]
-- 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : (↑Y : Type (max u₂ u_1))
s : S
⊢ 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)))
have 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)
Tactic: change s • (g y) = g (s • y)
-- 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : (↑Y : Type (max u₂ u_1))
s : S
⊢ 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)
have 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)))
Tactic: rw [map_smul]