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 : (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)))
    ((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)))
have 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)))
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 : X ⟶ (restrictScalars f).obj Y
⊢ 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)
have 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)
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 : 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)
⊢ 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)
have zero₁ : 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 : X ⟶ (restrictScalars f).obj Y
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑X : Type (max v u₂))
⊢ 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)))
have 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)))
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 : X ⟶ (restrictScalars f).obj Y
x : (↑((restrictScalars f).obj (of S S)) : Type u₂)
y : (↑X : Type (max v u₂))
⊢ 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)))
have 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' := sorry, map_smul' := sorry },
            map_add' := sorry, map_smul' := sorry } :
        (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)))
Tactic: erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_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
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)))
⊢ 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)))
have 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' := sorry, map_smul' := sorry } :
        (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' := sorry, map_smul' := sorry } :
        (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)))
Tactic: erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_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
x : (↑((extendScalars f).obj X) : Type (max u₂ v))
⊢ 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)))
have zero : 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: induction x using TensorProduct.induction_on with
        | zero => rw [map_zero, map_zero]
        | tmul =>
          rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
          dsimp
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
          erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply]
        | add => rw [map_add, map_add]; congr 1
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 : X ⟶ (restrictScalars f).obj Y
x : (↑((extendScalars f).obj X) : Type (max u₂ v))
zero :
  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)
⊢ 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)))
have tmul : ∀ (x : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑X : Type (max v u₂))),
  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 ⊗ₜ[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: induction x using TensorProduct.induction_on with
        | zero => rw [map_zero, map_zero]
        | tmul =>
          rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
          dsimp
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
          erw [ExtendRestrictScalarsAdj.Counit.map_hom_apply,
              ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply]
        | add => rw [map_add, map_add]; congr 1
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_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
⊢ IsLimit ((restrictScalars f).mapCone c)
have 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)
Tactic: have hc' := isLimitOfPreserves (forget₂ _ AddCommGrpCat) hc
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (hypothesis)
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))
⊢ PreservesColimit F (restrictScalars f)
have 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))
Tactic: have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGrpCat) :=
    inferInstanceAs (HasColimit (F ⋙ forget₂ _ AddCommGrpCat))
-- 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_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))
⊢ PreservesColimit F (restrictScalars f)
have apply : IsColimit ((restrictScalars f).mapCocone (HasColimit.colimitCocone F))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (HasColimit.isColimitColimitCocone F)
-- 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_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))
⊢ IsColimit ((restrictScalars f).mapCocone (HasColimit.colimitCocone F))
have 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)))
Tactic: apply isColimitOfReflects (forget₂ (ModuleCat.{v} R) AddCommGrpCat)
-- 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_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))
⊢ 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)))
have t : IsColimit (HasColimit.colimitCocone F)
Tactic: apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGrpCat.{v})
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R : Type u₁
inst : CommRing R
M : ModuleCat R
⊢ (Adjunction.homEquiv (extendRestrictScalarsAdj.{u_1, u₁, u₁} (RingHom.id R)) M (Functor.obj (𝟭 (ModuleCat R)) M) :
        (a : (extendScalars (RingHom.id R)).obj M ⟶ (𝟭 (ModuleCat R)).obj M) →
          M ⟶ (restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M))
      (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M) =
    NatTrans.app (Iso.inv (restrictScalarsId R)) M
have hf : ∀ (m : (↑M : Type (max u_1 u₁))),
  Eq (α := (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
    ((Hom.hom
            ((Adjunction.homEquiv (extendRestrictScalarsAdj.{u_1, u₁, u₁} (RingHom.id R)) M
                  (Functor.obj (𝟭 (ModuleCat R)) M) :
                (a : (extendScalars (RingHom.id R)).obj M ⟶ (𝟭 (ModuleCat R)).obj M) →
                  M ⟶ (restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M))
              (NatTrans.app (Iso.hom (extendScalarsId.{u₁, u_1} R)) M)) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
    ((Hom.hom (NatTrans.app (Iso.inv (restrictScalarsId R)) M) :
          (a : (↑M : Type (max u_1 u₁))) →
            (↑((restrictScalars (RingHom.id R)).obj ((𝟭 (ModuleCat R)).obj M)) : Type (max u_1 u₁)))
        m :
      (↑(Functor.obj (restrictScalars (RingHom.id R)) (Functor.obj (𝟭 (ModuleCat R)) M)) : Type (max u_1 u₁)))
Tactic: ext m