-- 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
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ 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))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
ht :
  (@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))
          _ _ _ (t.hom.app A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{w + 1} (F.obj (↑X : C)).obj
X : (↑I : Type u₁)
f : A ⟶ P
refine_1 :
  Eq (α := (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a : (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) → (F.obj (↑X : C)).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))
                _ _ _
                (t.hom.app (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) :
                  F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶
                    F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))) :
              (a : (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) →
                (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj)
            ((fun (f : A ⟶ 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))
                        _ _ _ (F.map f) :
                      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                    a :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
              f) :
          (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) :
      (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C)))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
        ((fun (f : A ⟶ 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))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
          f) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
refine_1₁ :
  Eq (α := (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a : (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) → (F.obj (↑X : C)).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 f) :
              (a : (F.obj A).obj) → (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).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))
                    _ _ _ (t.hom.app A) :
                  (a : (F.obj A).obj) → (F.obj A).obj)
                a :
              (F.obj A).obj) :
          (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) :
      (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C)))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
        ((fun (f : A ⟶ 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))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
          f) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
refine_1₂ refine_1₃ :
  Eq (α := (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a : (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) → (F.obj (↑X : C)).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 f) :
              (a : (F.obj A).obj) → (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj)
            a :
          (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj) :
      (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C)))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
        ((fun (f : A ⟶ 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))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
          f) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
⊢ Eq (α := (F.obj (↑X : C)).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))
            _ _ _ (t.hom.app (↑X : C) : F.obj (↑X : C) ⟶ F.obj (↑X : C)) :
          (a : (F.obj (↑X : C)).obj) → (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
                  F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
              (a :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C)))) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
            ((fun (f : A ⟶ 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))
                        _ _ _ (F.map f) :
                      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                    a :
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
              f) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C))) :
      (F.obj (↑X : C)).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 (Pi.π (fun (X : (↑I : Type u₁)) ↦ (↑X : C)) X) :
              F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)) ⟶ F.obj (↑X : C)) :
          (a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (∏ᶜ fun (X : (↑I : Type u₁)) ↦ (↑X : C)))) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))
        ((fun (f : A ⟶ 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))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P)))
          f) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (↑X : C)))

Tactic:
rw [NatTrans.naturality_apply, NatTrans.naturality_apply, ht]

Premises used: CategoryTheory.NatTrans.naturality_apply