-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
lemma toAut_surjective_isGalois_finite_family (t : Aut F) {ι : Type*} [Finite ι] (X : ι → C)
    [∀ i, IsGalois (X i)] (h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X)) :
    ∃ (g : G), ∀ (i : ι) (x : F.obj (X i)), g • x = t.hom.app (X i) x

Proof state:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Tactic:
have hpx (i : ι) : F.map (Pi.π X i) px = x i := by
  simp only [px, is₁, is₂, ← piComparison_comp_π, ← PreservesProduct.iso_hom]
  simp only [FintypeCat.comp_apply, FintypeCat.inv_hom_id_apply,
    FintypeCat.productEquiv_symm_comp_π_apply]

Result:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
hpx : ∀ (i : ι), F.map (Pi.π X i) px = x i
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Proof state:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
hpx : ∀ (i : ι), F.map (Pi.π X i) px = x i
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Tactic:
obtain ⟨A, f, a, _, hfa⟩ := exists_hom_from_galois_of_fiber F P px

Result:
case intro.intro.intro.intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
hpx : ∀ (i : ι), F.map (Pi.π X i) px = x i
A : C
f : A ⟶ P
a : (F.obj A).carrier
left✝ : IsGalois A
hfa : F.map f a = px
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Proof state:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Tactic:
letI : Fintype ι := Fintype.ofFinite ι

Result:
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Proof state:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
hpx : ∀ (i : ι), F.map (Pi.π X i) px = x i
A : C
f : A ⟶ P
a : (F.obj A).carrier
left✝ : IsGalois A
hfa : F.map f a = px
g : G
hg : ∀ (x : (F.obj A).carrier), g • x = t.hom.app A x
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Tactic:
refine ⟨g, fun i y ↦ action_ext_of_isGalois F (x i) ?_ _⟩

Result:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [inst : IsGalois X], MulAction.IsPretransitive G (F.obj X).carrier
x : (i : ι) → (F.obj (X i)).carrier := fun i => ⋯.some
P : C := ∏ᶜ X
this : Fintype ι := Fintype.ofFinite ι
is₁ : F.obj P ≅ ∏ᶜ fun i => F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i => F.obj (X i)).carrier ≃ ((i : ι) → (F.obj (X i)).carrier) :=
  FintypeCat.productEquiv fun i => F.obj (X i)
px : (F.obj P).carrier := is₁.inv (is₂.symm x)
hpx : ∀ (i : ι), F.map (Pi.π X i) px = x i
A : C
f : A ⟶ P
a : (F.obj A).carrier
left✝ : IsGalois A
hfa : F.map f a = px
g : G
hg : ∀ (x : (F.obj A).carrier), g • x = t.hom.app A x
i : ι
y : (F.obj (X i)).carrier
⊢ g • x i = t.hom.app (X i) (x i)