-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha_1 : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
this : Fintype (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))
x : (F.obj X).obj
j : fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)
a :
  (obj (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) ⋙ F)
      { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }).obj
ha :
  (@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))
          _ _ _
          (F.map
              ((Limits.Cofan.mk (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI) : C)
                      (fc (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))).ι.app
                { as := j }) :
            F.obj
                (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                  { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }) ⟶
              F.obj X) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j }))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    x
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@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))
            _ _ _
            (F.map
                ((Limits.Cofan.mk (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI) : C)
                        (fc (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))).ι.app
                  { as := j }) :
              F.obj
                  (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                    { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }) ⟶
                F.obj X) :
          (a : (F.obj ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j })).obj) → (F.obj X).obj)
        ((@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))
                _ _ _
                (σ.hom.app
                    (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                      { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }) :
                  F.obj
                      (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                        { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }) ⟶
                    F.obj
                      (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                        { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) })) :
              (a : (F.obj ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j })).obj) →
                (F.obj ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j })).obj)
            a :
          (F.obj
              (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) })).obj) :
      (F.obj X).obj)
    ((@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))
            _ _ _
            (F.map
                ((Limits.Cofan.mk (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI) : C)
                        (fc (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI))).ι.app
                  { as := j }) :
              F.obj
                  (obj.{0, u₂, 0, u₁} (Discrete.functor (ff (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)))
                    { as := j : Discrete (fι (Subtype.mk (p := fun (x : C) ↦ x ∈ I) X XinI)) }) ⟶
                F.obj X) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j }))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))

Tactic:
simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]

Premises used: Subtype.mk, And.intro, Exists.intro, Set.range, rfl