-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Colimits (goal)
Goal:
J : Type v
inst : Category.{u, v} J
F : CategoryTheory.Functor.{u, v, v, v + 1} J MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : Prequotient F
hf :
  ∀ (j : J) (x : (↑(F.obj j) : Type v)),
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
        (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (Prequotient.of j x)) :
        (↑s.pt : Type v))
hf₁ :
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) one) :
      (↑s.pt : Type v))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
      (↑s.pt : Type v))
have hf₂ : ∀ (x y : Prequotient F)
  (hx :
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
        (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x) :
        (↑s.pt : Type v)))
  (hy :
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
        (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y) :
        (↑s.pt : Type v))),
  Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) (x.mul y)) :
      (↑s.pt : Type v))
Tactic: induction x with
    | of j =>
      change _ = s.ι.app j _
      rw [← w j]
      rfl
    | one =>
      rw [quot_one, map_one]
      rfl
    | mul x y hx hy =>
      rw [quot_mul, map_mul, hx, hy]
      solve_by_elim
Cleared hypotheses: x