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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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 ⥤ RingCat
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]
    | 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 ⥤ RingCat
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]
    | 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 ⥤ RingCat
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]
    | 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 ⥤ RingCat
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 : 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)) =
    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]
    | 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 ⥤ RingCat
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
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 : 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)) =
      descFunLift F s (Prequotient.of j x)
⊢ descFunLift F s x = descFunLift F s y
have a₄ : ∀ (j : J), descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
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]
    | 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 ⥤ RingCat
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
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 : 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)) =
      descFunLift F s (Prequotient.of j x)
a₄ : ∀ (j : J), descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
⊢ descFunLift F s x = descFunLift F s y
have a₅ : ∀ (j : J), descFunLift F s (Prequotient.of j 1) = descFunLift F s one
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]
    | 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 ⥤ RingCat
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
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 : 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)) =
      descFunLift F s (Prequotient.of j x)
a₄ : ∀ (j : J), descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
a₅ : ∀ (j : J), descFunLift F s (Prequotient.of j 1) = descFunLift F s one
⊢ descFunLift F s x = descFunLift F s y
have a₆ : ∀ (j : J) (x : (↑(F.obj j) : Type v)),
  descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (Prequotient.of j x).neg
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]
    | 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 ⥤ RingCat
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
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 : 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)) =
      descFunLift F s (Prequotient.of j x)
a₄ : ∀ (j : J), descFunLift F s (Prequotient.of j 0) = descFunLift F s zero
a₅ : ∀ (j : J), descFunLift F s (Prequotient.of j 1) = descFunLift F s one
a₆ :
  ∀ (j : J) (x : (↑(F.obj j) : Type v)),
    descFunLift F s (Prequotient.of j (-x)) = descFunLift F s (Prequotient.of j x).neg
⊢ descFunLift F s x = descFunLift F s y
have a₇ : ∀ (j : J) (x y : (↑(F.obj j) : Type v)),
  descFunLift F s (Prequotient.of j (x + y)) = descFunLift F s ((Prequotient.of j x).add (Prequotient.of j y))
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]
    | 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