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.{u_1, u₁} R
Y : ModuleCat.{u_1, u₂} S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : (↑X : Type u_1)
⊢ AddHom.toFun
      {
        toFun := fun (x : (↑X : Type u_1)) ↦
          HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                    (CC := carrier) g :
                  (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                x :
              (↑((restrictScalars f).obj Y) : Type u_1)),
        map_add' := ⋯ }
      (r • x) =
    HSMul.hSMul (α := R) (β := (↑Y : Type u_1)) ((RingHom.id R : (a : R) → R) r : R)
      (AddHom.toFun
        {
          toFun := fun (x : (↑X : Type u_1)) ↦
            HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦
                      (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) g :
                    (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                  x :
                (↑((restrictScalars f).obj Y) : Type u_1)),
          map_add' := ⋯ : (↑X : Type u_1) →ₙ+ (↑Y : Type u_1) }
        x)
have rw : ({
        toFun := fun (x : (↑X : Type u_1)) ↦
          HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                    (CC := carrier) g :
                  (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                x :
              (↑((restrictScalars f).obj Y) : Type u_1)),
        map_add' := sorry } :
      (a : (↑X : Type u_1)) → (↑Y : Type u_1))
    (r • x) =
  HSMul.hSMul (α := R) (β := (↑Y : Type u_1)) ((RingHom.id R : (a : R) → R) r : R)
    (({
            toFun := fun (x : (↑X : Type u_1)) ↦
              HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
                ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦
                        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) g :
                      (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                    x :
                  (↑((restrictScalars f).obj Y) : Type u_1)),
            map_add' := sorry : (↑X : Type u_1) →ₙ+ (↑Y : Type u_1) } :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))
        x :
      (↑Y : Type u_1))
Tactic: rw [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply, map_smul, smul_comm r s (g x : 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
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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
⊢ (extendScalars f).obj X ⟶ Y
have refine_1 : (z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1))
Tactic: refine ofHom
    { toFun z := TensorProduct.lift (σ₁₂ := .id _) ?_ z, map_add' := ?_, map_smul' := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
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
refine_1 :
  (z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
    (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1))
⊢ (extendScalars f).obj X ⟶ Y
have refine_2 : ∀ (x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))),
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
            map_smul' := sorry } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (x + y) =
    HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
                map_smul' := sorry :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          x :
        (↑Y : Type (max u₂ u_1)))
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
                map_smul' := sorry :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          y :
        (↑Y : Type (max u₂ u_1)))
Tactic: refine ofHom
    { toFun z := TensorProduct.lift (σ₁₂ := .id _) ?_ z, map_add' := ?_, map_smul' := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
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
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
⊢ (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1))
have refine_1 : ∀ (s₁ s₂ : S), evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g
Tactic: refine
    { toFun s := HomEquiv.evalAt f s g, map_add' := fun (s₁ s₂ : S) ↦ ?_,
      map_smul' := fun (r : R) (s : S) ↦ ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
refine_1 : ∀ (s₁ s₂ : S), evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g
⊢ (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1))
have refine_1₁ : ∀ (r : R) (s : S), evalAt f (r • s) g = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (evalAt f s g)
Tactic: refine
    { toFun s := HomEquiv.evalAt f s g, map_add' := fun (s₁ s₂ : S) ↦ ?_,
      map_smul' := fun (r : R) (s : S) ↦ ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g
have refine_1 : ∀ (x : (↑X : Type (max u₂ u_1))),
  Eq (α := (↑Y : Type (max u₂ u_1)))
    ((evalAt f (s₁ + s₂) g : (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1))) x : (↑Y : Type (max u₂ u_1)))
    ((evalAt f s₁ g + evalAt f s₂ g : (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1))) x :
      (↑Y : 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 : 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
s₁ s₂ : S
x : (↑X : Type (max u₂ u_1))
⊢ Eq (α := (↑Y : Type (max u₂ u_1)))
    ((evalAt f (s₁ + s₂) g : (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1))) x : (↑Y : Type (max u₂ u_1)))
    ((evalAt f s₁ g + evalAt f s₂ g : (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1))) x :
      (↑Y : Type (max u₂ u_1)))
have refine_1 : HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) =
  HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) 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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) +
    HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) 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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
Tactic: dsimp only [m2, evalAt_apply, LinearMap.add_apply]
-- 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
s₁ s₂ : S
x : (↑X : Type (max u₂ u_1))
⊢ HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
          x :
        (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) 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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
            x :
          (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) +
      HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) 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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
            x :
          (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
have refine_1 : HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) =
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) (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 : (↑X : Type (max u₂ u_1))) → (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
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
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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
r : R
s : S
⊢ evalAt f (r • s) g = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (evalAt f s g)
have refine_1 : ∀ (x : (↑X : Type (max u₂ u_1))),
  Eq (α := (↑Y : Type (max u₂ u_1)))
    ((evalAt f (r • s) g : (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1))) x : (↑Y : Type (max u₂ u_1)))
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (evalAt f s g) :
          (a : (↑X : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        x :
      (↑Y : Type (max u₂ u_1)))
Tactic: ext x
-- 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • z) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          z :
        (↑Y : Type (max u₂ u_1)))
have refine_3 : (lift
        { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
          map_smul' := sorry } :
      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
    (s • z) =
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
    ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
              map_smul' := sorry :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        z :
      (↑Y : Type (max u₂ u_1)))
Tactic: change lift _ (s • z) = s • lift _ z
-- 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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        0)
have refine_3 : (lift
        { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
          map_smul' := sorry } :
      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
    0 =
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
    ((lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
            map_smul' := sorry :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
              (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑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
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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
refine_3 :
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      0 =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        0)
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        0)
have refine_3₁ : 0 = HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s 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
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₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
refine_3 :
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      0 =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        0)
refine_3₁ : 0 = HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s 0
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
            { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
              map_smul' := ⋯ :
              (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
            (↑Y : Type (max u₂ u_1)))
        0)
have refine_3₂ : Eq (α := (↑Y : Type (max u₂ u_1))) 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]