awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f_1 : A ⟶ B
X Y : GrpCat
f : X ⟶ Y
e : Epi f
rwa :
  ∀
    (e :
      Function.Surjective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
    Epi (X :=
      Functor.obj
        (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
⊢ Epi (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
have rwa₁ : ∀
  (e :
    Epi (X := (↑X : Type u_1)) (Y := (↑Y : Type u_1))
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1)))),
  Epi (X :=
    Functor.obj
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)) f)
Tactic: rwa [epi_iff_surjective, ← CategoryTheory.ofHom_epi_iff_surjective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f : A ⟶ B
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
have rw : (Hom.hom f).range = ⊤ ↔
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
Tactic: rw [epi_iff_range_eq_top, MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f : A ⟶ B
rw :
  (Hom.hom f).range = ⊤ ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))
have rw₁ : Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u)) ↔
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
Tactic: rw [epi_iff_range_eq_top, MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f_1 : A ⟶ B
X Y : CommGrpCat
f : X ⟶ Y
e : Mono f
⊢ Mono (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
have rwa : ∀
  (e :
    Function.Injective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
  Mono (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
Tactic: rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f_1 : A ⟶ B
X Y : CommGrpCat
f : X ⟶ Y
e : Mono f
rwa :
  ∀
    (e :
      Function.Injective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
    Mono (X :=
      Functor.obj
        (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier))
        X)
      (CategoryTheory.Functor.map
        (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier))
        f)
⊢ Mono (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
have rwa₁ : ∀
  (e :
    Mono (X := (↑X : Type u_1)) (Y := (↑Y : Type u_1))
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1)))),
  Mono (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
Tactic: rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f_1 : A ⟶ B
X Y : CommGrpCat
f : X ⟶ Y
e : Epi f
⊢ Epi (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
have rwa : ∀
  (e :
    Function.Surjective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
  Epi (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
Tactic: rwa [epi_iff_surjective, ← CategoryTheory.ofHom_epi_iff_surjective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : CommGrpCat
f_1 : A ⟶ B
X Y : CommGrpCat
f : X ⟶ Y
e : Epi f
rwa :
  ∀
    (e :
      Function.Surjective (α := (↑X : Type u_1)) (β := (↑Y : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1))),
    Epi (X :=
      Functor.obj
        (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier))
        X)
      (CategoryTheory.Functor.map
        (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier))
        f)
⊢ Epi (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
have rwa₁ : ∀
  (e :
    Epi (X := (↑X : Type u_1)) (Y := (↑Y : Type u_1))
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f) :
          (a : (↑X : Type u_1)) → (↑Y : Type u_1)))),
  Epi (X :=
    Functor.obj
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier))
      f)
Tactic: rwa [epi_iff_surjective, ← CategoryTheory.ofHom_epi_iff_surjective] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (hypothesis)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
j : J
x y : (↑(F.obj j) : Type (max u v))
⊢ HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v)))
      (G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))
      (G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
    G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j (x * y))
have this : HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v)))
    (G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))
    (G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
  G.mk F
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j
      (HMul.hMul (α := (↑(F.obj j) : Type (max u v))) (β := (↑(F.obj j) : Type (max u v)))
        ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                carrier
                (fun (X Y : GrpCat) ↦
                  (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))) j x)))) :
              (a : (↑(F.obj ⟨j, x⟩.fst) : Type (max u v))) → (↑(F.obj 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 x)) :
          (↑(F.obj j) : Type (max u v)))
        ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                carrier
                (fun (X Y : GrpCat) ↦
                  (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))) j y)))) :
              (a : (↑(F.obj ⟨j, y⟩.fst) : Type (max u v))) → (↑(F.obj 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 y)) :
          (↑(F.obj j) : Type (max u v)))))
Tactic: have := colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, y⟩ j (𝟙 _) (𝟙 _)
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  Types.FilteredColimit.Rel
    (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    x y
⊢ Eq (α := (↑(G.{v, u} F) : Type (max u v))) (colimitInvAux F x) (colimitInvAux F y)
have 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)))
        (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
        (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹) ⟶
    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)))
        (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
        (y.snd (β := 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 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map f) :
          (a : (↑(F.obj ⟨x.fst, x.snd⁻¹⟩.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)))
            (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : 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 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (F.map g) :
          (a : (↑(F.obj ⟨y.fst, y.snd⁻¹⟩.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)))
            (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
            (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹)) :
      (↑(F.obj k) : Type (max u v)))
Tactic: apply G.mk_eq
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x : (↑(G.{v, u} F) : Type (max u v))
⊢ (↑(G.{v, u} F) : Type (max u v))
have refine : ∀ (a b : (j : J) × (↑(F.obj j) : Type (max u v)))
  (a_1 :
    ((F ⋙
            forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).ColimitTypeRel
      a b),
  Eq (α := (↑(G.{v, u} F) : Type (max u v))) (colimitInvAux F a) (colimitInvAux F b)
Tactic: refine Quot.lift (colimitInvAux.{v, u} F) ?_ x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x_1 : (↑(G.{v, u} F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((F ⋙
          forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).ColimitTypeRel
    x y
⊢ Eq (α := (↑(G.{v, u} F) : Type (max u v))) (colimitInvAux F x) (colimitInvAux F y)
have h₁ : Types.FilteredColimit.Rel
  (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier)) x
  y
Tactic: apply colimitInvAux_eq_of_rel
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x_1 : (↑(G.{v, u} F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((F ⋙
          forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).ColimitTypeRel
    x y
⊢ Types.FilteredColimit.Rel
    (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    x y
have h₁ : (F ⋙
      forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
        carrier)).ColimitTypeRel
  x y
Tactic: apply Types.FilteredColimit.rel_of_colimitTypeRel
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x : (↑(G.{v, u} F) : Type (max u v))
⊢ x⁻¹ * x = 1
have refine : ∀
  (a :
    (j : J) ×
      ((F ⋙
              forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).obj
        j),
  (Quot.mk
          ((F ⋙
                forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          a)⁻¹ *
      Quot.mk
        ((F ⋙
              forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        a =
    1
Tactic: refine Quot.inductionOn x ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x :
  (j : J) ×
    ((F ⋙
            forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j
⊢ (Quot.mk
          ((F ⋙
                forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          x)⁻¹ *
      Quot.mk
        ((F ⋙
              forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        x =
    1
have change : HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v))) (G.mk F x)⁻¹ (G.mk F x) = 1
Tactic: change (G.mk _ _)⁻¹ * G.mk _ _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x :
  (j : J) ×
    ((F ⋙
            forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j
⊢ HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v))) (G.mk F x)⁻¹ (G.mk F x) = 1
have obtain : ∀ (j : J)
  (x :
    ((F ⋙
            forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j),
  HMul.hMul (α := (↑(G.{v, u} F) : Type (max u v)))
      (G.mk F
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x))⁻¹
      (G.mk F
        (Sigma.mk (β := fun (j : J) ↦
          ((F ⋙
                  forget₂ GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑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)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  MonCat.carrier)).obj
            j)
          j x)) =
    1
Tactic: obtain ⟨j, x⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.ForgetCorepresentable (goal)
Goal:
G : Type u
inst : AddCommGroup G
x y : G
⊢ (uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) (x + y) =
    HAdd.hAdd (α := ULift.{u, 0} ℤ →+ G) (β := ULift.{u, 0} ℤ →+ G)
      ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) x : ULift.{u, 0} ℤ →+ G)
      ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) y : ULift.{u, 0} ℤ →+ G)
have h : ∀ (x_1 : ULift.{u, 0} ℤ),
  Eq (α := G)
    ((((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) (x + y) : ULift.{u, 0} ℤ →+ G) : (a : ULift.{u, 0} ℤ) → G)
        x_1 :
      G)
    ((HAdd.hAdd (α := ULift.{u, 0} ℤ →+ G) (β := ULift.{u, 0} ℤ →+ G)
            ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) x : ULift.{u, 0} ℤ →+ G)
            ((uliftZMultiplesHom G : (a : G) → ULift.{u, 0} ℤ →+ G) y : ULift.{u, 0} ℤ →+ G) :
          (a : ULift.{u, 0} ℤ) → G)
        x_1 :
      G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Images (goal)
Goal:
G H : AddCommGrpCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f
have hf : ∀ (x : (↑G : Type)),
  Eq (α := (↑H : Type)) ((Hom.hom (factorThruImage f ≫ ι f) : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
    ((Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x : (↑H : Type))
Tactic: ext