-- Module: Mathlib.CategoryTheory.Galois.EssSurj
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
X : Action FintypeCat G
inst_4 : TopologicalSpace X.V.obj
inst_5 : DiscreteTopology.{u_1} X.V.obj
inst_6 : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this_1 : (i : ι) → TopologicalSpace (f i).V.obj := fun (i : ι) ↦ ⊥
this : ∀ (i : ι), DiscreteTopology.{u_1} (f i).V.obj
i : ι
r : f i ⟶ X := Sigma.ι f i ≫ u.hom
r'' : (p : G × (f i).V.obj) → G × X.V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (p.1,
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (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))
            _ _ _ r.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
        p.2)
q : (p : G × X.V.obj) → X.V.obj :=
  fun (p : G × X.V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
      p.2
q' : (p : G × (f i).V.obj) → (f i).V.obj :=
  fun (p : G × (f i).V.obj) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) (((f i).ρ : (a : G) → End (f i).V) p.1)) :
        (a : (fun (X : Type u_1) ↦ X) (f i).V.obj) → (fun (X : Type u_1) ↦ X) (f i).V.obj)
      p.2
h :
  ∀ (p : G × (f i).V.obj),
    (q ∘ r'') p =
      ((⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (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))
                _ _ _ r.hom) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
          q')
        p
⊢ q ∘ r'' =
    (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (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))
            _ _ _ r.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (f i).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) ∘
      q'

Tactic:
ext (p : G × (f i).V)

Premises used: Action.V