awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (c'.ι.app j) :
            (a : (↑(F.obj j) : Type w)) → (↑c'.pt : Type w))
          x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
have h : Eq (α := AddCircle (𝕜 := ℚ) 1)
  (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
        (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
      ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
        ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
          AddCircle (𝕜 := ℚ) 1)) :
    AddCircle (𝕜 := ℚ) 1)
  ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
    AddCircle (𝕜 := ℚ) 1)
Tactic: dsimp [c']
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
          ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
            AddCircle (𝕜 := ℚ) 1)) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
have h : Eq (α := AddCircle (𝕜 := ℚ) 1)
  ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
    AddCircle (𝕜 := ℚ) 1)
  ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
    AddCircle (𝕜 := ℚ) 1)
Tactic: rw [AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ Eq.{v + 1} (α :=
    (𝟙_ (Type v)) (𝒞 := types) ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (η ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd)) η
have rw : Eq (α :=
  (𝟙_ (Type v)) (𝒞 := types) ⟶
    CommGrp.X
      (Functor.obj (C := CommGrp.{v, u} C)
        (F ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              carrier)).mapCommGrp
        (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
  (η ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
  (CategoryStruct.comp (Y :=
    (F ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier)).obj
      (tensorUnit.{v, u} C (𝒞 := inst)))
    (Functor.LaxMonoidal.ε
      (F ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          carrier)))
    ((F ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier)).map
      η))
Tactic: rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    Functor.obj (C := CommGrp.{v, u} C)
      (F ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier)).mapCommGrp
      (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)
have refine : Eq.{v + 1} (α :=
  tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
      (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
    CommGrp.X
      (Functor.obj (C := CommGrp.{v, u} C)
        (F ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              carrier)).mapCommGrp
        (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
  (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
  ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
Tactic: refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
    rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
    cat_disch) ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ Eq.{v + 1} (α :=
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
have dsimp : (𝟙
        (tensorObj (𝒞 := types)
          (MonTypeEquivalenceMon.inverse.obj
              (Functor.obj
                (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                  MonCat.carrier))
                (Functor.obj
                  (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                    (CD := GrpCat.carrier))
                  (toCommGrp.obj (F.obj X))))).X
          (MonTypeEquivalenceMon.inverse.obj
              (Functor.obj
                (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                  MonCat.carrier))
                (Functor.obj
                  (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                    (CD := GrpCat.carrier))
                  (toCommGrp.obj (F.obj X))))).X) ≫
      μ) ≫
    Iso.hom (Equiv.toIso Multiplicative.toAdd) =
  (Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ
Tactic: dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ (𝟙
          (tensorObj (𝒞 := types)
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Iso.hom (Equiv.toIso Multiplicative.toAdd) =
    (Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ
have this₁ : F.Additive
Tactic: have : F.Additive := Functor.additive_of_preserves_binary_products _
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LeftExactFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this_2 : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ (𝟙
          (tensorObj (𝒞 := types)
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Iso.hom (Equiv.toIso Multiplicative.toAdd) =
    (Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ
have simp : Eq.{v + 1} (α :=
  tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
      (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
  (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
  ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
Tactic: simp only [Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  a ∈ (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).map
            f) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget GrpCat).obj j)) → (fun (X : Type u) ↦ X) ((F ⋙ forget GrpCat).obj j'))
      (a⁻¹ j) =
    a⁻¹ j'
have simp : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                (F.map f)) :
            (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))) :
      (a : (F ⋙ forget GrpCat).obj j) → (F ⋙ forget GrpCat).obj j')
    (a j)⁻¹ =
  (a j')⁻¹
Tactic: simp only [Functor.comp_map, Pi.inv_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  a ∈ (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (F.map f)) :
              (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))) :
        (a : (F ⋙ forget GrpCat).obj j) → (F ⋙ forget GrpCat).obj j')
      (a j)⁻¹ =
    (a j')⁻¹
have dsimp : (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.map f) :
      (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
    (a j)⁻¹ =
  (a j')⁻¹
Tactic: dsimp [Functor.sections] at ah ⊢
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
        (a j) =
      a j'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.map f) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
      (a j)⁻¹ =
    (a j')⁻¹
have rw : ((Hom.hom (F.map f) : (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u)) (a j))⁻¹ = (a j')⁻¹
Tactic: rw [(F.map f).hom.map_inv (a j), ah f]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
        (a j) =
      a j'
j j' : J
f : j ⟶ j'
rw : ((Hom.hom (F.map f) : (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u)) (a j))⁻¹ = (a j')⁻¹
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.map f) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
      (a j)⁻¹ =
    (a j')⁻¹
have rw₁ : (a j')⁻¹ = (a j')⁻¹
Tactic: rw [(F.map f).hom.map_inv (a j), ah f]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
this : Functor.ReflectsIsomorphisms
  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
    fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier)) :=
  ⋯
c' :
  Cone
    (F ⋙
      forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
        fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
t : IsLimit c'
⊢ Small.{u, max u v}
    (↑((F ⋙
              forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
                (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              MonCat.carrier)).sections :
      Type (max u v))
have this₁ : HasLimit
  (F ⋙
    forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
      fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
Tactic: have : HasLimit (F ⋙ forget₂ GrpCat MonCat) := ⟨_, t⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ HasLimit F ↔
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))
have mp : HasLimit F →
  Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
mp :
  HasLimit F →
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))
⊢ HasLimit F ↔
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))
have mpr : Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v)) →
  HasLimit F
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommGrpCat
c :
  Cone
    (F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
hc : IsLimit c
⊢ LiftsToLimit F
    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
      (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
    c hc
have this : HasLimit
  (F ⋙
    forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
      (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
Tactic: have : HasLimit _ := ⟨_, hc⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Limits (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommGrpCat
c :
  Cone
    (F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
hc : IsLimit c
this :
  HasLimit
    (F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
⊢ LiftsToLimit F
    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
      (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
    c hc
have this₁ : Small.{u, max u v}
  (↑(F ⋙
          forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
            carrier)).sections :
    Type (max u v))
Tactic: have : Small.{u} (F ⋙ forget CommGrpCat).sections :=
      Concrete.small_sections_of_hasLimit (F ⋙ forget₂ CommGrpCat GrpCat)