awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x_1 y x : Prequotient F
⊢ descFunLift F s x = descFunLift F s x

Tactic:
rfl
-- 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
x_1 y_1 x y : Prequotient F
h_1 : Relation F x y
h : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
h.symm

Premises used: Eq.symm
-- 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
x_1 y_1 x y : Prequotient F
h_1 : Relation F x y
h : descFunLift F s x = descFunLift F s y
⊢ descFunLift F s y = descFunLift F s x

Tactic:
exact h.symm

Premises used: Eq.symm
-- 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
x_1 y_1 x y z : Prequotient F
h : Relation F x y
h_1 : Relation F y z
h₁ : descFunLift F s x = descFunLift F s y
h₂ : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
h₁.trans h₂

Premises used: Eq.trans
-- 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
x_1 y_1 x y z : Prequotient F
h : Relation F x y
h_1 : Relation F y z
h₁ : descFunLift F s x = descFunLift F s y
h₂ : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
exact h₁.trans h₂

Premises used: Eq.trans
-- 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
x_1 y : Prequotient F
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : 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:
s.w_apply f x

Premises used: CategoryTheory.Limits.Cocone.w_apply, MonCat.Colimits.descFunLift
-- 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
x_1 y : Prequotient F
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type v)
⊢ descFunLift F s
      (Prequotient.of j'
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : 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:
exact s.w_apply f x

Premises used: CategoryTheory.Limits.Cocone.w_apply
-- 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
x_1 y_1 : Prequotient F
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))

Tactic:
map_mul (s.ι.app j).hom x y

Premises used: MonCat.Hom.hom, map_mul, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app, MonCat.Colimits.descFunLift
-- 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
x_1 y_1 : Prequotient F
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))

Tactic:
exact map_mul (s.ι.app j).hom x y

Premises used: MonCat.Hom.hom, map_mul, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- 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
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one

Tactic:
map_one (s.ι.app j).hom

Premises used: MonCat.Hom.hom, CategoryTheory.Limits.Cocone.ι, map_one, CategoryTheory.NatTrans.app, MonCat.Colimits.descFunLift
-- 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
x y : Prequotient F
j : J
⊢ descFunLift F s (Prequotient.of j 1) = descFunLift F s one

Tactic:
exact map_one (s.ι.app j).hom

Premises used: MonCat.Hom.hom, CategoryTheory.Limits.Cocone.ι, map_one, CategoryTheory.NatTrans.app
-- 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
x_1 y_1 x x' y : Prequotient F
h_1 : Relation F x x'
h : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
congr_arg (· * _) h

Premises used: HMul.hMul, congr_arg, MonCat.Colimits.descFunLift
-- 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
x_1 y_1 x x' y : Prequotient F
h_1 : Relation F x x'
h : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
exact congr_arg (· * _) h

Premises used: HMul.hMul, congr_arg
-- 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
x_1 y_1 x y y' : Prequotient F
h_1 : Relation F y y'
h : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
congr_arg (_ * ·) h

Premises used: HMul.hMul, congr_arg, MonCat.Colimits.descFunLift
-- 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
x_1 y_1 x y y' : Prequotient F
h_1 : Relation F y y'
h : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
exact congr_arg (_ * ·) h

Premises used: HMul.hMul, congr_arg
-- 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
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))

Tactic:
mul_assoc _ _ _

Premises used: mul_assoc, MonCat.Colimits.descFunLift
-- 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
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))

Tactic:
exact mul_assoc _ _ _

Premises used: mul_assoc
-- 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
x_1 y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x

Tactic:
one_mul _

Premises used: one_mul, MonCat.Colimits.descFunLift
-- 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
x_1 y x : Prequotient F
⊢ descFunLift F s (mul one x) = descFunLift F s x

Tactic:
exact one_mul _

Premises used: one_mul
-- 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
x_1 y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
mul_one _

Premises used: mul_one, MonCat.Colimits.descFunLift
-- 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
x_1 y x : Prequotient F
⊢ descFunLift F s (x.mul one) = descFunLift F s x

Tactic:
exact mul_one _

Premises used: mul_one
-- 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
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 → ∀ (h : 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 →
        ∀ (h₁ : descFunLift F s x = descFunLift F s y) (h₂ : 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 (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : 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) (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₅ : ∀ (j : J), descFunLift F s (Prequotient.of j 1) = descFunLift F s one
a₆ :
  ∀ (x x' y : Prequotient F),
    Relation F x x' →
      ∀ (h : 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),
    Relation F y y' →
      ∀ (h : descFunLift F s y = descFunLift F s y'), descFunLift F s (x.mul y) = descFunLift F s (x.mul y')
a₈ : ∀ (x y z : Prequotient F), descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))
a₉ : ∀ (x : Prequotient F), descFunLift F s (mul one x) = descFunLift F s x
a₁₀ : ∀ (x : Prequotient F), descFunLift F s (x.mul one) = descFunLift F s x
⊢ descFunLift F s x = descFunLift F s y

Tactic:
induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _

Premises used: mul_assoc, MonCat.Colimits.Prequotient.one, MonCat.Colimits.Prequotient.mul, symm, mul_one, refl, one_mul
-- 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
x y : ColimitType F
h :
  ∀ (a : Prequotient F),
    descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a * y) =
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) * descFun F s y
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
induction x using Quot.inductionOn
-- 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
y : ColimitType F
a : Prequotient F
h :
  ∀ (a_1 : Prequotient F),
    descFun F s
        (HMul.hMul (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
          (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a_1)) =
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) *
        descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a_1)
⊢ descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a * y) =
    descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) * descFun F s y

Tactic:
induction y using Quot.inductionOn
-- 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
a a_1 : Prequotient F
⊢ descFun F s
      (HMul.hMul (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a_1)) =
    descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a) *
      descFun F s (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) a_1)

Tactic:
solve_by_elim
-- 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
hf :
  ∀ (x : (↑(colimitCocone F).pt : Type v)),
    Eq (α := (↑s.pt : Type v))
      ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
      ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
⊢ m = descMorphism F s

Tactic:
ext x
-- 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
⊢ 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:
?_
-- 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 : (↑(colimitCocone F).pt : Type v)
hf :
  ∀ (x : Prequotient F),
    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))
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))

Tactic:
induction x using Quot.inductionOn with | h x => ?_
-- 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
j : J
x : (↑(F.obj j) : Type v)
hf :
  Eq (α := (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : 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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type v)) → (↑(((Functor.const J).obj s.pt).obj j) : Type v))
        x :
      (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) 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))

Tactic:
change _ = s.ι.app j _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.ι, DFunLike.coe, CategoryTheory.NatTrans.app
-- 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
j : J
x : (↑(F.obj j) : Type v)
hf :
  Eq (α := (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : 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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            ((colimitCocone F).ι.app j ≫ m) :
          (a : (↑(F.obj j) : Type v)) → (↑(((Functor.const J).obj s.pt).obj j) : Type v))
        x :
      (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : Type v))
⊢ Eq (α := (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : 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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            (s.ι.app j) :
          (a : (↑(F.obj j) : Type v)) → (↑(((Functor.const J).obj s.pt).obj j) : Type v))
        x :
      (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : Type v))

Tactic:
rw [← w j]
-- 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
j : J
x : (↑(F.obj j) : Type v)
⊢ Eq (α := (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : 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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := carrier)
            ((colimitCocone F).ι.app j ≫ m) :
          (a : (↑(F.obj j) : Type v)) → (↑(((Functor.const J).obj s.pt).obj j) : Type v))
        x :
      (↑(Functor.obj.{u, v, v, v + 1} (Functor.obj (Functor.const J) s.pt) j) : Type v))

Tactic:
rfl
-- 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
hf :
  Eq (α := (↑s.pt : Type v)) (1 : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) 1 : (↑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) 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))

Tactic:
rw [quot_one, map_one]

Premises used: MonCat.Colimits.quot_one, map_one
-- 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
⊢ Eq (α := (↑s.pt : Type v)) (1 : (↑s.pt : Type v))
    ((Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v)) 1 : (↑s.pt : Type v))

Tactic:
rfl
-- 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 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))
hf :
  HMul.hMul (α := (↑s.pt : Type v)) (β := (↑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))
      ((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)) =
    (Hom.hom (descMorphism F s) : (a : (↑(colimitCocone F).pt : Type v)) → (↑s.pt : Type v))
      (HMul.hMul (α := ColimitType F) (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) x)
        (Quot.mk (⇑(colimitSetoid F) : Prequotient F → Prequotient F → Prop) y))
⊢ 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:
rw [quot_mul, map_mul, hx, hy]

Premises used: MonCat.Colimits.quot_mul, map_mul