awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
w : (↑A : Type u)
h :
  Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
⊢ Membership.mem (α := (↑B : Type u)) (↑(Hom.hom f).range : Set (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
use a
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
⊢ Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {b : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')}
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
have : f a ∈ { b | h b = g b } := by
    rw [← agree]
    use a
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
this :
  Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {b : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')}
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
hf hf₁ :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
    ((((g : (a : (↑B : Type u)) → SX')
              ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      f :
                    (a : (↑A : Type u)) → (↑B : Type u))
                  a :
                (↑B : Type u)) :
            SX') :
          (a : X') → X')
        x :
      X')
⊢ Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')
    ((((h : (a : (↑B : Type u)) → SX') ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) : SX') :
          (a : X') → X')
        x :
      X')

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∉ (Hom.hom f).range
r : g = h
apply :
  Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (x • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))
⊢ False

Tactic:
apply fromCoset_ne_of_nin_range _ hx

Premises used: GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∉ (Hom.hom f).range
r : g = h
⊢ Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    ((((h : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')

Tactic:
replace r :=
    DFunLike.congr_fun (DFunLike.congr_fun r x) (fromCoset ⟨f.hom.range, ⟨1, one_leftCoset _⟩⟩)
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∉ (Hom.hom f).range
r :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
    ((((h : (a : (↑B : Type u)) → SX') x : SX') : (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯)) :
      X')
⊢ Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (x • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (↑(Hom.hom f).range : Set (↑B : Type u)) ⋯))

Tactic:
simpa [g_apply_fromCoset, «h», tau, g_apply_infinity] using r

Premises used: GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity, GrpCat.SurjectiveOfEpiAuxs.h, GrpCat.SurjectiveOfEpiAuxs.tau, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
inst : Epi f
by_contra! :
  ∀ (b : (↑B : Type u))
    (hb :
      ∀ (a : (↑A : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
              (a : (↑A : Type u)) → (↑B : Type u))
            a ≠
          b),
    False
⊢ ∀ (b : (↑B : Type u)),
    ∃ (a : (↑A : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          a =
        b

Tactic:
by_contra! ⟨b, hb⟩
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
inst : Epi f
b : (↑B : Type u)
hb :
  ∀ (a : (↑A : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a ≠
      b
⊢ False

Tactic:
SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
      (congr_arg GrpCat.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

Premises used: False, _private.0.GrpCat.surjective_of_epi.match_1, GrpCat.Hom.hom, GrpCat.SurjectiveOfEpiAuxs.comp_eq, congr_arg, GrpCat.SurjectiveOfEpiAuxs.g_ne_h, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
inst : Epi f
b : (↑B : Type u)
hb :
  ∀ (a : (↑A : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        a ≠
      b
⊢ False

Tactic:
exact
    SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
      (congr_arg GrpCat.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

Premises used: False, _private.0.GrpCat.surjective_of_epi.match_1, GrpCat.Hom.hom, GrpCat.SurjectiveOfEpiAuxs.comp_eq, congr_arg, GrpCat.SurjectiveOfEpiAuxs.g_ne_h, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
⊢ Epi f ↔
    Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) f) :
        (a : (↑A : Type u)) → (↑B : Type u))

Tactic:
⟨fun _ => surjective_of_epi f, ConcreteCategory.epi_of_surjective f⟩

Premises used: GrpCat.surjective_of_epi, CategoryTheory.ConcreteCategory.epi_of_surjective, Iff.intro
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
⊢ Epi f ↔ (Hom.hom f).range = ⊤

Tactic:
Iff.trans (epi_iff_surjective _) (Subgroup.eq_top_iff' f.hom.range).symm

Premises used: MonoidHom.range, GrpCat.Hom.hom, Subgroup.eq_top_iff', Iff.trans, GrpCat.epi_iff_surjective, Iff.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩

Premises used: Iff.intro, CategoryTheory.Functor.epi_of_epi_map, groupAddGroupEquivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
refine : Epi f → Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
apply groupAddGroupEquivalence.inverse.map_epi

Premises used: CategoryTheory.Functor.map_epi, groupAddGroupEquivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) := by
    refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
    apply groupAddGroupEquivalence.inverse.map_epi
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (i1 :
      Epi f ↔
        Function.Surjective (α := (↑(groupAddGroupEquivalence.inverse.obj A) : Type u)) (β :=
          (↑(groupAddGroupEquivalence.inverse.obj B) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                GrpCat.carrier) (groupAddGroupEquivalence.inverse.map f)) :
            (a : (↑(groupAddGroupEquivalence.inverse.obj A) : Type u)) →
              (↑(groupAddGroupEquivalence.inverse.obj B) : Type u))),
    Epi f ↔
      Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddGrpCat.{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 : AddGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            f) :
        (a : (↑A : Type u)) → (↑B : Type u))

Tactic:
rwa [GrpCat.epi_iff_surjective] at i1

Premises used: GrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔ (Hom.hom f).range = ⊤

Tactic:
Iff.trans (epi_iff_surjective _) (AddSubgroup.eq_top_iff' f.hom.range).symm

Premises used: AddMonoidHom.range, AddGrpCat.Hom.hom, AddSubgroup.eq_top_iff', Iff.trans, AddGrpCat.epi_iff_surjective, Iff.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f_1 : A ⟶ B
X Y : GrpCat
f : X ⟶ Y
e : Mono f
rwa :
  ∀
    (e :
      Function.Injective (α := (↑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))),
    Mono (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)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (e :
      Mono (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)))),
    Mono (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)
⊢ Mono (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 [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e

Premises used: GrpCat.mono_iff_injective, CategoryTheory.ofHom_mono_iff_injective
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ 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

Premises used: CategoryTheory.ofHom_epi_iff_surjective, GrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : CommGrpCat
f : A ⟶ B
inst : Mono f
⊢ (Hom.hom f).ker = ⊥

Tactic:
MonoidHom.ker_eq_bot_of_cancel fun u v h => ConcreteCategory.ext_iff.mp <|
    (@cancel_mono _ _ _ _ _ f _ (ofHom u) (ofHom v)).1 <| ConcreteCategory.ext h

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ConcreteCategory.ext, CategoryTheory.ConcreteCategory.ext_iff, MonoidHom.ker_eq_bot_of_cancel, Iff.mp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : CommGrpCat
f : A ⟶ B
⊢ Mono f ↔ (Hom.hom f).ker = ⊥

Tactic:
⟨fun _ => ker_eq_bot_of_mono f, fun h =>
    ConcreteCategory.mono_of_injective _ <| (MonoidHom.ker_eq_bot_iff f.hom).1 h⟩

Premises used: MonoidHom.ker_eq_bot_iff, Iff.intro, Iff.mp, CommGrpCat.ker_eq_bot_of_mono, CategoryTheory.ConcreteCategory.mono_of_injective, CommGrpCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : CommGrpCat
f : A ⟶ B
⊢ Mono f ↔
    Function.Injective (α := (↑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:
Iff.trans (mono_iff_ker_eq_bot f) <| MonoidHom.ker_eq_bot_iff f.hom

Premises used: CommGrpCat.mono_iff_ker_eq_bot, MonoidHom.ker_eq_bot_iff, Iff.trans, CommGrpCat.Hom.hom
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : CommGrpCat
f : A ⟶ B
inst : Epi f
⊢ (Hom.hom f).range = ⊤

Tactic:
MonoidHom.range_eq_top_of_cancel fun u v h => ConcreteCategory.ext_iff.mp <|
    (@cancel_epi _ _ _ _ _ f _ (ofHom u) (ofHom v)).1 (ConcreteCategory.ext h)

Premises used: CategoryTheory.ConcreteCategory.ext, CategoryTheory.ConcreteCategory.ext_iff, MonoidHom.range_eq_top_of_cancel, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : CommGrpCat
f : A ⟶ B
⊢ Epi f ↔ (Hom.hom f).range = ⊤

Tactic:
⟨fun _ => range_eq_top_of_epi _, fun hf =>
    ConcreteCategory.epi_of_surjective _ <| show Function.Surjective f.hom from
      MonoidHom.range_eq_top.mp hf⟩

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective, CommGrpCat.range_eq_top_of_epi, MonoidHom.range_eq_top, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
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))
rw₁ 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))
⊢ 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))

Tactic:
rw [epi_iff_range_eq_top, MonoidHom.range_eq_top]

Premises used: MonoidHom.range_eq_top, CommGrpCat.epi_iff_range_eq_top
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ 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

Premises used: CommGrpCat.mono_iff_injective, CategoryTheory.ofHom_mono_iff_injective
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ 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

Premises used: CommGrpCat.epi_iff_surjective, CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
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 :
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k) (g :
    y.fst (β := 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) : Type (max u v))) → (↑(F.obj k) : 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) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
        (↑(F.obj k) : Type (max u v)))
⊢ Eq (α := (↑(G.{v, u} F) : Type (max u v))) (mk F x) (mk F y)

Tactic:
Quot.eqvGen_sound (Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel (F ⋙ forget GrpCat) x y h)

Premises used: Quot.eqvGen_sound, GrpCat, CategoryTheory.Functor.comp, CategoryTheory.Functor.ColimitType, CategoryTheory.forget, CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
j : J
⊢ Eq (α := (↑(G.{v, u} F) : Type (max u v))) 1
    (G.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1))

Tactic:
MonCat.FilteredColimits.colimit_one_eq _ _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.ColimitType, MonCat.FilteredColimits.colimit_one_eq