-- Mathlib/GroupTheory/GroupAction/Iwasawa.lean
theorem commutator_le (IwaS : IwasawaStructure M α) [IsQuasiPreprimitive M α]
    (N : Subgroup M) [nN : N.Normal] (hNX : MulAction.fixedPoints N α ≠ .univ) :
    commutator M ≤ N

Proof state:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Tactic:
have hk' : k ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_right hk

Result:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Proof state:
case intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a

Tactic:
rintro _ ⟨k, hk, rfl⟩

Result:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
⊢ commutator M ≤ N

Tactic:
have is_transN := IsQuasiPreprimitive.isPretransitive_of_normal hNX

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
⊢ commutator M ≤ N

Proof state:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Tactic:
have hg' : ↑g ∈ N ⊔ IwaS.T a := Subgroup.mem_sup_left (Subtype.mem g)

Result:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
⊢ commutator M ≤ N

Tactic:
have ntα : Nontrivial α := nontrivial_of_fixedPoints_ne_univ hNX

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤

Tactic:
rw [eq_top_iff, ← IwaS.is_generator, iSup_le_iff]

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N

Tactic:
apply nN.commutator_le_of_self_sup_commutative_eq_top ?_ (IwaS.is_comm a)

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ N ⊔ IwaS.T a = ⊤

Proof state:
case intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a

Tactic:
rw [Subgroup.smul_def, IwaS.is_conj g a]

Result:
case intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a

Proof state:
case intro.intro.intro
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
k : M
hk : k ∈ ↑(IwaS.T a)
hg' : ↑g ∈ N ⊔ IwaS.T a
hk' : k ∈ N ⊔ IwaS.T a
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut M) M) (MulAut.conj ↑g)) k ∈ N ⊔ IwaS.T a

Tactic:
exact (N ⊔ IwaS.T a).mul_mem ((N ⊔ IwaS.T a).mul_mem hg' hk') ((N ⊔ IwaS.T a).inv_mem hg')

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ ∀ (i : α), IwaS.T i ≤ N ⊔ IwaS.T a

Tactic:
intro x

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a x : α
⊢ IwaS.T x ≤ N ⊔ IwaS.T a

Proof state:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N

Tactic:
obtain a : α := Nontrivial.to_nonempty.some

Result:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N