-- Module: Mathlib.Algebra.Category.MonCat.Colimits
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))
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))
⊢ 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))

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

Premises used: MonCat.Colimits.quot_one, MonCat.of, MonCat.Colimits.quot_mul, map_mul, map_one, MonCat.Colimits.Prequotient.one, MonCat.Colimits.Prequotient.mul