awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{v, u₁} R
N : ModuleCat.{v, u₂} S
g : (↑M : Type v) →ₛₗ[f] (↑N : Type v)
⊢ ∀ (x y : (↑M : Type v)),
    (g : (a : (↑M : Type v)) → (↑N : Type v)) (x + y) =
      HAdd.hAdd (α := (↑((restrictScalars f).obj N) : Type v)) (β := (↑((restrictScalars f).obj N) : Type v))
        ((g : (a : (↑M : Type v)) → (↑N : Type v)) x : (↑N : Type v))
        ((g : (a : (↑M : Type v)) → (↑N : Type v)) y : (↑N : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{v, u₁} R
N : ModuleCat.{v, u₂} S
g : (↑M : Type v) →ₛₗ[f] (↑N : Type v)
⊢ ∀ (m : R) (x : (↑M : Type v)),
    (g : (a : (↑M : Type v)) → (↑N : Type v)) (m • x) =
      HSMul.hSMul (α := R) (β := (↑((restrictScalars f).obj N) : Type v)) ((RingHom.id R : (a : R) → R) m : R)
        ((g : (a : (↑M : Type v)) → (↑N : Type v)) x : (↑N : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
M : ModuleCat.{v, u₁} R
N : ModuleCat.{v, u₂} S
g : M ⟶ (restrictScalars f).obj N
⊢ ∀ (x y : (↑M : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑M : Type v)) → (↑((restrictScalars f).obj N) : Type v))
        (x + y) =
      HAdd.hAdd (α := (↑N : Type v)) (β := (↑N : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) g :
              (a : (↑M : Type v)) → (↑((restrictScalars f).obj N) : Type v))
            x :
          (↑((restrictScalars f).obj N) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u₁} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) g :
              (a : (↑M : Type v)) → (↑((restrictScalars f).obj N) : Type v))
            y :
          (↑((restrictScalars f).obj N) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
X : ModuleCat.{u_1, u₂} S
x : R
x_1 : (↑((restrictScalars f).obj X) : Type u_1)
subst :
  Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) x_1)
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) x_1)

Tactic:
subst e
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X : ModuleCat.{u_1, u₂} S
x : R
x_1 : (↑((restrictScalars f).obj X) : Type u_1)
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1))) x_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
X Y : ModuleCat.{u_1, u₂} S
x : X ⟶ Y
subst :
  (restrictScalars f).map x ≫
      Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars f).obj X) : Type u_1))))
          Y) =
    Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃ₗ[R] (↑((restrictScalars f).obj X) : Type u_1) }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars f).obj X) : Type u_1))))
          X) ≫
      (restrictScalars f).map x
⊢ (restrictScalars f).map x ≫
      Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars g).obj X) : Type u_1))))
          Y) =
    Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃ₗ[R] (↑((restrictScalars g).obj X) : Type u_1) }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars g).obj X) : Type u_1))))
          X) ≫
      (restrictScalars g).map x

Tactic:
subst e
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f : R →+* S
X Y : ModuleCat.{u_1, u₂} S
x : X ⟶ Y
⊢ (restrictScalars f).map x ≫
      Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars f).obj X) : Type u_1))))
          Y) =
    Iso.hom
        ((fun (X : ModuleCat.{u_1, u₂} S) ↦
            (LinearEquiv.toModuleIso
                (let __spread.0 :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃+ (↑((restrictScalars f).obj X) : Type u_1) :=
                  AddEquiv.refl (↑((restrictScalars f).obj X) : Type u_1);
                { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                  right_inv := ⋯ :
                  (↑((restrictScalars f).obj X) : Type u_1) ≃ₗ[R] (↑((restrictScalars f).obj X) : Type u_1) }) :
              Iso (C := ModuleCat.{u_1, u₁} R) (of R (↑((restrictScalars f).obj X) : Type u_1))
                (of R (↑((restrictScalars f).obj X) : Type u_1))))
          X) ≫
      (restrictScalars f).map x

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
⊢ (restrictScalarsCongr e).symm = restrictScalarsCongr ⋯

Tactic:
rfl

Premises used: ModuleCat.restrictScalarsCongr, CategoryTheory.Iso.symm, rfl, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
M : ModuleCat.{u_1, u₂} S
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ ((restrictScalarsCongr e).hom.app M) :
        (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑((restrictScalars g).obj M) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : Ring R
inst_1 : Ring S
f g : R →+* S
e : f = g
M : ModuleCat.{u_1, u₂} S
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ ((restrictScalarsCongr e).inv.app M) :
        (a : (↑((restrictScalars g).obj M) : Type u_1)) → (↑((restrictScalars f).obj M) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat.{u_1, u₁} R
⊢ (↑((restrictScalars f).obj M) : Type u_1) ≃+ (↑M : Type u_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat.{u_1, u₁} R
r : R
x : (↑((restrictScalars f).obj M) : Type u_1)
subst :
  ∀ (x : (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1)),
    (AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
          (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
        (r • x) =
      HSMul.hSMul (β := (↑M : Type u_1)) r
        ((AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
              (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
            x :
          (↑M : Type u_1))
⊢ (AddEquiv.refl (↑((restrictScalars f).obj M) : Type u_1) :
        (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑M : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑M : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars f).obj M) : Type u_1) :
            (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑M : Type u_1))
          x :
        (↑M : Type u_1))

Tactic:
subst hf
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
M : ModuleCat.{u_1, u₁} R
r : R
x : (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1)
⊢ (AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
        (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑M : Type u_1)) r
      ((AddEquiv.refl (↑(Functor.obj (restrictScalars (RingHom.id R)) M) : Type u_1) :
            (a : (↑((restrictScalars (RingHom.id R)).obj M) : Type u_1)) → (↑M : Type u_1))
          x :
        (↑M : Type u_1))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat.{u_1, u₁} R
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (restrictScalarsId'App f hf M).hom :
        (a : (↑((restrictScalars f).obj M) : Type u_1)) → (↑M : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M : ModuleCat.{u_1, u₁} R
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (restrictScalarsId'App f hf M).inv :
        (a : (↑M : Type u_1)) → (↑((restrictScalars f).obj M) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M N : ModuleCat.{u_1, u₁} R
φ : M ⟶ N
⊢ (restrictScalars f).map φ ≫ (restrictScalarsId'App f hf N).hom = (restrictScalarsId'App f hf M).hom ≫ φ

Tactic:
(restrictScalarsId' f hf).hom.naturality φ

Premises used: CategoryTheory.NatTrans.naturality, ModuleCat.restrictScalarsId', CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
inst : Ring R
f : R →+* R
hf : f = RingHom.id R
M N : ModuleCat.{u_1, u₁} R
φ : M ⟶ N
⊢ φ ≫ (restrictScalarsId'App f hf N).inv = (restrictScalarsId'App f hf M).inv ≫ (restrictScalars f).map φ

Tactic:
(restrictScalarsId' f hf).inv.naturality φ

Premises used: CategoryTheory.NatTrans.naturality, ModuleCat.restrictScalarsId', CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat.{u_1, u₃} R₃
⊢ (↑((restrictScalars gf).obj M) : Type u_1) ≃+ (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat.{u_1, u₃} R₃
r : R₁
x : (↑((restrictScalars gf).obj M) : Type u_1)
subst :
  ∀ (x : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)),
    (AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
          (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
            (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
        (r • x) =
      HSMul.hSMul (β := (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) r
        ((AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
              (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
                (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
            x :
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
⊢ (AddEquiv.refl (↑((restrictScalars gf).obj M) : Type u_1) :
        (a : (↑((restrictScalars gf).obj M) : Type u_1)) →
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars gf).obj M) : Type u_1) :
            (a : (↑((restrictScalars gf).obj M) : Type u_1)) →
              (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
          x :
        (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))

Tactic:
subst hgf
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
M : ModuleCat.{u_1, u₃} R₃
r : R₁
x : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)
⊢ (AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
        (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
      (r • x) =
    HSMul.hSMul (β := (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) r
      ((AddEquiv.refl (↑((restrictScalars (g.comp f)).obj M) : Type u_1) :
            (a : (↑((restrictScalars (g.comp f)).obj M) : Type u_1)) →
              (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
          x :
        (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat.{u_1, u₃} R₃
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R₁)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R₁) ↦ (↑x1 : Type u_1) →ₗ[R₁] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R₁) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R₁] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (restrictScalarsComp'App f g gf hgf M).hom :
        (a : (↑((restrictScalars gf).obj M) : Type u_1)) →
          (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M : ModuleCat.{u_1, u₃} R₃
x : (↑M : Type u_1)
⊢ (@ConcreteCategory.hom _ (moduleCategory R₁)
          (fun (x1 x2 : ModuleCat.{u_1, u₁} R₁) ↦ (↑x1 : Type u_1) →ₗ[R₁] (↑x2 : Type u_1)) carrier
          (fun (X Y : ModuleCat.{u_1, u₁} R₁) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type u_1) →ₗ[R₁] (↑Y : Type u_1)) (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (restrictScalarsComp'App f g gf hgf M).inv :
        (a : (↑((restrictScalars f).obj ((restrictScalars g).obj M)) : Type u_1)) →
          (↑((restrictScalars gf).obj M) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M N : ModuleCat.{u_1, u₃} R₃
φ : M ⟶ N
⊢ (restrictScalars gf).map φ ≫ (restrictScalarsComp'App f g gf hgf N).hom =
    (restrictScalarsComp'App f g gf hgf M).hom ≫ (restrictScalars f).map ((restrictScalars g).map φ)

Tactic:
(restrictScalarsComp' f g gf hgf).hom.naturality φ

Premises used: ModuleCat.RestrictScalars.obj', ModuleCat.restrictScalarsComp', CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₁ : Type u₁
R₂ : Type u₂
R₃ : Type u₃
inst : Ring R₁
inst_1 : Ring R₂
inst_2 : Ring R₃
f : R₁ →+* R₂
g : R₂ →+* R₃
gf : R₁ →+* R₃
hgf : gf = g.comp f
M N : ModuleCat.{u_1, u₃} R₃
φ : M ⟶ N
⊢ (restrictScalars f).map ((restrictScalars g).map φ) ≫ (restrictScalarsComp'App f g gf hgf N).inv =
    (restrictScalarsComp'App f g gf hgf M).inv ≫ (restrictScalars gf).map φ

Tactic:
(restrictScalarsComp' f g gf hgf).inv.naturality φ

Premises used: ModuleCat.RestrictScalars.obj', ModuleCat.restrictScalarsComp', CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
e : R ≃+* S
⊢ (restrictScalars e.toRingHom).IsEquivalence

Tactic:
(restrictScalarsEquivalenceOfRingEquiv e).isEquivalence_functor

Premises used: ModuleCat.restrictScalarsEquivalenceOfRingEquiv, ModuleCat.restrictScalars, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R S : Type v
inst : Ring R
inst_1 : Ring S
e : R ≃+* S
this : Module R (↑(of S S) : Type v) := e.toRingHom.toModule
x : R
y : (↑(of S S) : Type v)
⊢ e.symm.toFun (x • y) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (e.symm.toFun y)

Tactic:
simp [RingHom.toModule_smul]

Premises used: RingHom.toModule_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R S : Type v
inst : Ring R
inst_1 : Ring S
e : R ≃+* S
x : S
⊢ Eq (α := R)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
            (restrictScalarsIsoOfEquiv e).hom :
          (a : (↑((restrictScalars (↑e : R →+* S)).obj (of S S)) : Type v)) → R)
        x :
      R)
    ((e.symm : (a : S) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R S : Type v
inst : Ring R
inst_1 : Ring S
e : R ≃+* S
x : R
⊢ Eq (α := (↑(Functor.obj (C := ModuleCat S) (restrictScalars (↑e : R →+* S)) (of S S)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
            (restrictScalarsIsoOfEquiv e).inv :
          (a : R) → (↑((restrictScalars (↑e : R →+* S)).obj (of S S)) : Type v))
        x :
      (↑(Functor.obj (C := ModuleCat S) (restrictScalars (↑e : R →+* S)) (of S S)) : Type v))
    ((e : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Ring S
inst_3 : Algebra R₀ R
inst_4 : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat.{u_4, u_3} S
g : M ⟶ N
r₀ : R₀
hf :
  ∀ (m : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)),
    Eq (α := (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
      ((Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g)) :
            (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
              (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
          m :
        (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
      ((Hom.hom (r₀ • (restrictScalars f.toRingHom).map g) :
            (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
              (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
          m :
        (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
⊢ (restrictScalars f.toRingHom).map (r₀ • g) = r₀ • (restrictScalars f.toRingHom).map g

Tactic:
ext m
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R₀
inst_1 : Ring R
inst_2 : Ring S
inst_3 : Algebra R₀ R
inst_4 : Algebra R₀ S
f : R →ₐ[R₀] S
M N : ModuleCat.{u_4, u_3} S
g : M ⟶ N
r₀ : R₀
m : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)
⊢ Eq (α := (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom ((restrictScalars f.toRingHom).map (r₀ • g)) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
    ((Hom.hom (r₀ • (restrictScalars f.toRingHom).map g) :
          (a : (↑((restrictScalars f.toRingHom).obj M) : Type u_4)) →
            (↑((restrictScalars f.toRingHom).obj N) : Type u_4))
        m :
      (↑((restrictScalars f.toRingHom).obj N) : Type u_4))

Tactic:
congr_arg (· • g.hom m) (f.commutes r₀).symm

Premises used: congr_arg, AlgHom.commutes, HSMul.hSMul, Eq.symm, ModuleCat.Hom.hom, DFunLike.coe