awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
⊢ (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)
have zero₂ : Eq (α := (↑Y : Type (max u₂ u_1))) 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- 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 : ModuleCat S
s : S
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))
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
⊢ (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)))
      (s • z) =
    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)))
          z :
        (↑Y : Type (max u₂ u_1)))
have zero : (lift
        { toFun := fun (s : S) ↦ { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry },
          map_add' := sorry, map_smul' := sorry } :
      (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' := sorry, map_smul' := sorry :
                (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
            map_add' := sorry, map_smul' := sorry : 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: induction z using TensorProduct.induction_on with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s' y => simp [mul_smul]
      | add _ _ ih1 ih2 => rw [smul_add, map_add, map_add, ih1, ih2, smul_add]
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
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))
⊢ (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
have change : HSMul.hSMul (α := S) 1 y = y
Tactic: change (1 : S) • y = y
-- 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
⊢ (restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f =
    Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g
have 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)))
Tactic: ext z
-- 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
⊢ 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)
have 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)
Tactic: rw [map_zero, map_zero]
-- 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
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)
⊢ 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)
have hf₁ : Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) 0 0
Tactic: rw [map_zero, map_zero]
-- 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
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)))
have 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)))
Tactic: dsimp
-- 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
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj 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)))
have hf : Eq (α := (↑Y' : Type (max u₂ v)))
  ((lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y' : Type (max u₂ v))) ↦ s • y, map_add' := sorry, map_smul' := sorry },
            map_add' := sorry, map_smul' := sorry } :
        (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: erw [Counit.map_hom_apply]
-- 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
s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj 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)))
have 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' := sorry, map_smul' := sorry },
                map_add' := sorry } :
              (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: rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
-- 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
s'_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
s' : S := s'_1
⊢ 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)))
have 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)
Tactic: change s' • g y = g (s' • y)
-- 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
s'_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑((restrictScalars f).obj Y) : Type (max u₂ v))
s' : S := s'_1
⊢ 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)
have 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))) =
  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)))
Tactic: rw [map_smul]
-- 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))
⊢ 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 : 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: 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