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

Tactic:
let is₁ : F.obj P ≅ ∏ᶜ fun i ↦ (F.obj (X i)) := PreservesProduct.iso F 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
⊢ ∃ 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
i : ι
y : (F.obj (X i)).carrier
⊢ g • x i = t.hom.app (X i) (x i)

Tactic:
rw [← hpx i, ← IsNaturalSMul.naturality, FunctorToFintypeCat.naturality,
  ← hfa, FunctorToFintypeCat.naturality, ← IsNaturalSMul.naturality, hg]

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

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

Tactic:
let is₂ : (∏ᶜ fun i ↦ F.obj (X i) : FintypeCat) ≃ ∀ i, F.obj (X i) :=
  Limits.FintypeCat.productEquiv (fun i ↦ (F.obj (X i)))

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

Tactic:
let x (i : ι) : F.obj (X i) := (nonempty_fiber_of_isConnected F (X i)).some

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