-- 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
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)
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
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))
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).mul (Prequotient.of j y))
a₉ :
  ∀ (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
a₁₀ :
  ∀ (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)
a₁₁ :
  ∀ (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')
a₁₂ :
  ∀ (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)
a₁₃ :
  ∀ (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')
⊢ descFunLift F s x = descFunLift F s y
have a₁₄ : ∀ (x : Prequotient F), descFunLift F s (add zero 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