-- Module: Mathlib.CategoryTheory.Galois.Examples
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
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)
⊢ 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) σ))

Tactic:
ext (a : G ⧸ MulAction.stabilizer G x)

Premises used: MulAction.stabilizer