-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
hf :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    f
g : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
hg :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    g
hfg :
  Eq.{u_1 + 1} (α :=
    S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) ⟶
      S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd))
    ((fun (f : Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc ⟶ Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) ↦
        S.hom.map f)
      (Subtype.mk (p :=
        fun
          (x :
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
              (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)) ↦
        Membership.mem (γ :=
          Set
            ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
              (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
          (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
          x)
        f hf))
    ((fun (f : Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc ⟶ Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) ↦
        S.hom.map f)
      (Subtype.mk (p :=
        fun
          (x :
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
              (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)) ↦
        Membership.mem (γ :=
          Set
            ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
              (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
          (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
          x)
        g hg))
⊢ Subtype.mk (p :=
      fun
        (x :
          (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)) ↦
      Membership.mem (γ :=
        Set
          ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
        (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
          (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
        x)
      f hf =
    Subtype.mk (p :=
      fun
        (x :
          (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)) ↦
      Membership.mem (γ :=
        Set
          ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
            (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
        (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
          (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
        x)
      g hg

Tactic:
Subtype.ext hfg

Premises used: Subtype.ext