-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x : X.V.obj
inst_2 : Fintype (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x))
this : MulAction.IsPretransitive G X.V.obj
e : X.V.obj ≃ HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x) :=
  Equiv.trans (Equiv.symm (Equiv.Set.univ X.V.obj))
    (Equiv.trans (Equiv.setCongr (s := Set.univ) (t := MulAction.orbit G x) ⋯)
      (MulAction.orbitEquivQuotientStabilizer G x))
σ : G
⊢ Eq.{u + 1} (α :=
    Action.V
        (Action.FintypeCat.ofMulAction G
          (FintypeCat.of (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)))) ⟶
      X.V)
    (CategoryStruct.comp (Y :=
      Action.V
        (Action.FintypeCat.ofMulAction G
          (FintypeCat.of (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)))))
      ((Action.ρ
            (Action.FintypeCat.ofMulAction G
              (FintypeCat.of (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)))) :
          (a : G) → End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V)
        σ)
      (Iso.hom
        ((FintypeCat.equivEquivIso :
            (a : (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V.obj ≃ X.V.obj) →
              (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V ≅ X.V)
          e.symm)))
    (CategoryStruct.comp (Y := X.V)
      (Iso.hom
        ((FintypeCat.equivEquivIso :
            (a : (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V.obj ≃ X.V.obj) →
              (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V ≅ X.V)
          e.symm))
      ((X.ρ : (a : G) → End X.V) σ))
have h : ∀ (a : HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
    ((@ConcreteCategory.hom _ _ (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (CategoryStruct.comp (Y :=
              Action.V
                (Action.FintypeCat.ofMulAction G
                  (FintypeCat.of (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)))))
              ((Action.ρ
                    (Action.FintypeCat.ofMulAction G
                      (FintypeCat.of (HasQuotient.Quotient G (B := Subgroup G) (MulAction.stabilizer G x)))) :
                  (a : G) → End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V)
                σ)
              (Iso.hom
                ((FintypeCat.equivEquivIso :
                    (a :
                        (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V.obj ≃
                          X.V.obj) →
                      (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V ≅ X.V)
                  e.symm))) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
    ((@ConcreteCategory.hom _ _ (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (CategoryStruct.comp (Y := X.V)
              (Iso.hom
                ((FintypeCat.equivEquivIso :
                    (a :
                        (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V.obj ≃
                          X.V.obj) →
                      (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V ≅ X.V)
                  e.symm))
              ((X.ρ : (a : G) → End X.V) σ)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
Tactic: ext (a : G ⧸ MulAction.stabilizer G x)