-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
lemma action_ext_of_isGalois {t : F ⟶ F} {X : C} [IsGalois X] {g : G} (x : F.obj X)
    (hg : g • x = t.app X x) (y : F.obj X) : g • y = t.app X y

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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
x : (F.obj X).carrier
hg : g • x = t.app X x
y : (F.obj X).carrier
⊢ g • y = t.app X y

Tactic:
obtain ⟨φ, (rfl : F.map φ.hom y = x)⟩ := MulAction.exists_smul_eq (Aut X) y x

Result:
case 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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
⊢ g • y = t.app X y

Proof state:
case 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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
⊢ g • y = t.app X y

Tactic:
have : Function.Injective (F.map φ.hom) :=
  ConcreteCategory.injective_of_mono_of_preservesPullback (F.map φ.hom)

Result:
case 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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
this : Function.Injective (F.map φ.hom)
⊢ g • y = t.app X y

Proof state:
case intro.a
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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
this : Function.Injective (F.map φ.hom)
⊢ F.map φ.hom (g • y) = F.map φ.hom (t.app X y)

Tactic:
rw [IsNaturalSMul.naturality, hg, FunctorToFintypeCat.naturality]

Result:
no goals

Proof state:
case 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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
this : Function.Injective (F.map φ.hom)
⊢ g • y = t.app X y

Tactic:
apply this

Result:
case intro.a
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 : F ⟶ F
X : C
inst✝ : IsGalois X
g : G
y : (F.obj X).carrier
φ : Aut X
hg : g • F.map φ.hom y = t.app X (F.map φ.hom y)
this : Function.Injective (F.map φ.hom)
⊢ F.map φ.hom (g • y) = F.map φ.hom (t.app X y)