-- Mathlib/GroupTheory/GroupAction/Iwasawa.lean
theorem isSimpleGroup [Nontrivial M] (is_perfect : commutator M = ⊤)
    [IsQuasiPreprimitive M α] (IwaS : IwasawaStructure M α) (is_faithful : FaithfulSMul M α) :
    IsSimpleGroup M

Proof state:
case eq_bot_or_eq_top_of_normal.inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤

Tactic:
exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Result:
no goals

Proof state:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ n = 1

Tactic:
apply is_faithful.eq_of_smul_eq_smul

Result:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a

Proof state:
case eq_bot_or_eq_top_of_normal
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ ∀ (H : Subgroup M), H.Normal → H = ⊥ ∨ H = ⊤

Tactic:
intro N nN

Result:
case eq_bot_or_eq_top_of_normal
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
⊢ N = ⊥ ∨ N = ⊤

Proof state:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x

Tactic:
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩

Result:
no goals

Proof state:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a

Tactic:
intro x

Result:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x

Proof state:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
⊢ N = ⊥ ∨ N = ⊤

Tactic:
refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)

Result:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
⊢ n = 1

Proof state:
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ IsSimpleGroup M

Tactic:
apply IsSimpleGroup.mk

Result:
case eq_bot_or_eq_top_of_normal
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
⊢ ∀ (H : Subgroup M), H.Normal → H = ⊥ ∨ H = ⊤

Proof state:
case eq_bot_or_eq_top_of_normal
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
⊢ N = ⊥ ∨ N = ⊤

Tactic:
cases or_iff_not_imp_left.mpr (IwaS.commutator_le N) with
| inl h =>
  refine Or.inl (N.eq_bot_iff_forall.mpr fun n hn => ?_)
  apply is_faithful.eq_of_smul_eq_smul
  intro x
  rw [one_smul]
  exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
 | inr h => exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))

Result:
no goals

Proof state:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x

Tactic:
rw [one_smul]

Result:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x