awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ 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 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 _
Cleared hypotheses: r
-- 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
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
⊢ descFunLift F s x = descFunLift F s y
have 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)
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 _
Cleared hypotheses: r
-- 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
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)
⊢ descFunLift F s x = descFunLift F s y
have 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')
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 _
Cleared hypotheses: r
-- 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
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')
⊢ descFunLift F s x = descFunLift F s y
have a₈ : ∀ (x y z : Prequotient F), descFunLift F s ((x.mul y).mul z) = descFunLift F s (x.mul (y.mul z))
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 _
Cleared hypotheses: r
-- 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
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))
⊢ descFunLift F s x = descFunLift F s y
have a₉ : ∀ (x : Prequotient F), descFunLift F s (mul one x) = descFunLift F s x
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 _
Cleared hypotheses: r
-- 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
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
⊢ descFunLift F s x = descFunLift F s y
have a₁₀ : ∀ (x : Prequotient F), descFunLift F s (x.mul one) = descFunLift F s x
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 _
Cleared hypotheses: r
-- 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
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y
have 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
Tactic: induction x using Quot.inductionOn
Cleared hypotheses: x
-- 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
y : ColimitType F
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
have 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)
Tactic: induction y using Quot.inductionOn
Cleared hypotheses: y
-- 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
⊢ m = descMorphism F s
have 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))
Tactic: ext x
-- 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 : (↑(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))
have 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))
Tactic: induction x using Quot.inductionOn with | h x => ?_
Cleared hypotheses: x
-- 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
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))
have 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))
Tactic: change _ = s.ι.app j _
-- 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
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)
            (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))
have 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))
Tactic: rw [← w j]
-- 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
⊢ 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))
have 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))
Tactic: rw [quot_one, map_one]
-- 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 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))
have 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))
Tactic: rw [quot_mul, map_mul, hx, hy]
-- 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
⊢ 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 : ∀ (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))
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