-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_3 : IsNaturalSMul F G
inst_4 : GaloisCategory.{u₁, u₂} C
inst_5 : FiberFunctor F
t : Aut F
ι : Type u_2
inst_6 : Finite ι
X : ι → C
inst_7 : ∀ (i : ι), IsGalois.{u₁, u₂} (X i)
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], MulAction.IsPretransitive.{u_1, w} G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun (i : ι) ↦ Nonempty.some ⋯
P : C := piObj.{u_2, u₂, u₁} X
is₁ : F.obj P ≅ ∏ᶜ fun (i : ι) ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i)) ≃ ((i : ι) → (F.obj (X i)).obj) :=
  FintypeCat.productEquiv fun (i : ι) ↦ F.obj (X i)
px : (F.obj P).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))
        _ _ _ is₁.inv :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (∏ᶜ fun (i : ι) ↦ F.obj (X i))) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    ((is₂.symm : (a : (i : ι) → (F.obj (X i)).obj) → (∏ᶜ fun (i : ι) ↦ F.obj (X i)).obj) x :
      ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i)))
i : ι
rw :
  (@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))
          _ _ _ (Pi.π (fun (b : ι) ↦ F.obj (X b)) i : (∏ᶜ fun (b : ι) ↦ F.obj (X b)) ⟶ F.obj (X i)) :
        (a : (∏ᶜ fun (b : ι) ↦ F.obj (X b)).obj) → (F.obj (X i)).obj)
      (((Equiv.symm (FintypeCat.productEquiv fun (i : ι) ↦ F.obj (X i)) :
              ((i : ι) → (F.obj (X i)).obj) ≃
                ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i))) :
            (a : (i : ι) → (F.obj (X i)).obj) → (∏ᶜ fun (i : ι) ↦ F.obj (X i)).obj)
          x :
        ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i))) =
    x i
⊢ (@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))
          _ _ _ (Pi.π (fun (b : ι) ↦ F.obj (X b)) i : (∏ᶜ fun (b : ι) ↦ F.obj (X b)) ⟶ F.obj (X i)) :
        (a : (∏ᶜ fun (b : ι) ↦ F.obj (X b)).obj) → (F.obj (X i)).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))
              _ _ _
              (Iso.hom (PreservesProduct.iso F X) : F.obj (piObj.{u_2, u₂, u₁} X) ⟶ ∏ᶜ fun (j : ι) ↦ F.obj (X j)) :
            (a : (F.obj (∏ᶜ X)).obj) → (∏ᶜ fun (b : ι) ↦ F.obj (X b)).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))
                  _ _ _ (Iso.inv (PreservesProduct.iso F X) : (∏ᶜ fun (i : ι) ↦ F.obj (X i)) ⟶ F.obj P) :
                (a : (∏ᶜ fun (i : ι) ↦ F.obj (X i)).obj) → (F.obj P).obj)
              (((Equiv.symm (FintypeCat.productEquiv fun (i : ι) ↦ F.obj (X i)) :
                      ((i : ι) → (F.obj (X i)).obj) ≃
                        ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i))) :
                    (a : (i : ι) → (F.obj (X i)).obj) → (∏ᶜ fun (i : ι) ↦ F.obj (X i)).obj)
                  x :
                ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (i : ι) ↦ F.obj (X i))) :
            (F.obj P).obj) :
        ObjectProperty.FullSubcategory.obj (P := Finite) (∏ᶜ fun (b : ι) ↦ F.obj (X b))) =
    x i
have rw₁ : x i = x i
Tactic: rw [FintypeCat.inv_hom_id_apply, FintypeCat.productEquiv_symm_comp_π_apply]