awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j₁ : J
y : (↑(F.obj j₁) : Type (max u v))
j₂ : J
x : (↑(F.obj j₂) : Type (max u v))
j₃ : J
y' : (↑(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₁ y) ⟶
    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₃ y') ⟶
    l
hfg :
  Eq (α :=
    ToType (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) (F.obj l))
    ((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 l) : Type (max u v)))
        y :
      (↑(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₃) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        y' :
      (↑(F.obj l) : Type (max u v)))
obtain :
  ∀ (s : J) (α : IsFiltered.max j₂ j₁ ⟶ s) (β : l ⟶ s) (γ : IsFiltered.max j₂ j₃ ⟶ s)
    (h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β)
    (h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ)
    (h₃ : IsFiltered.rightToMax 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.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁)
      (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax 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
y : (↑(F.obj j₁) : Type (max u v))
j₂ : J
x : (↑(F.obj j₂) : Type (max u v))
j₃ : J
y' : (↑(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₁ y) ⟶
    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₃ y') ⟶
    l
hfg :
  Eq (α :=
    ToType (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) (F.obj l))
    ((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 l) : Type (max u v)))
        y :
      (↑(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₃) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        y' :
      (↑(F.obj l) : Type (max u v)))
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax 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 : M.{v, u} F
refine_1 :
  ∀ (a b₁ b₂ : (j : J) × (↑(F.obj j) : Type (max u v))),
    (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).ColimitTypeRel
        b₁ b₂ →
      colimitMulAux F a b₁ = colimitMulAux F a b₂
refine_2 :
  ∀ (a₁ a₂ b : (j : J) × (↑(F.obj j) : Type (max u v))),
    (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).ColimitTypeRel
        a₁ a₂ →
      colimitMulAux F a₁ b = colimitMulAux F a₂ b
⊢ M.{v, u} F

Tactic:
refine Quot.lift₂ (colimitMulAux F) ?_ ?_ x y

Premises used: Quot.lift₂, MonCat.FilteredColimits.colimitMulAux
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x y y' : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'
refine_1 :
  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'
⊢ colimitMulAux F x y = colimitMulAux F x y'

Tactic:
apply colimitMulAux_eq_of_rel_right

Premises used: MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x y y' : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'
refine_1 :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'
⊢ 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'

Tactic:
apply Types.FilteredColimit.rel_of_colimitTypeRel

Premises used: CategoryTheory.Limits.Types.FilteredColimit.rel_of_colimitTypeRel
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x y y' : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'
⊢ (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'

Tactic:
h
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x y y' : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'
⊢ (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    y y'

Tactic:
exact h
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x x' y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'
refine_2 :
  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'
⊢ colimitMulAux F x y = colimitMulAux F x' y

Tactic:
apply colimitMulAux_eq_of_rel_left

Premises used: MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x x' y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'
refine_2 :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'
⊢ 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'

Tactic:
apply Types.FilteredColimit.rel_of_colimitTypeRel

Premises used: CategoryTheory.Limits.Types.FilteredColimit.rel_of_colimitTypeRel
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x x' y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'
⊢ (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'

Tactic:
h
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x_1 y_1 : M.{v, u} F
x x' y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'
⊢ (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).ColimitTypeRel
    x x'

Tactic:
exact h
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
x y : (↑(F.obj j) : Type (max u v))
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) *
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j (x * y))

Tactic:
simpa using colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, MonCat.FilteredColimits.colimit_mul_mk_eq, Sigma.mk
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x : M.{v, u} F
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    1 * M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
⊢ 1 * x = x

Tactic:
obtain ⟨j, x, rfl⟩ := x.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- 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))
rw :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1) *
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
rw₁ :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j (1 * x)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
rw₂ rw₃ :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
⊢ 1 * M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)

Tactic:
rw [colimit_one_eq F j, colimit_mul_mk_eq', one_mul]

Premises used: MonCat.FilteredColimits.colimit_mul_mk_eq', MonCat.FilteredColimits.colimit_one_eq, one_mul
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x : M.{v, u} F
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) * 1 =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
⊢ x * 1 = x

Tactic:
obtain ⟨j, x, rfl⟩ := x.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- 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))
rw :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) *
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
rw₁ :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j (x * 1)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
rw₂ rw₃ :
  M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) * 1 =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)

Tactic:
rw [colimit_one_eq F j, colimit_mul_mk_eq', mul_one]

Premises used: MonCat.FilteredColimits.colimit_mul_mk_eq', MonCat.FilteredColimits.colimit_one_eq, mul_one
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x y z : M.{v, u} F
obtain :
  ∀ (j₁ : J) (x₁ : (↑(F.obj j₁) : Type (max u v))),
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) * y * z =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) * (y * z)
⊢ x * y * z = x * (y * z)

Tactic:
obtain ⟨j₁, x₁, rfl⟩ := x.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
y z : M.{v, u} F
j₁ : J
x₁ : (↑(F.obj j₁) : Type (max u v))
obtain :
  ∀ (j₂ : J) (y₂ : (↑(F.obj j₂) : Type (max u v))),
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
          M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
        z =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) * z)
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) * y * z =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) * (y * z)

Tactic:
obtain ⟨j₂, y₂, rfl⟩ := y.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
z : M.{v, u} F
j₁ : J
x₁ : (↑(F.obj j₁) : Type (max u v))
j₂ : J
y₂ : (↑(F.obj j₂) : Type (max u v))
obtain :
  ∀ (j₃ : J) (z₃ : (↑(F.obj j₃) : Type (max u v))),
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
          M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃) =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
          M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃))
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
      z =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) * z)

Tactic:
obtain ⟨j₃, z₃, rfl⟩ := z.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- 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
z₃ : (↑(F.obj j₃) : Type (max u v))
⊢ ∃ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x : (↑(F.obj j) : Type (max u v))) (y :
    (↑(F.obj j) : Type (max u v))) (z : (↑(F.obj j) : 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₁) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
          x₁ =
        x ∧
      (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 j) : Type (max u v)))
            y₂ =
          y ∧
        (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 j) : Type (max u v)))
            z₃ =
          z

Tactic:
⟨IsFiltered.max₃ j₁ j₂ j₃, IsFiltered.firstToMax₃ _ _ _,
          IsFiltered.secondToMax₃ _ _ _, IsFiltered.thirdToMax₃ _ _ _,
          _, _, _, rfl, rfl, rfl⟩

Premises used: CategoryTheory.IsFiltered.firstToMax₃, CategoryTheory.IsFiltered.max₃, And.intro, Exists.intro, CategoryTheory.IsFiltered.secondToMax₃, CategoryTheory.IsFiltered.thirdToMax₃, rfl
-- 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
z₃ : (↑(F.obj j₃) : Type (max u v))
obtain :
  ∀ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x y z : (↑(F.obj j) : Type (max u v)))
    (h₁ :
      (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 j) : Type (max u v)))
          x₁ =
        x)
    (h₂ :
      (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 j) : Type (max u v)))
          y₂ =
        y)
    (h₃ :
      (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 j) : Type (max u v)))
          z₃ =
        z),
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
          M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃) =
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
          M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃))
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃))

Tactic:
obtain ⟨j, f₁, f₂, f₃, x, y, z, h₁, h₂, h₃⟩ :
          ∃ (j : J) (f₁ : j₁ ⟶ j) (f₂ : j₂ ⟶ j) (f₃ : j₃ ⟶ j) (x y z : F.obj j),
          F.map f₁ x₁ = x ∧ F.map f₂ y₂ = y ∧ F.map f₃ z₃ = z :=
        ⟨IsFiltered.max₃ j₁ j₂ j₃, IsFiltered.firstToMax₃ _ _ _,
          IsFiltered.secondToMax₃ _ _ _, IsFiltered.thirdToMax₃ _ _ _,
          _, _, _, rfl, rfl, rfl⟩
-- 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
z₃ : (↑(F.obj j₃) : Type (max u v))
j : J
f₁ : j₁ ⟶ j
f₂ : j₂ ⟶ j
f₃ : j₃ ⟶ j
x y z : (↑(F.obj j) : Type (max u v))
h₁ :
  (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 j) : Type (max u v)))
      x₁ =
    x
h₂ :
  (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 j) : Type (max u v)))
      y₂ =
    y
h₃ :
  (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 j) : Type (max u v)))
      z₃ =
    z
⊢ M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
      M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ x₁) *
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ y₂) *
        M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ z₃))

Tactic:
simp only [← M.map_mk F f₁, ← M.map_mk F f₂, ← M.map_mk F f₃, h₁, h₂, h₃,
        colimit_mul_mk_eq', mul_assoc]

Premises used: MonCat.FilteredColimits.colimit_mul_mk_eq', mul_assoc, MonCat.FilteredColimits.M.map_mk