awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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)
⊢ 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)
have 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)
Tactic: rw [colimit_one_eq F j, colimit_mul_mk_eq', one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x : M.{v, u} F
⊢ x * 1 = x
have 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)
Tactic: obtain ⟨j, x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
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)
have 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)
Tactic: rw [colimit_one_eq F j, colimit_mul_mk_eq', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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)
⊢ 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)
have 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)
Tactic: rw [colimit_one_eq F j, colimit_mul_mk_eq', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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)
⊢ 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)
have 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)
Tactic: rw [colimit_one_eq F j, colimit_mul_mk_eq', mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
x y z : M.{v, u} F
⊢ x * y * z = x * (y * z)
have 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)
Tactic: obtain ⟨j₁, x₁, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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))
⊢ 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)
have 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)
Tactic: obtain ⟨j₂, y₂, rfl⟩ := y.mk_surjective
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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))
⊢ 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)
have 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₃))
Tactic: obtain ⟨j₃, z₃, rfl⟩ := z.mk_surjective
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
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))
⊢ 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₃))
have 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₃))
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⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
m : (colimitCocone.{v, u} F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone.{v, u} F).ι.app j ≫ m = t.ι.app j
y : (↑(colimitCocone.{v, u} F).pt : Type (max u v))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) m :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        y :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        y :
      (↑t.pt : Type (max u v)))
have obtain : ∀ (j : J)
  (y :
    (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).obj
      j),
  Eq (α := (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) m :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))
Tactic: obtain ⟨j, y, rfl⟩ := Functor.ιColimitType_jointly_surjective _ y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
x y : (↑(M.{v, u} F) : Type (max u v))
⊢ x * y = y * x
have obtain : ∀ (i : J)
  (x :
    (↑(Functor.obj
          (F ⋙
            forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
              (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
              (CD := MonCat.carrier))
          i) :
      Type (max u v))),
  MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          i x) *
      y =
    y *
      MonCat.FilteredColimits.M.mk
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        (Sigma.mk (β := fun (j : J) ↦
          (↑(Functor.obj
                (F ⋙
                  forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
                    (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier))
                j) :
            Type (max u v)))
          i x)
Tactic: obtain ⟨i, x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
j : J
⊢ Eq (α := (↑(F.obj j) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Types.Small.limitCone
                    (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier))).π.app
              j) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget MonCat)).pt).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
        1 :
      (fun (X : Type u) ↦ X)
        ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj j))
    (1 : (↑(F.obj j) : Type u))
have simp : Eq.{u + 1} (α := (↑(F.obj j) : Type u)) ((↑1 : (j : J) → ToType (F.obj j)) j) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ IsLimit (limitCone F)
have refine_1 : ∀ (s : Cone F),
  EquivLike.coe (E :=
      (↑(F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)) ≃
        Shrink.{u, max u v}
          (↑(F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
      (equivShrink
        (↑(F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier)).obj
                j) ↦
        x ∈
          (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier))
                      s))
                  j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget MonCat).mapCone s).pt).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
            1)
        sorry) =
    1
Tactic: refine IsLimit.ofFaithful (forget MonCat) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_ }) (fun s => rfl)
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ CreatesLimit F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
have h : (c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))) →
  (t : IsLimit c) →
    LiftsToLimit F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) c
      t
Tactic: apply createsLimitOfReflectsIso
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
s : Cone F
⊢ Eq (α :=
    (Types.Small.limitCone
        (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (IsLimit.lift
              (Types.Small.limitConeIsLimit
                (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)))
              (Functor.mapCone
                (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
            (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt)
        1 :
      (fun (X : Type u) ↦ X)
        (Types.Small.limitCone
            (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
    (1 :
      (Types.Small.limitCone
          (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
have simp : Eq.{u + 1} (α :=
  Shrink.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v)))
  ((equivShrink
          (↑(F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) :
        (a : (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
          Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦ 1) sorry) :
    Shrink.{u, max u v}
      (↑(F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
  (1 :
    (Types.Small.limitCone
        (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Shrink (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C MonCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) =
    ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
      (shrinkFunctor.{w, w', v, u} G).map f
have hf : ∀ (x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)),
  Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            ((shrinkFunctor.{w, w', v, u} F).map f ≫
              ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            (ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
              (shrinkFunctor.{w, w', v, u} G).map f) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
Tactic: ext x