-- 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
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
z : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))
hf :
  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)
hf₁ :
  ∀ (s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑((restrictScalars 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)))
          (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)))
⊢ 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)))
have hf₂ : ∀ (x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
  (ih₁ :
    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)))
          x :
        (↑(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)))
          x :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))))
  (ih₂ :
    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)))
          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)))
          y :
        (↑(Functor.obj (𝟭 (ModuleCat S)) 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)))
        (x + 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)))
        (x + y) :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
Tactic: induction z using TensorProduct.induction_on with
    | zero => rw [map_zero, map_zero]
    | tmul s' y =>
      dsimp
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [Counit.map_hom_apply]
      rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
      set s' : S := s'
      change s' • g y = g (s' • y)
      rw [map_smul]
    | add _ _ ih₁ ih₂ => rw [map_add, map_add]; congr 1
Cleared hypotheses: z