Theorem: Equiv.Perm.Equiv.Perm.normal_subgroups (Jordan/PermIwasawa.lean)

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ alternatingGroup α ≤ N
Tactic:
rw [← alternatingGroup.commutator_group_eq hα]
State after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ commutator (Perm α) ≤ N

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ commutator (Perm α) ≤ N
Tactic:
refine' commutator_le_iwasawa _ iwasawa_two hnN _
State after:
case refine'_1
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsQuasipreprimitive (Perm α) ↑(Nat.Combination α 2)

case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ fixedPoints ↥N ↑(Nat.Combination α 2) ≠ ⊤

State before:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ fixedPoints ↥N ↑(Nat.Combination α 2) ≠ ⊤
Tactic:
intro h
State after:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
⊢ False

State before:
case refine'_2
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
⊢ False
Tactic:
obtain ⟨g, hgN, hg_ne⟩ := N.nontrivial_iff_exists_ne_one.mp ntN
State after:
case refine'_2.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ False

State before:
case refine'_2.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ False
Tactic:
obtain ⟨s, hs⟩ := Nat.combination.mulAction_faithful
  (G := Equiv.Perm α) (α := α) (g := g) 2
  (by norm_num)
  (by rw [PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe]
      apply le_trans (by norm_num) hα)
  (by exact hg_ne)
State after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ False

State before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ False
Tactic:
apply hs
State after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ g • s = s

State before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ g • s = s
Tactic:
suffices s ∈ fixedPoints N (Nat.Combination α 2) by
  rw [mem_fixedPoints] at this
  exact this ⟨g, hgN⟩
State after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)

State before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)
Tactic:
rw [h, Set.top_eq_univ]
State after:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ _root_.Set.univ

State before:
case refine'_2.intro.intro.intro
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
⊢ s ∈ _root_.Set.univ
Tactic:
apply Set.mem_univ
State after:
no goals

State before:
case refine'_1
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsQuasipreprimitive (Perm α) ↑(Nat.Combination α 2)
Tactic:
apply IsPreprimitive.isQuasipreprimitive
State after:
case refine'_1.hGX
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsPreprimitive (Perm α) ↑(Nat.Combination α 2)

State before:
case refine'_1.hGX
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ IsPreprimitive (Perm α) ↑(Nat.Combination α 2)
Tactic:
apply Nat.Combination_isPreprimitive
State after:
case refine'_1.hGX.h_one_le
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2

State before:
case refine'_1.hGX.h_one_le
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 1 ≤ 2

case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
norm_num
State after:
case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2

State before:
case refine'_1.hGX.hn
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < Fintype.card α

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
apply lt_of_lt_of_le _ hα
State after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < 5

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 < 5

case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
norm_num
State after:
case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2

State before:
case refine'_1.hGX.hα
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ Fintype.card α ≠ 2 * 2
Tactic:
apply ne_of_gt
State after:
case refine'_1.hGX.hα.h
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < Fintype.card α

State before:
case refine'_1.hGX.hα.h
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < Fintype.card α
Tactic:
apply lt_of_lt_of_le _ hα
State after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < 5

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
⊢ 2 * 2 < 5
Tactic:
norm_num
State after:
no goals

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ ↑(Nat.succ 2) ≤ PartENat.card α
Tactic:
rw [PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe]
State after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ Fintype.card α

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ Fintype.card α
Tactic:
apply le_trans (by norm_num) hα
State after:
no goals

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ Nat.succ 2 ≤ 5
Tactic:
norm_num
State after:
no goals

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
⊢ toPerm g ≠ 1
Tactic:
exact hg_ne
State after:
no goals

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : s ∈ fixedPoints ↥N ↑(Nat.Combination α 2)
⊢ g • s = s
Tactic:
rw [mem_fixedPoints] at this
State after:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : ∀ (m : ↥N), m • s = s
⊢ g • s = s

State before:
α✝ : Type ?u.55854
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 5 ≤ Fintype.card α
N : Subgroup (Perm α)
hnN : Subgroup.Normal N
ntN : Nontrivial ↥N
h : fixedPoints ↥N ↑(Nat.Combination α 2) = ⊤
g : Perm α
hgN : g ∈ N
hg_ne : g ≠ 1
s : ↑(Nat.Combination α 2)
hs : g • s ≠ s
this : ∀ (m : ↥N), m • s = s
⊢ g • s = s
Tactic:
exact this ⟨g, hgN⟩
State after:
no goals