awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
n : Type v
inst : Unique n
X Y : CommRingCat
f : X ⟶ Y
⊢ Eq (α := (coyoneda.obj (op n)).obj X ⟶ Functor.obj (𝟭 CommRingCat) Y)
    ((coyoneda.obj (op n)).map f ≫
      Iso.hom
        ((fun (X : CommRingCat) ↦
            (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
              of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (X : CommRingCat) ↦
            (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
              of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 CommRingCat) f)
have hf : ∀ (x : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))),
  Eq (α := (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
    ((Hom.hom
            ((coyoneda.obj (op n)).map f ≫
              Iso.hom
                ((fun (X : CommRingCat) ↦
                    (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
                      of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
                  Y)) :
          (a : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))) → (↑((𝟭 CommRingCat).obj Y) : Type (max u v)))
        x :
      (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
    ((Hom.hom
            (Iso.hom
                ((fun (X : CommRingCat) ↦
                    (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
                      of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
                  X) ≫
              CategoryTheory.Functor.map (𝟭 CommRingCat) f) :
          (a : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))) → (↑((𝟭 CommRingCat).obj Y) : Type (max u v)))
        x :
      (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) ⋯ =
    Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
      Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯
have h : Hom.hom
    (Under.Hom.right
      (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) sorry)) =
  Hom.hom
    (Under.Hom.right
      (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) sorry ≫
        Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) sorry))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯))
have h : ∀ (r : (↑R : Type (max u v))),
  Eq (α :=
    (↑(Under.right (X := R)
          (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
            (ofHom MonoidAlgebra.singleOneRingHom))) :
      Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g))))
                sorry)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single 1 r) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) sorry ≫
                Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) sorry)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single 1 r) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
Tactic: apply MonoidAlgebra.ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
S : Under R
⊢ (Functor.obj
          ((Under.forget R ⋙
              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                CommMonCat.carrier)) ⋙
            R.monoidAlgebra)
          S).hom ≫
      ofHom
        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
          (MonoidHom.id
            (↑(Functor.obj
                  (Under.forget R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                      CommMonCat.carrier))
                  S) :
              Type u))
          ⋯) =
    (Functor.obj (𝟭 (Under R)) S).hom
have hf : ∀ (x : (↑R : Type u)),
  Eq (α := (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
    ((Hom.hom
            ((Functor.obj
                  ((Under.forget R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := CommMonCat.carrier)) ⋙
                    R.monoidAlgebra)
                  S).hom ≫
              ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id
                    (↑(Functor.obj
                          (Under.forget R ⋙
                            forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦
                              (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
                          S) :
                      Type u))
                  sorry)) :
          (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u))
        x :
      (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
    ((Hom.hom (Functor.obj (𝟭 (Under R)) S).hom : (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u)) x :
      (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)
have a : ∀ (x : (↑S : Type u)),
  Eq (α := (↑S : Type u))
    (((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)
have a : ∀ (x : (↑R : Type u)),
  Eq (α := (↑R : Type u))
    (((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)
have a : ∀ (x : (↑S : Type u)),
  Eq (α := (↑S : Type u))
    (((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)
have a : ∀ (x : (↑R : Type u)),
  Eq (α := (↑R : Type u))
    (((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)
have a : ∀ (x : (↑S : Type u)),
  Eq (α := (↑S : Type u))
    (((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)
have a : ∀ (x : (↑R : Type u)),
  Eq (α := (↑R : Type u))
    (((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) = RingHom.id (↑S : Type u)
have a : ∀ (x : (↑S : Type u)),
  Eq (α := (↑S : Type u))
    (((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) : (a : (↑S : Type u)) → (↑S : Type u)) x :
      (↑S : Type u))
    ((RingHom.id (↑S : Type u) : (a : (↑S : Type u)) → (↑S : Type u)) x : (↑S : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Basic (goal)
Goal:
R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) = RingHom.id (↑R : Type u)
have a : ∀ (x : (↑R : Type u)),
  Eq (α := (↑R : Type u))
    (((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) : (a : (↑R : Type u)) → (↑R : Type u)) x :
      (↑R : Type u))
    ((RingHom.id (↑R : Type u) : (a : (↑R : Type u)) → (↑R : Type u)) x : (↑R : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 1 = 1
have a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 1) one
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j : J
x y : (↑(F.1 j) : Type v)
⊢ coconeFun F j (x * y) = coconeFun F j x * coconeFun F j y
have a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x * y))
  ((Prequotient.of j x).mul (Prequotient.of j y))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 0 = 0
have a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j 0) zero
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j : J
x y : (↑(F.1 j) : Type v)
⊢ coconeFun F j (x + y) = coconeFun F j x + coconeFun F j y
have a : (colimitSetoid F : Prequotient F → Prequotient F → Prop) (Prequotient.of j (x + y))
  ((Prequotient.of j x).add (Prequotient.of j y))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j
have hf : ∀ (x : (↑(F.obj j) : Type v)),
  Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((Hom.hom (F.map f ≫ coconeMorphism F j') : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x :
      (↑(colimit F) : Type v))
    ((Hom.hom (coconeMorphism F j) : (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v)) x : (↑(colimit F) : Type v))
have hf : (colimitSetoid F : Prequotient F → Prequotient F → Prop)
  (Prequotient.of j' (((F.map f).hom' : (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v)) x)) (Prequotient.of j x)
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j) :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
have rw : Eq (α := (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
          (coconeMorphism F j') :
        (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
        x) :
    (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
          (F.map f ≫ coconeMorphism F j') :
        (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
      x :
    (↑(colimit F) : Type v))
Tactic: rw [← cocone_naturality F f, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
rw :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (F.map f ≫ coconeMorphism F j') :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
⊢ Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j') :
          (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x) :
      (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (coconeMorphism F j) :
          (a : (↑(F.obj j) : Type v)) → (↑(colimit F) : Type v))
        x :
      (↑(colimit F) : Type v))
have rw₁ : Eq (α := (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
          (coconeMorphism F j') :
        (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
        x) :
    (↑(colimit F) : Type v))
  ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
          (coconeMorphism F j') :
        (a : (↑(F.obj j') : Type v)) → (↑(colimit F) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
        x) :
    (↑(colimit F) : Type v))
Tactic: rw [← cocone_naturality F f, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
⊢ ColimitType F → (↑s.pt : Type v)
have f : (a : Prequotient F) → (↑s.pt : Type v)
Tactic: fapply Quot.lift
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
f : (a : Prequotient F) → (↑s.pt : Type v)
⊢ ColimitType F → (↑s.pt : Type v)
have a : ∀ (a b : Prequotient F) (a_1 : (colimitSetoid F : Prequotient F → Prequotient F → Prop) a b),
  descFunLift F s a = descFunLift F s b
Tactic: fapply Quot.lift
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg
have a : -descFunLift F s x = -descFunLift F s x'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ -descFunLift F s x = -descFunLift F s x'
have a : -descFunLift F s x' = -descFunLift F s x'
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.add y) = descFunLift F s (x'.add y)
have a : descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x' + descFunLift F s y
have a : descFunLift F s x' + descFunLift F s y = descFunLift F s x' + descFunLift F s y
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.add y) = descFunLift F s (x.add y')
have a : descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s x + descFunLift F s y'
have a : descFunLift F s x + descFunLift F s y' = descFunLift F s x + descFunLift F s y'
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)
have a : descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x x' y : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x' * descFunLift F s y
have a : descFunLift F s x' * descFunLift F s y = descFunLift F s x' * descFunLift F s y
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')
have a : descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y_1 x y y' : Prequotient F
r : Relation F y y'
ih : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s x * descFunLift F s y'
have a : descFunLift F s x * descFunLift F s y' = descFunLift F s x * descFunLift F s y'
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (add zero x) = descFunLift F s x
have a : 0 + descFunLift F s x = descFunLift F s x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x
have a : descFunLift F s x = descFunLift F s x
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (x.add zero) = descFunLift F s x
have a : descFunLift F s x + 0 = descFunLift F s x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s x + 0 = descFunLift F s x
have a : descFunLift F s x = descFunLift F s x
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x
have a : 1 * descFunLift F s x = descFunLift F s x
Tactic: dsimp