-- 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:
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

Tactic:
obtain ⟨g, hg⟩ := toAut_surjective_isGalois F G t A

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
⊢ ∃ 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)
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).carrier), g • x = t.hom.app (X i) x

Tactic:
let px : F.obj P := is₁.inv (is₂.symm x)

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)
⊢ ∃ 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)
i : ι
⊢ ((PreservesProduct.iso F X).hom ≫ Pi.π (fun b => F.obj (X b)) i)
      ((PreservesProduct.iso F X).inv ((FintypeCat.productEquiv fun i => F.obj (X i)).symm x)) =
    x i

Tactic:
simp only [FintypeCat.comp_apply, FintypeCat.inv_hom_id_apply,
  FintypeCat.productEquiv_symm_comp_π_apply]

Result:
no goals

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)
i : ι
⊢ F.map (Pi.π X i) px = x i

Tactic:
simp only [px, is₁, is₂, ← piComparison_comp_π, ← PreservesProduct.iso_hom]

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)
i : ι
⊢ ((PreservesProduct.iso F X).hom ≫ Pi.π (fun b => F.obj (X b)) i)
      ((PreservesProduct.iso F X).inv ((FintypeCat.productEquiv fun i => F.obj (X i)).symm x)) =
    x i