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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
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 : S
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • z) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          z :
        (↑Y : Type (max u₂ u_1)))
have refine_3 : (lift
        { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
          map_smul' := sorry } :
      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
    (HSMul.hSMul (β := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) s 0) =
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
    ((lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := sorry,
            map_smul' := sorry :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
              (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑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' x => simp [mul_smul]
    | add _ _ ih1 ih2 => rw [smul_add, map_add, ih1, ih2, map_add, smul_add]
Cleared hypotheses: 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
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
⊢ HomEquiv.fromExtendScalars.{u₁, u₂, v} f (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g) = g
have hf : Hom.hom (HomEquiv.fromExtendScalars.{u₁, u₂, v} f (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g)) = Hom.hom g
Tactic: apply hom_ext
-- 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
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
⊢ Hom.hom (HomEquiv.fromExtendScalars.{u₁, u₂, v} f (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g)) = Hom.hom g
have hf : ∀ (x : (↑((extendScalars f).obj X) : 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 : 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)))
Tactic: apply LinearMap.ext
-- 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
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
⊢ 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)
have hf : Eq (α := (↑Y : Type (max u₂ v))) 0
  ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑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
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
hf :
  Eq (α := (↑Y : Type (max u₂ v))) 0
    ((Hom.hom g : (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v))) 0)
⊢ 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)
have hf₁ : Eq (α := (↑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
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
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)))
have hf : Eq (α := (↑Y : Type (max u₂ v)))
  (((({
                toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                  HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                map_add' := sorry, map_smul' := sorry } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
            x :
          (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
        (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
      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)))
Tactic: erw [TensorProduct.lift.tmul]
-- 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
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
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
s : (↑X : Type (max v u₂))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    (((({
                  toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                    HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              x :
            (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        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)))
have hf : ∀ (x : S),
  Eq (α := (↑Y : Type (max u₂ v)))
    (((({
                  toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                    HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                  map_add' := sorry } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              x :
            (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        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)))
Tactic: change S at x
Cleared hypotheses: x
-- 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
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
s : (↑X : Type (max v u₂))
x : S
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    (((({
                  toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                    HomEquiv.evalAt f s (HomEquiv.toRestrictScalars.{u₁, u₂, v} f g),
                  map_add' := ⋯ } :
                (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) →
                  (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v)))
              x :
            (↑X : Type (max v u₂)) →ₗ[R] (↑Y : Type (max u₂ v))) :
          (a : (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        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)))
have hf : HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[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)
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
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
s : (↑X : Type (max v u₂))
x : S
⊢ HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ v)) →ₗ[S] (↑x2 : Type (max u₂ v)))
              (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          (1 ⊗ₜ[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)
have hf : Eq (α := (↑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 : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
      (x ⊗ₜ[R] s) :
    (↑((restrictScalars f).obj 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)))
Tactic: erw [← map_smul, ExtendScalars.smul_tmul, mul_one x]
-- 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
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
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)))
have hf : HAdd.hAdd (α := (↑Y : Type (max u₂ v))) (β := (↑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 (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))) (x + y)
Tactic: rw [map_add, map_add, ih1, ih2]
-- 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
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))
⊢ 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)))
have 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)
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]
Cleared hypotheses: 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
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)
⊢ 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)))
have 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)))
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]
Cleared hypotheses: 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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj 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
⊢ HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) = g
have hf : ∀ (x : (↑X : Type (max u₂ v))),
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom (HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g)) :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
Tactic: ext x
-- 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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj 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
x : (↑X : Type (max u₂ v))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom (HomEquiv.toRestrictScalars.{u₁, u₂, v} f (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g)) :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
have hf : Eq (α := (↑((restrictScalars f).obj 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) (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      (1 ⊗ₜ[R] x) :
    (↑Y : Type (max u₂ v)))
  ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
    (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
Tactic: rw [HomEquiv.toRestrictScalars_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
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj 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
x : (↑X : Type (max u₂ v))
⊢ Eq (α := (↑((restrictScalars f).obj 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) (HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
      (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
have hf : Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
  ((lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ HomEquiv.evalAt f s g, map_add' := sorry,
            map_smul' := sorry } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
      (1 ⊗ₜ[R] x) :
    (↑Y : Type (max u₂ v)))
  ((Hom.hom g : (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v))) x :
    (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
Tactic: erw [HomEquiv.fromExtendScalars_hom_apply]