-- 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
x : (↑((extendScalars f).obj X) : Type (max u₂ v))
zero :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
          ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
              (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
            g) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      0)
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      0)
tmul :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑X : Type (max v u₂))),
    Eq (α := (↑Y : Type (max u₂ v)))
      ((Hom.hom
              ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                  (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                g) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (x ⊗ₜ[R] y) :
        (↑Y : Type (max u₂ v)))
add :
  ∀ (x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))),
    Eq (α := (↑Y : Type (max u₂ v)))
        ((Hom.hom
                ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                    (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                  g) :
              (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
            x :
          (↑Y : Type (max u₂ v)))
        ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
              (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
            x :
          (↑Y : Type (max u₂ v))) →
      Eq (α := (↑Y : Type (max u₂ v)))
          ((Hom.hom
                  ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                      (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                    g) :
                (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
              y :
            (↑Y : Type (max u₂ v)))
          ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
                (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
              y :
            (↑Y : Type (max u₂ v))) →
        Eq (α := (↑Y : Type (max u₂ v)))
          ((Hom.hom
                  ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                      (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                    g) :
                (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
              (x + y) :
            (↑Y : Type (max u₂ v)))
          ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
                (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
              (x + y) :
            (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))

Tactic:
induction x using TensorProduct.induction_on with
        | zero => rw [map_zero, map_zero]
        | tmul =>
          rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
          dsimp
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
          erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply]
        | add => rw [map_add, map_add]; congr 1

Premises used: ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply, map_zero, map_add, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply, TensorProduct.tmul