awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
x : (↑(free.obj X') : Type u)
hf :
  Eq (α := (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X')) Y) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → (↑Y : Type u)) → FreeAbelianGroup X' →+ (↑Y : Type u))
              (Function.comp (β := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X)) :
            FreeAbelianGroup X' →+ (↑Y : Type u)) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
⊢ Eq (α := (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X')) Y) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X → ToType Y) → ToHom (of (FreeAbelianGroup X)) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X)) Y) :
          (a : FreeAbelianGroup X) → (↑Y : Type u))
        ((FreeAbelianGroup.map (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X) :
              (a : FreeAbelianGroup X') → FreeAbelianGroup X)
            x :
          FreeAbelianGroup X) :
      (↑Y : Type u))

Tactic:
rw [← FreeAbelianGroup.lift_comp]

Premises used: FreeAbelianGroup.lift_comp
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
x : (↑(free.obj X') : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X')) Y) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → (↑Y : Type u)) → FreeAbelianGroup X' →+ (↑Y : Type u))
              (Function.comp (β := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X)) :
            FreeAbelianGroup X' →+ (↑Y : Type u)) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
⊢ free.IsLeftAdjoint

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, AddCommGrpCat.adj
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, AddCommGrpCat.adj
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
G H : AddCommGrpCat
f : G ⟶ H
inst : Mono f
⊢ Function.Injective (α := (↑G : Type u)) (β := (↑H : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑G : Type u)) → (↑H : Type u))

Tactic:
(mono_iff_injective _).mp (Functor.map_mono (forget AddCommGrpCat) f)

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.Functor.map_mono, AddCommGrpCat, CategoryTheory.forget, Iff.mp
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
pos : ∀ (hX : IsEmpty X), Mono (free.map f)
neg : ∀ (hX : Nonempty X), Mono (free.map f)
⊢ Mono (free.map f)

Tactic:
by_cases! hX : IsEmpty X

Premises used: IsEmpty
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : IsEmpty X
pos : ∀ {Z : AddCommGrpCat.{u}} (g h : Z ⟶ free.obj X), g ≫ free.map f = h ≫ free.map f → g = h
⊢ Mono (free.map f)

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : IsEmpty X
Z : AddCommGrpCat
g h_1 : Z ⟶ free.obj X
h_2 : g ≫ free.map f = h_1 ≫ free.map f
⊢ g = h_1

Tactic:
apply (IsInitial.isInitialObj free _
        ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt

Premises used: Iff.mpr, AddCommGrpCat.free, CategoryTheory.Limits.Types.initial_iff_empty, Nonempty.some, CategoryTheory.Limits.IsInitial.isZero, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.Limits.IsInitial.isInitialObj
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
rwa rwa₁ rwa₂ rwa₃ : Mono f
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
rwa [← mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
have hf : Function.Injective f := by rwa [← mono_iff_injective]
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
hf :
  Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
neg :
  ∀ (g : (fun (X : Type u) ↦ X) Y → (fun (X : Type u) ↦ X) X)
    (hg :
      Function.LeftInverse g
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)),
    Mono (free.map f)
⊢ Mono (free.map f)

Tactic:
obtain ⟨g, hg⟩ := hf.hasLeftInverse

Premises used: Function.Injective.hasLeftInverse
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
hf :
  Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
g : (fun (X : Type u) ↦ X) Y → (fun (X : Type u) ↦ X) X
hg :
  Function.LeftInverse g
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
⊢ IsSplitMono f

Tactic:
have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
hf :
  Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
g : (fun (X : Type u) ↦ X) Y → (fun (X : Type u) ↦ X) X
hg :
  Function.LeftInverse g
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
this : IsSplitMono f
⊢ Mono (free.map f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : GrpCat
f : X' ⟶ X
g :
  X ⟶ Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
hf :
  Eq (α := (↑(free.obj X') : Type u) →* (↑Y : Type u))
    (Hom.hom
      ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
          g))
⊢ Eq (α := free.obj X' ⟶ Y)
    ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g) :
      free.obj X' ⟶ Y)
    (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
          g :
      free.obj X' ⟶ Y)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : GrpCat
f : X' ⟶ X
g :
  X ⟶ Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
hf :
  ∀ (a : X'),
    Eq (α := (↑Y : Type u))
      (((Hom.hom
                ((Equiv.symm
                      (Equiv.trans
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := carrier))
                        (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                    (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
                  (f ≫ g)) :
              (↑(free.obj X') : Type u) →* (↑Y : Type u)) :
            (a : FreeGroup X') → (↑Y : Type u))
          (FreeGroup.of a) :
        (↑Y : Type u))
      ((Hom.hom
              (free.map f ≫
                (Equiv.symm
                      (Equiv.trans
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := carrier))
                        (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                    (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
                  g) :
            (a : FreeGroup X') → (↑Y : Type u))
          (FreeGroup.of a) :
        (↑Y : Type u))
⊢ Eq (α := (↑(free.obj X') : Type u) →* (↑Y : Type u))
    (Hom.hom
      ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
          g))

Tactic:
apply FreeGroup.ext_hom

Premises used: FreeGroup.ext_hom
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : Type u
Y : GrpCat
f : X' ⟶ X
g :
  X ⟶ Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
a : X'
⊢ Eq (α := (↑Y : Type u))
    (((Hom.hom
              ((Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
                (f ≫ g)) :
            (↑(free.obj X') : Type u) →* (↑Y : Type u)) :
          (a : FreeGroup X') → (↑Y : Type u))
        (FreeGroup.of a) :
      (↑Y : Type u))
    ((Hom.hom
            (free.map f ≫
              (Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
                g) :
          (a : FreeGroup X') → (↑Y : Type u))
        (FreeGroup.of a) :
      (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: GrpCat.adj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : GrpCat
hf :
  CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X))))) =
    CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u))))
⊢ CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X)))) =
    𝟙 (CommGrpCat.of (Abelianization (↑X : Type u)))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : GrpCat
hf :
  MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X)) =
    (Equiv.symm Abelianization.lift :
        (a : Abelianization (↑X : Type u) →* Abelianization (↑X : Type u)) →
          (↑X : Type u) →* Abelianization (↑X : Type u))
      (CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u)))))
⊢ CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X))))) =
    CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u))))

Tactic:
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr

Premises used: Iff.mpr, Abelianization.lift, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X : GrpCat
⊢ MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X)) =
    (Equiv.symm Abelianization.lift :
        (a : Abelianization (↑X : Type u) →* Abelianization (↑X : Type u)) →
          (↑X : Type u) →* Abelianization (↑X : Type u))
      (CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u)))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
hf :
  Eq.{u + 1} (α :=
    (↑(CommGrpCat.of (Abelianization (↑X : Type u))) : Type u) →*
      (↑(CommGrpCat.of (Abelianization (↑Z : Type u))) : Type u))
    (CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g))))))
    (CommGrpCat.Hom.hom
      (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom f))))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom g))))))
⊢ Eq.{u + 1} (α := CommGrpCat.of (Abelianization (↑X : Type u)) ⟶ CommGrpCat.of (Abelianization (↑Z : Type u)))
    (CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g)))))
    (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom f))))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom g)))))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
hf :
  MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g)) =
    (Equiv.symm Abelianization.lift :
        (a : Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u)) →
          (↑X : Type u) →* Abelianization (↑Z : Type u))
      (CommGrpCat.Hom.hom
        (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
          (CommGrpCat.ofHom
            ((Abelianization.lift :
                (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                  Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
              (MonoidHom.comp Abelianization.of (Hom.hom f))))
          (CommGrpCat.ofHom
            ((Abelianization.lift :
                (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                  Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
              (MonoidHom.comp Abelianization.of (Hom.hom g))))))
⊢ Eq.{u + 1} (α :=
    (↑(CommGrpCat.of (Abelianization (↑X : Type u))) : Type u) →*
      (↑(CommGrpCat.of (Abelianization (↑Z : Type u))) : Type u))
    (CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g))))))
    (CommGrpCat.Hom.hom
      (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom f))))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom g))))))

Tactic:
apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr

Premises used: Iff.mpr, Abelianization.lift, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g)) =
    (Equiv.symm Abelianization.lift :
        (a : Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u)) →
          (↑X : Type u) →* Abelianization (↑Z : Type u))
      (CommGrpCat.Hom.hom
        (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
          (CommGrpCat.ofHom
            ((Abelianization.lift :
                (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                  Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
              (MonoidHom.comp Abelianization.of (Hom.hom f))))
          (CommGrpCat.ofHom
            ((Abelianization.lift :
                (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                  Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
              (MonoidHom.comp Abelianization.of (Hom.hom g))))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Adjunctions
Goal:
X' X : GrpCat
Y : CommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := carrier))
      Y
x : (↑(abelianize.obj X') : Type u)
x_1 : (↑X' : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((CommGrpCat.Hom.hom
            (abelianize.map f ≫
              (Equiv.symm
                    (Equiv.trans (β :=
                      ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X
                        (Functor.obj
                          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                            (CC := CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦
                            (↑x1 : Type u) →* (↑x2 : Type u)) (CD := carrier))
                          Y))
                      (Equiv.trans (β :=
                        ToHom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          CommGrpCat.carrier) (abelianize.obj X) Y)
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : CommGrpCat.{u}) ↦
                          (↑x1 : Type u) →* (↑x2 : Type u)) (CC := CommGrpCat.carrier))
                        (Equiv.symm Abelianization.lift))
                      (Equiv.symm
                        (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := carrier)))) :
                  (a : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → abelianize.obj X ⟶ Y)
                g) :
          (a : Abelianization (↑X' : Type u)) → (↑Y : Type u))
        ((Abelianization.of : (a : (↑X' : Type u)) → Abelianization (↑X' : Type u)) x_1 :
          Abelianization (↑X' : Type u)) :
      (↑Y : Type u))
    ((((Equiv.symm
                  (Equiv.symm
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                      (CC := carrier))) :
                (a : X' ⟶ (forget₂ CommGrpCat GrpCat).obj Y) → ToHom X' ((forget₂ CommGrpCat GrpCat).obj Y))
              (f ≫ g) :
            ToHom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) X'
              (Functor.obj
                (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  carrier))
                Y)) :
          (a : (↑X' : Type u)) → (↑Y : Type u))
        x_1 :
      (↑Y : Type u))

Tactic:
apply Abelianization.lift_apply_of

Premises used: Abelianization.lift_apply_of