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
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))
⊢ 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:
solve_by_elim
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
m : M.{v, u} F
⊢ ∃ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) = m

Tactic:
(F ⋙ forget MonCat).ιColimitType_jointly_surjective m

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, CategoryTheory.Functor.comp, MonCat, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k) (g :
    y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj x.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
        (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map g) :
            (a : (↑(F.obj y.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
        (↑(F.obj k) : Type (max u v)))
⊢ mk F x = mk F y

Tactic:
Quot.eqvGen_sound (Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel (F ⋙ forget MonCat) x y h)

Premises used: Quot.eqvGen_sound, CategoryTheory.Functor.comp, CategoryTheory.Functor.ColimitType, MonCat, CategoryTheory.forget, CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
j k : J
f : j ⟶ k
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑(F.obj k) : Type (max u v)))
    ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
            carrier
            (fun (X Y : MonCat) ↦
              (MonoidHom.instFunLike :
                FunLike ((↑X : Type (max u v)) →* (↑Y : Type (max u v))) (↑X : Type (max u v)) (↑Y : Type (max u v))))
            _ _ _
            (F.map
              (𝟙
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
                    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦
                          (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) (F.map f) :
                        (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
                      x))))) :
          (a :
              (↑(F.obj
                    ⟨k,
                        (ConcreteCategory.hom (F.map f) :
                            (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
                          x⟩.fst) :
                Type (max u v))) →
            (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
            ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CC := carrier) (F.map f) :
                (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
              x))) :
      (↑(F.obj k) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map f) :
          (a : (↑(F.obj ⟨j, x⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) :
      (↑(F.obj k) : Type (max u v)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
h :
  ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj ⟨⋯.some, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)) :
        (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map g) :
            (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)) :
        (↑(F.obj k) : Type (max u v)))
⊢ 1 = M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)

Tactic:
apply M.mk_eq

Premises used: MonCat.FilteredColimits.M.mk_eq
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
⊢ ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj ⟨⋯.some, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)) :
        (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map g) :
            (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)) :
        (↑(F.obj k) : Type (max u v)))

Tactic:
⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.max, Exists.intro, CategoryTheory.IsFiltered.leftToMax
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
⊢ Eq (α :=
    (↑(F.obj
          (IsFiltered.max
            (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
            j)) :
      Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X :=
            F.obj
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)))
            (Y :=
            F.obj
              (IsFiltered.max
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j))
            (F.map
              (IsFiltered.leftToMax
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j)) :
          (a : (↑(F.obj ⟨⋯.some, 1⟩.fst) : Type (max u v))) →
            (↑(F.obj (IsFiltered.max ⟨⋯.some, 1⟩.fst j)) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)) :
      (↑(F.obj
            (IsFiltered.max
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
              j)) :
        Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (Y :=
            F.obj
              (IsFiltered.max
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j))
            (F.map
              (IsFiltered.rightToMax
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j)) :
          (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max ⟨⋯.some, 1⟩.fst j)) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)) :
      (↑(F.obj
            (IsFiltered.max
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
              j)) :
        Type (max u v)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x x' y : (j : J) × (↑(F.obj j) : Type (max u v))
hxx' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    x x'
obtain :
  ∀ (j₁ : J) (x : (↑(F.obj j₁) : Type (max u v)))
    (hxx' :
      Types.FilteredColimit.Rel
        (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) x'),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) y = colimitMulAux F x' y
⊢ colimitMulAux F x y = colimitMulAux F x' y

Tactic:
obtain ⟨j₁, x⟩ := x
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x' y : (j : J) × (↑(F.obj j) : Type (max u v))
j₁ : J
x : (↑(F.obj j₁) : Type (max u v))
hxx' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) x'
obtain :
  ∀ (j₂ : J) (y : (↑(F.obj j₂) : Type (max u v))),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
      colimitMulAux F x' (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) y = colimitMulAux F x' y

Tactic:
obtain ⟨j₂, y⟩ := y
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x' : (j : J) × (↑(F.obj j) : Type (max u v))
j₁ : J
x : (↑(F.obj j₁) : Type (max u v))
hxx' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) x'
j₂ : J
y : (↑(F.obj j₂) : Type (max u v))
obtain :
  ∀ (j₃ : J) (x' : (↑(F.obj j₃) : Type (max u v)))
    (hxx' :
      Types.FilteredColimit.Rel
        (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x')),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
      colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x')
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
    colimitMulAux F x' (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)

Tactic:
obtain ⟨j₃, x'⟩ := x'
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j₁ : J
x : (↑(F.obj j₁) : Type (max u v))
j₂ : J
y : (↑(F.obj j₂) : Type (max u v))
j₃ : J
x' : (↑(F.obj j₃) : Type (max u v))
l : J
f :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) ⟶
    l
g :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x') ⟶
    l
hfg :
  Eq (α := (↑(F.obj l) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map f) :
          (a : (↑(F.obj ⟨j₁, x⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x :
      (↑(F.obj l) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map g) :
          (a : (↑(F.obj ⟨j₃, x'⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x' :
      (↑(F.obj l) : Type (max u v)))
obtain :
  ∀ (s : J) (α : IsFiltered.max j₁ j₂ ⟶ s) (β : l ⟶ s) (γ : IsFiltered.max j₃ j₂ ⟶ s)
    (h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β)
    (h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ)
    (h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
      colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x')
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x')
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)

Tactic:
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
    IsFiltered.tulip (IsFiltered.leftToMax j₁ j₂) (IsFiltered.rightToMax j₁ j₂)
      (IsFiltered.rightToMax j₃ j₂) (IsFiltered.leftToMax j₃ j₂) f g

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.tulip, CategoryTheory.IsFiltered.leftToMax
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j₁ : J
x : (↑(F.obj j₁) : Type (max u v))
j₂ : J
y : (↑(F.obj j₂) : Type (max u v))
j₃ : J
x' : (↑(F.obj j₃) : Type (max u v))
l : J
f :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x) ⟶
    l
g :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x') ⟶
    l
hfg :
  Eq (α := (↑(F.obj l) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map f) :
          (a : (↑(F.obj ⟨j₁, x⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x :
      (↑(F.obj l) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map g) :
          (a : (↑(F.obj ⟨j₃, x'⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x' :
      (↑(F.obj l) : Type (max u v)))
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ x')
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y)

Tactic:
apply M.mk_eq

Premises used: MonCat.FilteredColimits.M.mk_eq
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x y y' : (j : J) × (↑(F.obj j) : Type (max u v))
hyy' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    y y'
obtain :
  ∀ (j₁ : J) (y : (↑(F.obj j₁) : Type (max u v)))
    (hyy' :
      Types.FilteredColimit.Rel
        (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) y'),
    colimitMulAux F x (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) = colimitMulAux F x y'
⊢ colimitMulAux F x y = colimitMulAux F x y'

Tactic:
obtain ⟨j₁, y⟩ := y
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x y' : (j : J) × (↑(F.obj j) : Type (max u v))
j₁ : J
y : (↑(F.obj j₁) : Type (max u v))
hyy' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) y'
obtain :
  ∀ (j₂ : J) (x : (↑(F.obj j₂) : Type (max u v))),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
      colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x) y'
⊢ colimitMulAux F x (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) = colimitMulAux F x y'

Tactic:
obtain ⟨j₂, x⟩ := x
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
y' : (j : J) × (↑(F.obj j) : Type (max u v))
j₁ : J
y : (↑(F.obj j₁) : Type (max u v))
hyy' :
  Types.FilteredColimit.Rel
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) y'
j₂ : J
x : (↑(F.obj j₂) : Type (max u v))
obtain :
  ∀ (j₃ : J) (y' : (↑(F.obj j₃) : Type (max u v)))
    (hyy' :
      Types.FilteredColimit.Rel
        (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')),
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
      colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x) y'

Tactic:
obtain ⟨j₃, y'⟩ := y'