-- 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')
rw :
  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)
          (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯) :
      X')
rw₁ :
  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')
    ((((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')
rw₂ rw₃ :
  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')
    ((((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')
⊢ 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)
        (b • (↑(Hom.hom f).range : Set (↑B : Type u))) ⋯))

Tactic:
rw [← eq1, ← eq2, DFunLike.congr_fun hb]

Premises used: DFunLike.congr_fun