-- 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
z : (↑((extendScalars f).obj X) : Type (max u₂ v))
hf :
  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)
hf₁ :
  ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (s : (↑X : Type (max v u₂))),
    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)))
hf₂ :
  ∀ (x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂)))
    (ih1 :
      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))))
    (ih2 :
      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)))
            y :
          (↑Y : Type (max u₂ v)))
        ((Hom.hom g : (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 (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) :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom g : (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 (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)))
        z :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) z :
      (↑Y : Type (max u₂ v)))

Tactic:
induction z using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero]
    | tmul x s =>
      erw [TensorProduct.lift.tmul]
      simp only [LinearMap.coe_mk]
      change S at x
      dsimp
      erw [← map_smul, ExtendScalars.smul_tmul, mul_one x]
      rfl
    | add _ _ ih1 ih2 => rw [map_add, map_add, ih1, ih2]

Premises used: LinearMap.coe_mk, map_zero, map_add, TensorProduct.lift.tmul, ModuleCat.ExtendScalars.smul_tmul, TensorProduct.tmul, map_smul