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
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
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' := ⋯, 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)))
⊢ { 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)) }

Tactic:
ext y
-- 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
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 : HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) s • y = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)
⊢ 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)))

Tactic:
change (f r • s) • y = (f r) • s • y

Premises used: HSMul.hSMul, 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
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)
h₁ h₂ : 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 = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (s • y)

Tactic:
rw [smul_eq_mul, mul_smul]

Premises used: smul_eq_mul, 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
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)
zero₁ : 0 = HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S) 0
zero₂ zero₃ : Eq (α := (↑Y : Type (max u₂ u_1))) 0 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)

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
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
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))
⊢ (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
        (s' ⊗ₜ[R] y)) =
    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)))
          (s' ⊗ₜ[R] y) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
Y : ModuleCat S
y : (↑Y : Type (max u₂ u_1))
change : HSMul.hSMul (α := S) 1 y = y
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) (X := (restrictScalars f ⋙ extendScalars f).obj Y) (map.{u₁, u₂, u_1} f) :
        (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] y) =
    y

Tactic:
change (1 : S) • y = y

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
Y : ModuleCat S
y : (↑Y : Type (max u₂ u_1))
⊢ HSMul.hSMul (α := S) 1 y = y

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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
hf :
  ∀ (z : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))),
    Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          z :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
              (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
                (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          z :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f =
    Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g

Tactic:
ext z
-- 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
hf :
  Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) 0
    (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
          (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
            (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
        (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
          (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
      0)
hf₁ hf₂ : Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) 0 0
⊢ Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
        (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
          (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
      0)
    (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
          (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
            (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
        (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
          (↑((𝟭 (ModuleCat S)).obj 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
hf :
  Eq (α := (↑Y' : Type (max u₂ v)))
    ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
          (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        (s' ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
            y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))
⊢ Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        (s' ⊗ₜ[R] y) :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
            (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
              (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        (s' ⊗ₜ[R] y) :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
hf :
  Eq (α := (↑Y' : Type (max u₂ v)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : S ⊗[R] (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        (s' ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
            y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))
⊢ Eq (α := (↑Y' : Type (max u₂ v)))
    ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
          (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        (s' ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
            y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))

Tactic:
erw [Counit.map_hom_apply]

Premises used: ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
hf :
  Eq (α := (↑Y' : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯ } :
                (a : S) → (↑Y' : Type (max u₂ v)) →ₗ[R] (↑Y' : Type (max u₂ v)))
              s') :
          (a : (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
          y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))
⊢ Eq (α := (↑Y' : Type (max u₂ v)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : S ⊗[R] (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        (s' ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
            y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))

Tactic:
rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]

Premises used: LinearMap.coe_mk, TensorProduct.lift.tmul
-- 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
hf :
  let s' := s';
  Eq (α := (↑Y' : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯ } :
                (a : S) → (↑Y' : Type (max u₂ v)) →ₗ[R] (↑Y' : Type (max u₂ v)))
              s') :
          (a : (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
          y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))
⊢ Eq (α := (↑Y' : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯ } :
                (a : S) → (↑Y' : Type (max u₂ v)) →ₗ[R] (↑Y' : Type (max u₂ v)))
              s') :
          (a : (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
          y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))

Tactic:
set s' : 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
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
s'_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
s' : S := s'_1
hf :
  HSMul.hSMul (β := (↑Y' : Type (max u₂ v))) s'
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
          y :
        (↑Y' : Type (max u₂ v))) =
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
          (CC := carrier) g :
        (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
      (s' • y)
⊢ Eq (α := (↑Y' : Type (max u₂ v)))
    ((LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
            (({
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯ } :
                (a : S) → (↑Y' : Type (max u₂ v)) →ₗ[R] (↑Y' : Type (max u₂ v)))
              s') :
          (a : (↑Y' : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
          y) :
      (↑Y' : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑Y : Type (max u₂ v))) → (↑Y' : Type (max u₂ v)))
        ((Hom.hom (Counit.map.{u₁, u₂, v} f) :
            (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (s' ⊗ₜ[R] y)) :
      (↑Y' : Type (max u₂ v)))

Tactic:
change s' • g y = g (s' • y)

Premises used: CategoryTheory.ConcreteCategory.hom, HSMul.hSMul, DFunLike.coe