-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
lemma stabilizer_normal_of_isGalois (X : C) [IsGalois X] (x : F.obj X) :
    Subgroup.Normal (MulAction.stabilizer (Aut F) x) where
  conj_mem n ninstab g

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : F.map φ.hom x = g⁻¹ • x
⊢ g • g⁻¹ • x = x

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ (g * n * g⁻¹) • x = x

Tactic:
show g • n • (g⁻¹ • x) = x

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ g • n • g⁻¹ • x = x

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ g * n * g⁻¹ ∈ MulAction.stabilizer (Aut F) x

Tactic:
rw [MulAction.mem_stabilizer_iff]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ (g * n * g⁻¹) • x = x

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
⊢ g • n • g⁻¹ • x = x

Tactic:
have : ∃ (φ : Aut X), F.map φ.hom x = g⁻¹ • x :=
  MulAction.IsPretransitive.exists_smul_eq x (g⁻¹ • x)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
this : ∃ φ, F.map φ.hom x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
this : ∃ φ, F.map φ.hom x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x

Tactic:
obtain ⟨φ, h⟩ := this

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : F.map φ.hom x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : F.map φ.hom x = g⁻¹ • x
⊢ g • n • g⁻¹ • x = x

Tactic:
rw [← h, mulAction_naturality, ninstab, h]

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x : (F.obj X).carrier
n : Aut F
ninstab : n ∈ MulAction.stabilizer (Aut F) x
g : Aut F
φ : Aut X
h : F.map φ.hom x = g⁻¹ • x
⊢ g • g⁻¹ • x = x