Theorem: is_simple_iwasawa (Jordan/Iwasawa.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ IsSimpleGroup M
Tactic:
apply IsSimpleGroup.mk
State after:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ ∀ (H : Subgroup M), Subgroup.Normal H → H = ⊥ ∨ H = ⊤

State before:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
⊢ ∀ (H : Subgroup M), Subgroup.Normal H → H = ⊥ ∨ H = ⊤
Tactic:
intro N nN
State after:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
⊢ N = ⊥ ∨ N = ⊤

State before:
case eq_bot_or_eq_top_of_normal
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
⊢ N = ⊥ ∨ N = ⊤
Tactic:
cases or_iff_not_imp_left.mpr (commutator_le_iwasawa is_qprim IwaS nN) 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))
State after:
no goals

State before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
⊢ N = ⊥ ∨ N = ⊤
Tactic:
refine' Or.inl (N.eq_bot_iff_forall.mpr fun n hn => _)
State after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ n = 1

State before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ n = 1
Tactic:
apply is_faithful.eq_of_smul_eq_smul
State after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a

State before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
⊢ ∀ (a : α), n • a = 1 • a
Tactic:
intro x
State after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x

State before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x
Tactic:
rw [one_smul]
State after:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = x

State before:
case eq_bot_or_eq_top_of_normal.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : MulAction.fixedPoints (↥N) α = ⊤
n : M
hn : n ∈ N
x : α
⊢ n • x = x
Tactic:
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩
State after:
no goals

State before:
case eq_bot_or_eq_top_of_normal.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_nontrivial : Nontrivial M
is_perfect : commutator M = ⊤
is_qprim : IsQuasipreprimitive M α
is_faithful : FaithfulSMul M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤
Tactic:
exact Or.inr (top_le_iff.mp (le_trans (ge_of_eq is_perfect) h))
State after:
no goals