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 : 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))
⊢ 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)))
have 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' := sorry } :
              (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: rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
-- 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 : 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))
⊢ 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)))
have 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
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 : 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))
⊢ 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
have 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)))
Tactic: rw [one_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
x x' : (↑X : Type (max u₂ u_1))
⊢ 1 ⊗ₜ[R] (x + x') =
    HAdd.hAdd (α := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x')
have 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')
Tactic: rw [TensorProduct.tmul_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
r : R
x : (↑X : Type (max u₂ u_1))
m1 : Module R S := Module.compHom S f
⊢ 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)
have dsimp : 1 ⊗ₜ[R] (r • x) =
  HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)
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
r : R
x : (↑X : Type (max u₂ u_1))
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)
have 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)
Tactic: rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']
-- 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
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)
⊢ 1 ⊗ₜ[R] (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ u_1))) r (1 ⊗ₜ[R] x)
have 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)
Tactic: rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']
-- 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
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))
⊢ s • r • y = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (s • y)
have change : s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: change s • f r • y = f r • 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 : 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))
⊢ s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
have rw : HMul.hMul (β := S) 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]
-- 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
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)
⊢ s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
have rw₁ : HMul.hMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: rw [← mul_smul, mul_comm, mul_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
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)
⊢ s • HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
have rw₂ : HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: rw [← mul_smul, mul_comm, mul_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
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
⊢ { 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)) }
have 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' := sorry, map_smul' := sorry } :
          (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' := sorry, map_smul' := sorry :
              (↑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' := sorry, map_smul' := sorry :
              (↑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: ext 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 : 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))
⊢ 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)))
have h : (s₁ + s₂) • y = s₁ • y + s₂ • y
Tactic: change (s₁ + s₂) • y = s₁ • y + 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 : 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))
⊢ (s₁ + s₂) • y = s₁ • y + s₂ • y
have h : s₁ • y + s₂ • y = s₁ • y + s₂ • y
Tactic: rw [add_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
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
r : R
s : S
⊢ { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (r • s) • y, map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
      ((RingHom.id R : (a : R) → R) r : R)
      { 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)) }
have h : ∀ (y : (↑Y : Type (max u₂ u_1))),
  Eq (α := (↑Y : Type (max u₂ u_1)))
    (({ toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (r • s) • y, map_add' := sorry, map_smul' := sorry } :
          (a : (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        y :
      (↑Y : Type (max u₂ u_1)))
    ((HSMul.hSMul (α := R) (β := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
            ((RingHom.id R : (a : R) → R) r : R)
            { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry :
              (↑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: ext 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 : 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
r : R
s : S
y : (↑Y : Type (max u₂ u_1))
⊢ Eq (α := (↑Y : Type (max u₂ u_1)))
    (({ toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ (r • 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)))
    ((HSMul.hSMul (α := R) (β := (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)))
            ((RingHom.id R : (a : R) → R) r : R)
            { 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)))
have h : HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: change (f r • s) • y = (f r) • 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 : 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
r : R
s : S
y : (↑Y : Type (max u₂ u_1))
⊢ HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
have h : HMul.hMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: rw [smul_eq_mul, mul_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
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
r : R
s : S
y : (↑Y : Type (max u₂ u_1))
h : HMul.hMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
⊢ HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
have h₁ : HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
Tactic: rw [smul_eq_mul, mul_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
Y : ModuleCat S
s : 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
⊢ (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β :=
        (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
            {
              toFun := fun (s : S) ↦
                { 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)) },
              map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        0)
have zero : (lift
        { toFun := fun (s : S) ↦ { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry },
          map_add' := sorry, map_smul' := sorry } :
      (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
    0 =
  HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
    ((lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry :
                (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
            map_add' := sorry, map_smul' := sorry : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      0)
Tactic: rw [smul_zero, map_zero, smul_zero]
-- 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
Y : ModuleCat S
s : 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
zero :
  (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      0 =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
            {
              toFun := fun (s : S) ↦
                { 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)) },
              map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        0)
⊢ (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β :=
        (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
            {
              toFun := fun (s : S) ↦
                { 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)) },
              map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        0)
have zero₁ : 0 = HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S) 0
Tactic: rw [smul_zero, map_zero, smul_zero]