awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
inst_2 : Small.{w, max w u} (Quot F)
x x_1 : J
x_2 : x ⟶ x_1
x_3 : (↑(F.obj x) : Type w)
hf hf₁ :
  Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
      Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
      Shrink.{w, max u w} (Quot F))
⊢ Eq.{w + 1} (α := Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x_1 : (a : (↑(F.obj x_1) : Type w)) → Quot F)
            ((Hom.hom (F.map x_2) : (a : (↑(F.obj x) : Type w)) → (↑(F.obj x_1) : Type w)) x_3) :
          Quot F) :
      Shrink.{w, max u w} (Quot F))
    ((AddEquiv.symm Shrink.addEquiv : (a : Quot F) → Shrink.{w, max u w} (Quot F))
        ((Quot.ι F x : (a : (↑(F.obj x) : Type w)) → Quot F) x_3 : Quot F) :
      Shrink.{w, max u w} (Quot F))

Tactic:
rw [Quot.map_ι]

Premises used: AddCommGrpCat.Colimits.Quot.map_ι
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : DecidableEq J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_2 : Small.{w, max u w} (Quot F)
⊢ Eq (α := Quot F →+ (↑(colimitCocone F).pt : Type w)) (desc F (colimitCocone F))
    (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))

Tactic:
Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : DecidableEq J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_2 : Small.{w, max u w} (Quot F)
refine :
  ∀ (j : J) (x : (↑(F.obj j) : Type w)),
    Eq.{w + 1} (α := (↑(colimitCocone F).pt : Type w))
      ((desc F (colimitCocone F) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
          ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
        (↑(colimitCocone F).pt : Type w))
      ((AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
          ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
        (↑(colimitCocone F).pt : Type w))
⊢ Eq (α := Quot F →+ (↑(colimitCocone F).pt : Type w)) (desc F (colimitCocone F))
    (AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv))

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Premises used: AddCommGrpCat.Colimits.Quot.addMonoidHom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : DecidableEq J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_2 : Small.{w, max u w} (Quot F)
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑(colimitCocone F).pt : Type w))
    ((desc F (colimitCocone F) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(colimitCocone F).pt : Type w))
    ((AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
        ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) :
      (↑(colimitCocone F).pt : Type w))

Tactic:
simpa only [colimitCocone_pt, AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe]
    using Quot.ι_desc F (colimitCocone F) j x

Premises used: AddEquiv.toAddMonoidHom_eq_coe, AddMonoidHom.coe_coe, AddCommGrpCat.Colimits.colimitCocone_pt, AddCommGrpCat.Colimits.colimitCocone, AddCommGrpCat.Colimits.Quot.ι_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
inst_2 : Small.{w, max u w} (Quot F)
refine :
  Function.Bijective (α := Quot F) (β := (↑(colimitCocone F).pt : Type w))
    (⇑(Quot.desc F (colimitCocone F)) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
⊢ IsColimit (colimitCocone F)

Tactic:
refine isColimit_of_bijective_desc F _ ?_

Premises used: AddCommGrpCat.Colimits.isColimit_of_bijective_desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
inst_2 : Small.{w, max u w} (Quot F)
rw :
  Function.Bijective (α := Quot F) (β := (↑(colimitCocone F).pt : Type w))
    (⇑(AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))
⊢ Function.Bijective (α := Quot F) (β := (↑(colimitCocone F).pt : Type w))
    (⇑(Quot.desc F (colimitCocone F)) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))

Tactic:
rw [Quot.desc_colimitCocone]

Premises used: AddCommGrpCat.Colimits.Quot.desc_colimitCocone
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
inst_2 : Small.{w, max u w} (Quot F)
⊢ Function.Bijective (α := Quot F) (β := (↑(colimitCocone F).pt : Type w))
    (⇑(AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))

Tactic:
Shrink.addEquiv.symm.bijective

Premises used: Shrink.addEquiv, AddEquiv.bijective, AddEquiv.symm
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
inst_2 : Small.{w, max u w} (Quot F)
⊢ Function.Bijective (α := Quot F) (β := (↑(colimitCocone F).pt : Type w))
    (⇑(AddEquiv.toAddMonoidHom (AddEquiv.symm Shrink.addEquiv)) : (a : Quot F) → (↑(colimitCocone F).pt : Type w))

Tactic:
exact Shrink.addEquiv.symm.bijective

Premises used: Shrink.addEquiv, AddEquiv.bijective, AddEquiv.symm
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
h : Small.{w, max u w} (Colimits.Quot F)
⊢ HasColimit F

Tactic:
⟨_, colimitCoconeIsColimit F⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', AddCommGrpCat.Colimits.colimitCoconeIsColimit, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
inst_2 : Small.{w, u} J
⊢ Small.{w, max u w} (Colimits.Quot F)

Tactic:
small_of_surjective (QuotientAddGroup.mk'_surjective _)

Premises used: small_of_surjective, QuotientAddGroup.mk'_surjective
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F_1 : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : Small.{w, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
⊢ HasColimit F

Tactic:
hasColimit_of_small_quot F inferInstance

Premises used: AddCommGrpCat.hasColimit_of_small_quot, inferInstance
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F_1 : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : Small.{w, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
⊢ HasColimit F

Tactic:
exact hasColimit_of_small_quot F inferInstance

Premises used: AddCommGrpCat.hasColimit_of_small_quot, inferInstance
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F_1 : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : Small.{w, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
⊢ HasColimit F

Tactic:
classical
  exact hasColimit_of_small_quot F inferInstance
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
hf :
  ∀ (x : (↑G : Type u)),
    Eq (α := (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
      ((Hom.hom (f ≫ ofHom (mk' (Hom.hom f).range)) :
            (a : (↑G : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
          x :
        (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
      ((Hom.hom 0 : (a : (↑G : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u)) x :
        (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
⊢ f ≫ ofHom (mk' (Hom.hom f).range) = 0

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑G : Type u)
⊢ Eq (α := (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
    ((Hom.hom (f ≫ ofHom (mk' (Hom.hom f).range)) :
          (a : (↑G : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
        x :
      (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
    ((Hom.hom 0 : (a : (↑G : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u)) x :
      (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑G : Type u)
⊢ Membership.mem (α := (↑H : Type u))
    (AddMonoidHom.ker (M := (↑(colimit.cocone (parallelPair f 0)).1 : Type u)) (Hom.hom (cokernel.π f)))
    ((Hom.hom f : (a : (↑G : Type u)) → (↑H : Type u)) x : (↑H : Type u))

Tactic:
cokernel.condition_apply f x

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, CategoryTheory.Limits.cokernel.condition_apply
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑G : Type u)
⊢ Membership.mem (α := (↑H : Type u))
    (AddMonoidHom.ker (M := (↑(colimit.cocone (parallelPair f 0)).1 : Type u)) (Hom.hom (cokernel.π f)))
    ((Hom.hom f : (a : (↑G : Type u)) → (↑H : Type u)) x : (↑H : Type u))

Tactic:
exact cokernel.condition_apply f x

Premises used: CategoryTheory.Limits.cokernel.condition_apply
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
⊢ cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) =
    𝟙 (cokernel f)

Tactic:
coequalizer.hom_ext ?_

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
refine :
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯)) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
⊢ cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) =
    𝟙 (cokernel f)

Tactic:
refine coequalizer.hom_ext ?_

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
simp : ofHom (mk' (Hom.hom f).range) ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) = cokernel.π f
⊢ CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯)) =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)

Tactic:
simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]

Premises used: CategoryTheory.Limits.cokernel.π_desc_assoc, CategoryTheory.Limits.coequalizer_as_cokernel, CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (mk' (Hom.hom f).range) ≫ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) = cokernel.π f

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
hf :
  ∀ (x : (↑H : Type u)),
    Eq (α := (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
      (((Hom.hom
                  (ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫
                    cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯)).comp
              (mk' (Hom.hom f).range) :
            (a : (↑H : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
          x :
        (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
      (((Hom.hom (𝟙 (of ((↑H : Type u) ⧸ (Hom.hom f).range)))).comp (mk' (Hom.hom f).range) :
            (a : (↑H : Type u)) → (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
          x :
        (↑(of ((↑H : Type u) ⧸ (Hom.hom f).range)) : Type u))
⊢ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫ cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ =
    𝟙 (of ((↑H : Type u) ⧸ (Hom.hom f).range))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑H : Type u)
⊢ Eq (α := (↑H : Type u) ⧸ (Hom.hom f).range)
    ((Hom.hom (cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯) :
          (a : (↑(cokernel f) : Type u)) → (↑H : Type u) ⧸ (Hom.hom f).range)
        ((Hom.hom (ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯)) :
            (a : (↑H : Type u) ⧸ (Hom.hom f).range) → (↑(cokernel f) : Type u))
          (↑x : (↑H : Type u) ⧸ (Hom.hom f).range)) :
      (↑H : Type u) ⧸ (Hom.hom f).range)
    ((↑x : (↑H : Type u) ⧸ (Hom.hom f).range) : (↑H : Type u) ⧸ (Hom.hom f).range)

Tactic:
QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _

Premises used: QuotientAddGroup.mk, QuotientAddGroup.induction_on
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
G H : AddCommGrpCat
f : G ⟶ H
x : (↑H : Type u)
⊢ Eq (α := (↑H : Type u) ⧸ (Hom.hom f).range)
    ((Hom.hom (cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯) :
          (a : (↑(cokernel f) : Type u)) → (↑H : Type u) ⧸ (Hom.hom f).range)
        ((Hom.hom (ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯)) :
            (a : (↑H : Type u) ⧸ (Hom.hom f).range) → (↑(cokernel f) : Type u))
          (↑x : (↑H : Type u) ⧸ (Hom.hom f).range)) :
      (↑H : Type u) ⧸ (Hom.hom f).range)
    ((↑x : (↑H : Type u) ⧸ (Hom.hom f).range) : (↑H : Type u) ⧸ (Hom.hom f).range)

Tactic:
exact QuotientAddGroup.induction_on (α := H) x <| cokernel.π_desc_apply f _ _

Premises used: CategoryTheory.Limits.cokernel.π_desc_apply
-- Module: Mathlib.Algebra.Category.Grp.EnoughInjectives
Goal:
A_ : AddCommGrpCat
⊢ Eq.{u + 1} (α := CharacterModule (↑A_ : Type u) → ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1))
    ((fun (a : (↑A_ : Type u)) (i : CharacterModule (↑A_ : Type u)) ↦
        ({ down := (i : (a : (↑A_ : Type u)) → AddCircle 1) a } : ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1)))
      0)
    0

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.EnoughInjectives
Goal:
A_ : AddCommGrpCat
⊢ ∀ (x y : (↑A_ : Type u)),
    ZeroHom.toFun
        {
          toFun := fun (a : (↑A_ : Type u)) (i : CharacterModule (↑A_ : Type u)) ↦
            { down := (i : (a : (↑A_ : Type u)) → AddCircle 1) a },
          map_zero' := ⋯ }
        (x + y) =
      HAdd.hAdd (α := CharacterModule (↑A_ : Type u) → ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1))
        (ZeroHom.toFun
          {
            toFun := fun (a : (↑A_ : Type u)) (i : CharacterModule (↑A_ : Type u)) ↦
              { down := (i : (a : (↑A_ : Type u)) → AddCircle 1) a : ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1) },
            map_zero' := ⋯ :
            ZeroHom (↑A_ : Type u) (CharacterModule (↑A_ : Type u) → ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1)) }
          x)
        (ZeroHom.toFun
          {
            toFun := fun (a : (↑A_ : Type u)) (i : CharacterModule (↑A_ : Type u)) ↦
              { down := (i : (a : (↑A_ : Type u)) → AddCircle 1) a : ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1) },
            map_zero' := ⋯ :
            ZeroHom (↑A_ : Type u) (CharacterModule (↑A_ : Type u) → ULift.{u, 0} (AddCircle (𝕜 := ℚ) 1)) }
          y)

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.EnoughInjectives
Goal:
⊢ EnoughInjectives CommGrpCat

Tactic:
EnoughInjectives.of_equivalence commGroupAddCommGroupEquivalence.functor

Premises used: CategoryTheory.EnoughInjectives.of_equivalence, commGroupAddCommGroupEquivalence, CategoryTheory.Equivalence.functor
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : Group A
inst_1 : Group B
f : A →* B
h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v
⊢ f.ker = ⊥

Tactic:
simpa using congr_arg range (h f.ker.subtype 1 (by cat_disch))

Premises used: MonoidHom.range, Subgroup.subtype, congr_arg, MonoidHom.ker, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
specialize : Eq (α := MonoidHom.{u, v} A (B ⧸ f.range)) (comp 1 f) (comp (QuotientGroup.mk' f.range) f)
specialize₁ : ∀ (h : Eq (α := B →* B ⧸ f.range) 1 (QuotientGroup.mk' f.range)), f.range = ⊤
⊢ f.range = ⊤

Tactic:
specialize h 1 (QuotientGroup.mk' _) _

Premises used: QuotientGroup.mk', OfNat.ofNat
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
h₁ :
  ∀ (x : A),
    Eq.{v + 1} (α := B ⧸ f.range)
      (((comp 1 f : MonoidHom.{u, v} A (B ⧸ f.range)) : (a : A) → B ⧸ f.range) x : B ⧸ f.range)
      (((comp (QuotientGroup.mk' f.range) f : MonoidHom.{u, v} A (B ⧸ f.range)) : (a : A) → B ⧸ f.range) x :
        B ⧸ f.range)
⊢ Eq (α := MonoidHom.{u, v} A (B ⧸ f.range)) (comp 1 f) (comp (QuotientGroup.mk' f.range) f)

Tactic:
ext1 x
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
h₁ : Membership.mem (α := B) f.range ((f : (a : A) → B) x : B)
⊢ Eq.{v + 1} (α := B ⧸ f.range) (1 : B ⧸ f.range) ((↑((f : (a : A) → B) x) : B ⧸ f.range) : B ⧸ f.range)

Tactic:
rw [show (1 : B ⧸ f.range) = (1 : B) from QuotientGroup.mk_one _, QuotientGroup.eq, inv_one,
      one_mul]

Premises used: QuotientGroup.mk_one, MonoidHom.range, inv_one, QuotientGroup.eq, one_mul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ Membership.mem (α := B) f.range ((f : (a : A) → B) x : B)

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v
x : A
⊢ Membership.mem (α := B) f.range ((f : (a : A) → B) x : B)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : Eq (α := B →* B ⧸ f.range) 1 (QuotientGroup.mk' f.range)
rw rw₁ : ker (QuotientGroup.mk' f.range) = ker (QuotientGroup.mk' f.range)
⊢ ker (QuotientGroup.mk' f.range) = ker (M := B ⧸ f.range) 1

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : Eq (α := B →* B ⧸ f.range) 1 (QuotientGroup.mk' f.range)
⊢ ker (QuotientGroup.mk' f.range) = ker (M := B ⧸ f.range) 1

Tactic:
replace h : (QuotientGroup.mk' f.range).ker = (1 : B →* B ⧸ f.range).ker := by rw [h]
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A : Type u
B : Type v
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
h : ker (QuotientGroup.mk' f.range) = ker (M := B ⧸ f.range) 1
rwa : ∀ (h : ker (QuotientGroup.mk' f.range) = ⊤), f.range = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : f.range = ⊤), f.range = ⊤
⊢ f.range = ⊤

Tactic:
rwa [ker_one, QuotientGroup.ker_mk'] at h

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

Premises used: GrpCat.Hom.hom, GrpCat.mono_iff_ker_eq_bot, MonoidHom.ker_eq_bot_iff, Iff.trans
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
x : X'
y : (↑X : Type u)
rw :
  Membership.mem (γ := Set (Set (↑B : Type u))) X
    ((b *
        Exists.choose (p := fun (y_1 : (↑B : Type u)) ↦
          (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y_1 = (↑y : Set (↑B : Type u))) ⋯) •
      (↑(Hom.hom f).range : Set (↑B : Type u)))
⊢ Membership.mem (γ := Set (Set (↑B : Type u))) X (b • (↑y : Set (↑B : Type u)))

Tactic:
rw [← y.2.choose_spec, leftCoset_assoc]

Premises used: Exists.choose_spec, leftCoset_assoc, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
x : X'
y : (↑X : Type u)
b' : (↑B : Type u) :=
  Exists.choose (p := fun (y_1 : (↑B : Type u)) ↦
    (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y_1 = (↑y : Set (↑B : Type u))) ⋯
w : (↑B : Type u)
h :
  (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) (b * b') =
    (b *
        Exists.choose (p := fun (y_1 : (↑B : Type u)) ↦
          (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y_1 = (↑y : Set (↑B : Type u))) ⋯) •
      (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ Membership.mem (γ := Set (Set (↑B : Type u))) X
    ((b *
        Exists.choose (p := fun (y_1 : (↑B : Type u)) ↦
          (fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y_1 = (↑y : Set (↑B : Type u))) ⋯) •
      (↑(Hom.hom f).range : Set (↑B : Type u)))

Tactic:
use b * b'
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b b' : (↑B : Type u)
x : X'
y : (↑X : Type u)
⊢ fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        ((b * b') • (↑y : Set (↑B : Type u))) ⋯) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (b •
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                (b' • (↑y : Set (↑B : Type u))) ⋯) :
            Set (↑B : Type u)))
        ⋯)

Tactic:
simp only [leftCoset_assoc]

Premises used: leftCoset_assoc
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : X'
y : (↑X : Type u)
⊢ fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑B : Type u)) 1 (↑y : Set (↑B : Type u))) ⋯) =
    fromCoset y

Tactic:
simp only [one_leftCoset]

Premises used: one_leftCoset
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : b ∈ (Hom.hom f).range
e_a : b • (↑(Hom.hom f).range : Set (↑B : Type u)) = (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ Eq (α := X')
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (b • (↑(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:
congr