awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
hf 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)))
⊢ 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:
rw [map_smul]

Premises used: map_smul
-- 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
x : (↑X : Type (max u₂ v))
dsimp :
  Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom
            ((ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f :
                (a : (extendScalars f).obj X ⟶ Y) → X ⟶ (restrictScalars f).obj Y)
              g) :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((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) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        ((Hom.hom (ExtendRestrictScalarsAdj.Unit.map.{u₁, u₂, v} f) :
            (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ v)))
          x) :
      (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom
            ((ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f :
                (a : (extendScalars f).obj X ⟶ Y) → X ⟶ (restrictScalars f).obj Y)
              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 ((ExtendRestrictScalarsAdj.unit.{v, u₁, u₂} f).app X ≫ (restrictScalars f).map 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:
dsimp
-- 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
x : (↑X : Type (max u₂ v))
⊢ Eq (α := (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
    ((Hom.hom
            ((ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f :
                (a : (extendScalars f).obj X ⟶ Y) → X ⟶ (restrictScalars f).obj Y)
              g) :
          (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
        x :
      (↑((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) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        ((Hom.hom (ExtendRestrictScalarsAdj.Unit.map.{u₁, u₂, v} f) :
            (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj ((extendScalars f).obj X)) : Type (max u₂ v)))
          x) :
      (↑Y : Type (max u₂ v)))

Tactic:
rfl
-- 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 : X ⟶ (restrictScalars f).obj Y
zero :
  Eq (α := (↑Y : Type (max u₂ v))) 0
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      0)
zero₁ zero₂ : Eq (α := (↑Y : Type (max u₂ v))) 0 0
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
          ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
              (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
            g) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      0)
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
      0)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- 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 : X ⟶ (restrictScalars f).obj Y
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑X : Type (max v u₂))
tmul :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.Counit.map.{u₁, u₂, v} f) :
          (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
            y) :
      (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))

Tactic:
dsimp
-- 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 : X ⟶ (restrictScalars f).obj Y
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑X : Type (max v u₂))
tmul :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑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)))
        (x ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
            y) :
      (↑Y : Type (max u₂ v)))
tmul₁ tmul₂ :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((lift
            {
              toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g,
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))
    ((lift
            {
              toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦
                ExtendRestrictScalarsAdj.HomEquiv.evalAt f s g,
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars.{u₁, u₂, v} f g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R] y) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom (ExtendRestrictScalarsAdj.Counit.map.{u₁, u₂, v} f) :
          (a : (↑((extendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x ⊗ₜ[R]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v))) (CC := carrier) g :
              (a : (↑X : Type (max u₂ v))) → (↑((restrictScalars f).obj Y) : Type (max u₂ v)))
            y) :
      (↑Y : Type (max u₂ v)))

Tactic:
erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply]

Premises used: ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply
-- 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 : X ⟶ (restrictScalars f).obj Y
x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))
h :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
h_1 :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v)))
⊢ HAdd.hAdd (α := (↑Y : Type (max u₂ v))) (β := (↑Y : Type (max u₂ v)))
      ((Hom.hom
              ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                  (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                g) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          x :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom
              ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                  (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
                g) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          y :
        (↑Y : Type (max u₂ v))) =
    HAdd.hAdd (α := (↑Y : Type (max u₂ v))) (β := (↑Y : Type (max u₂ v)))
      ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          x :
        (↑Y : Type (max u₂ v)))
      ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
          y :
        (↑Y : Type (max u₂ v)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
φ : (extendScalars f).obj M ⟶ N
m : (↑M : Type (max u₂ v))
⊢ Eq (α := (↑((restrictScalars f).obj N) : Type (max u₂ v)))
    ((@ConcreteCategory.hom _ (moduleCategory R)
            (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v))) carrier
            (fun (X Y : ModuleCat R) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u₂ v)) →ₗ[R] (↑Y : Type (max u₂ v))) (↑X : Type (max u₂ v))
                  (↑Y : Type (max u₂ v))))
            _ M _
            (((extendRestrictScalarsAdj.{v, u₁, u₂} f).homEquiv M N :
                  (a : (extendScalars f).obj M ⟶ N) → M ⟶ (restrictScalars f).obj N)
                φ :
              M ⟶ (restrictScalars f).obj N) :
          (a : (↑M : Type (max u₂ v))) → (↑((restrictScalars f).obj N) : Type (max u₂ v)))
        m :
      (↑((restrictScalars f).obj N) : 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) φ :
          (a : (↑((extendScalars f).obj M) : Type (max u₂ v))) → (↑N : Type (max u₂ v)))
        (1 ⊗ₜ[R] m) :
      (↑N : Type (max u₂ v)))

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat R
m : (↑M : Type (max u₂ v))
⊢ Eq (α := (↑((extendScalars f ⋙ restrictScalars f).obj M) : Type (max u₂ v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u₂ v)) →ₗ[R] (↑x2 : Type (max u₂ v)))
            (CC := carrier) ((extendRestrictScalarsAdj.{v, u₁, u₂} f).unit.app M) :
          (a : (↑((𝟭 (ModuleCat R)).obj M) : Type (max u₂ v))) →
            (↑((extendScalars f ⋙ restrictScalars f).obj M) : Type (max u₂ v)))
        m :
      (↑((extendScalars f ⋙ restrictScalars f).obj M) : Type (max u₂ v)))
    (1 ⊗ₜ[R] m : S ⊗[R] (↑M : Type (max u₂ v)))

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat S
m : (↑M : 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) ((extendRestrictScalarsAdj.{u_1, u₁, u₂} f).counit.app M) :
        (a : (↑((extendScalars f).obj ((restrictScalars f).obj M)) : Type (max u₂ u_1))) → (↑M : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] m) =
    m

Tactic:
apply ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul

Premises used: ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul
-- 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
⊢ (extendScalars f).IsLeftAdjoint

Tactic:
(extendRestrictScalarsAdj f).isLeftAdjoint

Premises used: ModuleCat.extendRestrictScalarsAdj, CategoryTheory.Adjunction.isLeftAdjoint
-- 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
⊢ (restrictScalars f).IsRightAdjoint

Tactic:
(extendRestrictScalarsAdj f).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, ModuleCat.extendRestrictScalarsAdj
-- 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_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  Small.{v, max u_3 v}
    (↑(F ⋙
            forget (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦
              (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC := carrier)).sections :
      Type (max u_3 v))
c : Cone F
hc : IsLimit c
have :
  (hc' :
      IsLimit (F :=
        F ⋙
          forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦
            (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
            (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
        (Functor.mapCone
          (forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦
            (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
            (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier))
          c)) →
    IsLimit ((restrictScalars f).mapCone c)
⊢ IsLimit ((restrictScalars f).mapCone c)

Tactic:
have hc' := isLimitOfPreserves (forget₂ _ AddCommGrpCat) hc
-- 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_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  Small.{v, max u_3 v}
    (↑(F ⋙
            forget (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦
              (↑x1 : Type v) →ₗ[S] (↑x2 : Type v)) (CC := carrier)).sections :
      Type (max u_3 v))
c : Cone F
hc : IsLimit c
hc' :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      c)
⊢ IsLimit ((restrictScalars f).mapCone c)

Tactic:
exact isLimitOfReflects (forget₂ _ AddCommGrpCat) hc'

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.forget₂, AddCommGrpCat
-- 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_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
⊢ HasColimit
    ((F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))

Tactic:
have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat) :=
    inferInstanceAs (HasColimit (F ⋙ forget₂ _ AddCommGrpCat))
-- 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_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
this :
  HasColimit
    ((F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
apply : IsColimit ((restrictScalars f).mapCocone (HasColimit.colimitCocone F))
⊢ PreservesColimit F (restrictScalars f)

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (HasColimit.isColimitColimitCocone F)

Premises used: ModuleCat.HasColimit.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- 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_1
S : Type u_2
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
J : Type u_3
inst_4 : Category.{v_1, u_3} J
F : J ⥤ ModuleCat.{v, u_2} S
inst_5 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{v, u_2} S) (FC := fun (x1 x2 : ModuleCat.{v, u_2} S) ↦ (↑x1 : Type v) →ₗ[S] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
this :
  HasColimit
    ((F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
t :
  IsColimit (F :=
    (F ⋙ restrictScalars f) ⋙
      forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCocone
      (forget₂ (ModuleCat.{v, u_1} R) (FC := fun (x1 x2 : ModuleCat.{v, u_1} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      ((restrictScalars f).mapCocone (HasColimit.colimitCocone F)))
⊢ IsColimit ((restrictScalars f).mapCocone (HasColimit.colimitCocone F))

Tactic:
apply isColimitOfReflects (forget₂ (ModuleCat.{v} R) AddCommGrpCat)