-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.EpiMono (goal)
Goal:
A B : GrpCat
f : A ⟶ B
a : (↑A : Type u)
y : (↑B : Type u)
pos :
  ∀ (m : y ∈ (Hom.hom f).range),
    (((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)))
          ⋯)
⊢ (((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)))
        ⋯)
have neg : ∀ (m : y ∉ (Hom.hom f).range),
  (((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) sorry)) =
    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) sorry) :
            Set (↑B : Type u)))
        sorry)
Tactic: by_cases m : y ∈ f.hom.range