awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
⊢ fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) ≠
    ∞

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
refine : ∀ (r : x * b ∈ (Hom.hom f).range), b ∈ (Hom.hom f).range
⊢ Eq (α := X')
    ((Equiv.swap
            (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)) ⋯))
            ∞ :
          (a : X') → X')
        (fromCoset
          (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
            ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯)) :
      X')
    (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((x * b) • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')

Tactic:
refine Equiv.swap_apply_of_ne_of_ne (fromCoset_ne_of_nin_range _ fun r => hb ?_) (by simp)

Premises used: GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range, Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ x⁻¹ * (x * b) ∈ (Hom.hom f).range

Tactic:
Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r

Premises used: Subgroup.inv_mem, Subgroup.mul_mem
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
h : b = x⁻¹ * (x * b)
⊢ b ∈ (Hom.hom f).range

Tactic:
convert! Subgroup.mul_mem _ (Subgroup.inv_mem _ hx) r

Premises used: Subgroup.inv_mem, Subgroup.mul_mem
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
x : (↑B : Type u)
hx : x ∈ (Hom.hom f).range
b : (↑B : Type u)
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
h : b = x⁻¹ * x * b
h₁ : b = 1 * b
h₂ h₃ : b = b
⊢ b = x⁻¹ * (x * b)

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Premises used: inv_mul_cancel, mul_assoc, one_mul
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
⊢ (↑(Hom.hom f).range : Set (↑B : Type u)) =
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}

Tactic:
Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩

Premises used: Set.ext, Iff.intro, by_contradiction
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
refine_1 :
  ∀ b ∈ (↑(Hom.hom f).range : Set (↑B : Type u)),
    Membership.mem (γ := Set (↑B : Type u))
      {x : (↑B : Type u) |
        Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
      b
refine_2 :
  ∀ (b : (↑B : Type u))
    (hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX'))
    (r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))), False
⊢ (↑(Hom.hom f).range : Set (↑B : Type u)) =
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}

Tactic:
refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
refine_1 :
  Eq (α := SX')
    ((h : (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')
    ((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')
⊢ Membership.mem (α := (↑B : Type u)) (γ := Set (↑B : Type u))
    {x : (↑B : Type u) |
      Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') x : SX') ((g : (a : (↑B : Type u)) → SX') x : SX')}
    ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))

Tactic:
change h (f a) = g (f a)
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
refine_1 :
  ∀ (y : (↑B : Type u)),
    Eq (α := X')
      ((((h : (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')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) :
        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')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
              ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) :
        X')
refine_1₁ :
  Eq (α := X')
    ((((h : (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')
    ((((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')
⊢ Eq (α := SX')
    ((h : (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')
    ((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')

Tactic:
ext ⟨⟨_, ⟨y, rfl⟩⟩⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∈ (Hom.hom f).range
pos :
  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)) ⋯) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑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))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)
⊢ (((h : (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')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑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))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)

Tactic:
rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]

Premises used: GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset'
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∈ (Hom.hom f).range
⊢ Eq (α := 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)) ⋯))
    (fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑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))
          (y • (↑(Hom.hom f).range : Set (↑B : Type u))))
        ⋯))

Tactic:
simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m), smul_smul]

Premises used: smul_smul, GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range, Exists.intro, Subgroup.mul_mem, rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∉ (Hom.hom f).range
neg :
  fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HMul.hMul (α := (↑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))
            y •
          (↑(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)
        (HSMul.hSMul (α := (↑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))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)
⊢ (((h : (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')
      (fromCoset
        (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
          ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯)) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HSMul.hSMul (α := (↑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))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            Set (↑B : Type u)))
        ⋯)

Tactic:
rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]

Premises used: CategoryTheory.ConcreteCategory.hom, Exists.intro, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
m : y ∉ (Hom.hom f).range
⊢ fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
        (HMul.hMul (α := (↑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))
            y •
          (↑(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)
        (HSMul.hSMul (α := (↑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))
          (↑(Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦ Membership.mem (γ := Set (Set (↑B : Type u))) X x)
                ((fun (x : (↑B : Type u)) ↦ x • (↑(Hom.hom f).range : Set (↑B : Type u))) y) ⋯) :
            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
a : (↑A : Type u)
refine_1 :
  Eq (α := X')
    ((((h : (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')
refine_1₁ refine_1₂ : Eq.{u + 1} (α := X') ∞ ∞
⊢ Eq (α := X')
    ((((h : (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')
    ((((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')

Tactic:
rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]

Premises used: CategoryTheory.ConcreteCategory.hom, GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity, GrpCat.SurjectiveOfEpiAuxs.h_apply_infinity, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')
r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ (Equiv.swap
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
              Membership.mem (γ := Set (Set (↑B : Type u)))
                (Set.range fun (x : (↑B : Type u)) ↦
                  HSMul.hSMul (β := Set (↑B : Type u)) x
                    (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))))
                x)
              (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))) ⋯))
          ∞ :
        (a : X') → X')
      ((((g : (a : (↑B : Type u)) → SX') b : SX') : (a : X') → X')
        ((Equiv.swap
              (fromCoset
                (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
                  Membership.mem (γ := Set (Set (↑B : Type u)))
                    (Set.range fun (x : (↑B : Type u)) ↦
                      HSMul.hSMul (β := Set (↑B : Type u)) x
                        (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))))
                    x)
                  (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))) ⋯))
              ∞ :
            (a : X') → X')
          (fromCoset
            (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
              Membership.mem (γ := Set (Set (↑B : Type u)))
                (Set.range fun (x : (↑B : Type u)) ↦
                  HSMul.hSMul (β := Set (↑B : Type u)) x
                    (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))))
                x)
              (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))) ⋯)))) =
    fromCoset
      (Subtype.mk (p := fun (x : Set (↑B : Type u)) ↦
        Membership.mem (γ := Set (Set (↑B : Type u)))
          (Set.range fun (x : (↑B : Type u)) ↦
            HSMul.hSMul (β := Set (↑B : Type u)) x
              (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))))
          x)
        (Set.range (ι := (↑A : Type u)) (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))) ⋯)

Tactic:
simp [g_apply_infinity f]

Premises used: GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')
r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))
⊢ Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : 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')
    (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:
have eq1 : (h b) (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) =
        fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩ := by
      change ((τ).symm.trans (g b)).trans τ _ = _
      dsimp [tau]
      simp [g_apply_infinity f]
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')
r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : 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')
    (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')
    ((((g : (a : (↑B : Type u)) → SX') b : 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')
    (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))) ⋯) :
      X')

Tactic:
have eq2 :
        g b (fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩) = fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ :=
      rfl
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
b : (↑B : Type u)
hb : Eq (α := SX') ((h : (a : (↑B : Type u)) → SX') b : SX') ((g : (a : (↑B : Type u)) → SX') b : SX')
r : b ∉ (↑(Hom.hom f).range : Set (↑B : Type u))
eq1 :
  Eq (α := X')
    ((((h : (a : (↑B : Type u)) → SX') b : 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')
    (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')
eq2 :
  Eq (α := X')
    ((((g : (a : (↑B : Type u)) → SX') b : 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')
    (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))) ⋯) :
      X')
⊢ False

Tactic:
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

Premises used: GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range, Ne.symm
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
hf :
  ∀ (a : (↑A : Type u)) (x : X'),
    Eq (α := X')
      ((((Hom.hom (f ≫ ofHom g) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
          x :
        X')
      ((((Hom.hom (f ≫ ofHom h) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
          x :
        X')
⊢ f ≫ ofHom g = f ≫ ofHom h

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
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')
    ((((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')
⊢ Eq (α := X')
    ((((Hom.hom (f ≫ ofHom g) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')
    ((((Hom.hom (f ≫ ofHom h) : (a : (↑A : Type u)) → (↑(of SX') : Type u)) a : (↑(of SX') : Type u)) : (a : X') → X')
        x :
      X')

Tactic:
simp only [hom_comp, hom_ofHom, MonoidHom.coe_comp, Function.comp_apply]

Premises used: MonoidHom.coe_comp, GrpCat.hom_ofHom, Function.comp_apply, GrpCat.hom_comp
-- Module: Mathlib.Algebra.Category.Grp.EpiMono
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
x : X'
rw :
  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))
⊢ 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:
rw [← agree]

Premises used: GrpCat.SurjectiveOfEpiAuxs.agree