awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
rw :
  Eq (α := (↑(colimit F) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 : CommRingCat.{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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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 ⥤ CommRingCat
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
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ 1 * descFunLift F s x = descFunLift F s x
have a : descFunLift F s x = descFunLift F s x
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x
have a : descFunLift F s x * 1 = 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 ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s x * 1 = descFunLift F s x
have a : descFunLift F s x = descFunLift F s x
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (x.neg.add x) = descFunLift F s zero
have a : -descFunLift F s x + descFunLift F s x = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ -descFunLift F s x + descFunLift F s x = 0
have a : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
Tactic: rw [neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
⊢ descFunLift F s (x.add y) = descFunLift F s (y.add x)
have a : descFunLift F s x + descFunLift F s y = descFunLift F s y + 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 ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
⊢ descFunLift F s x + descFunLift F s y = descFunLift F s y + descFunLift F s x
have a : descFunLift F s y + descFunLift F s x = descFunLift F s y + descFunLift F s x
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
⊢ descFunLift F s (x.mul y) = descFunLift F s (y.mul x)
have a : descFunLift F s x * descFunLift F s y = descFunLift F s y * 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 ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y : Prequotient F
⊢ descFunLift F s x * descFunLift F s y = descFunLift F s y * descFunLift F s x
have a : descFunLift F s y * descFunLift F s x = descFunLift F s y * descFunLift F s x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s ((x.add y).add z) = descFunLift F s (x.add (y.add z))
have a : descFunLift F s x + descFunLift F s y + descFunLift F s z = descFunLift F s x + (descFunLift F s y + descFunLift F s z)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)
have a : descFunLift F s x + (descFunLift F s y + descFunLift F s z) =
  descFunLift F s x + (descFunLift F s y + descFunLift F s z)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))
have a : descFunLift F s x * descFunLift F s y * descFunLift F s z = descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y * descFunLift F s z =
    descFunLift F s x * (descFunLift F s y * descFunLift F s z)
have a : descFunLift F s x * (descFunLift F s y * descFunLift F s z) =
  descFunLift F s x * (descFunLift F s y * descFunLift F s z)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s (x.mul (y.add z)) = descFunLift F s ((x.mul y).add (x.mul z))
have a : descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
  descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
have a : descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z =
  descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ descFunLift F s ((x.add y).mul z) = descFunLift F s ((x.mul z).add (y.mul z))
have a : (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
  descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y_1 x y z : Prequotient F
⊢ (descFunLift F s x + descFunLift F s y) * descFunLift F s z =
    descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
have a : descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z =
  descFunLift F s x * descFunLift F s z + descFunLift F s y * descFunLift F s z
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (mul zero x) = descFunLift F s zero
have a : 0 * descFunLift F s x = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ 0 * descFunLift F s x = 0
have a : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s (x.mul zero) = descFunLift F s zero
have a : descFunLift F s x * 0 = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x_1 y x : Prequotient F
⊢ descFunLift F s x * 0 = 0
have a : Eq.{v + 1} (α := (↑s.pt : Type v)) 0 0
Tactic: rw [mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
⊢ descFunLift F s x = descFunLift F s y
have a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
Tactic: induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
⊢ descFunLift F s x = descFunLift F s y
have a₁ : ∀ (x y : Prequotient F),
  Relation F x y → ∀ (ih : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
Tactic: induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
a₁ :
  ∀ (x y : Prequotient F),
    Relation F x y → ∀ (ih : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
⊢ descFunLift F s x = descFunLift F s y
have a₂ : ∀ (x y z : Prequotient F),
  Relation F x y →
    Relation F y z →
      ∀ (ih1 : descFunLift F s x = descFunLift F s y) (ih2 : descFunLift F s y = descFunLift F s z),
        descFunLift F s x = descFunLift F s z
Tactic: induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Colimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F : Prequotient F → Prequotient F → Prop) x y
a : ∀ (x : Prequotient F), descFunLift F s x = descFunLift F s x
a₁ :
  ∀ (x y : Prequotient F),
    Relation F x y → ∀ (ih : descFunLift F s x = descFunLift F s y), descFunLift F s y = descFunLift F s x
a₂ :
  ∀ (x y z : Prequotient F),
    Relation F x y →
      Relation F y z →
        ∀ (ih1 : descFunLift F s x = descFunLift F s y) (ih2 : descFunLift F s y = descFunLift F s z),
          descFunLift F s x = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s y
have a₃ : ∀ (j j' : J) (f : j ⟶ j') (x : (↑(F.obj j) : Type v)),
  descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj j) : Type v)) → (↑(F.obj j') : Type v))
          x)) =
    descFunLift F s (Prequotient.of j x)
Tactic: induction r with
    | refl => rfl
    | symm x y _ ih => exact ih.symm
    | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2
    | map j j' f x => exact RingHom.congr_fun (congrArg Hom.hom <| s.ι.naturality f) x
    | zero j => simp +instances
    | one j => simp +instances
    | neg j x => simp +instances
    | add j x y => simp +instances
    | mul j x y => simp +instances
    | neg_1 x x' r ih => dsimp; rw [ih]
    | add_1 x x' y r ih => dsimp; rw [ih]
    | add_2 x y y' r ih => dsimp; rw [ih]
    | mul_1 x x' y r ih => dsimp; rw [ih]
    | mul_2 x y y' r ih => dsimp; rw [ih]
    | zero_add x => dsimp; rw [zero_add]
    | add_zero x => dsimp; rw [add_zero]
    | one_mul x => dsimp; rw [one_mul]
    | mul_one x => dsimp; rw [mul_one]
    | neg_add_cancel x => dsimp; rw [neg_add_cancel]
    | add_comm x y => dsimp; rw [add_comm]
    | mul_comm x y => dsimp; rw [mul_comm]
    | add_assoc x y z => dsimp; rw [add_assoc]
    | mul_assoc x y z => dsimp; rw [mul_assoc]
    | left_distrib x y z => dsimp; rw [mul_add]
    | right_distrib x y z => dsimp; rw [add_mul]
    | zero_mul x => dsimp; rw [zero_mul]
    | mul_zero x => dsimp; rw [mul_zero]
Cleared hypotheses: r