awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat.{u_1, u₁} R
Y : ModuleCat.{u_1, u₂} S
s : S
g : X ⟶ (restrictScalars f).obj Y
x y : (↑X : Type u_1)
dsimp :
  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 + y) :
        (↑((restrictScalars f).obj Y) : 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)) +
      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))
            y :
          (↑((restrictScalars f).obj Y) : 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 + y) :
        (↑((restrictScalars f).obj Y) : 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)) +
      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))
            y :
          (↑((restrictScalars f).obj Y) : Type u_1))

Tactic:
dsimp only
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ 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
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)
⊢ (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1))

Tactic:
refine
    { toFun s := HomEquiv.evalAt f s g, map_add' := fun (s₁ s₂ : S) ↦ ?_,
      map_smul' := fun (r : R) (s : S) ↦ ?_ }
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ 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
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)))
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g

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 : 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))
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)))
⊢ 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:
dsimp only [m2, evalAt_apply, LinearMap.add_apply]

Premises used: LinearMap.add_apply, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ 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))
refine_1 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)))
⊢ 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:
rw [← 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 : 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
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)))
⊢ evalAt f (r • s) g = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (evalAt f s g)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ 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
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:
apply mul_smul (f r) s (g x)

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
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
⊢ ∀ (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' := ⋯,
              map_smul' := ⋯ } :
          (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' := ⋯,
                  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)))
            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' := ⋯,
                  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)))
            y :
          (↑Y : Type (max u₂ 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 : 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₂))
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)))
      (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' := ⋯,
                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)))
⊢ (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)))

Tactic:
change lift _ (s • z) = s • lift _ z

Premises used: HSMul.hSMul, TensorProduct.lift, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
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
refine_3₂ refine_3₃ : Eq (α := (↑Y : Type (max u₂ u_1))) 0 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)

Tactic:
rw [smul_zero, map_zero, smul_zero]

Premises used: smul_zero, 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 : 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
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
x : (↑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)))
      (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) s
        (s' ⊗ₜ[R] x)) =
    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)))
          (s' ⊗ₜ[R] x) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
hf : Hom.hom (HomEquiv.fromExtendScalars.{u₁, u₂, v} f (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g)) = Hom.hom g
⊢ HomEquiv.fromExtendScalars.{u₁, u₂, v} f (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g) = g

Tactic:
apply hom_ext

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

Tactic:
apply LinearMap.ext

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

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

Tactic:
erw [TensorProduct.lift.tmul]

Premises used: TensorProduct.lift.tmul