Theorem: jordan_three_cycle (Jordan/Jordan.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
⊢ alternatingGroup α ≤ G
Tactic:
cases' Nat.lt_or_ge (Fintype.card α) 4 with hα4 hα4
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α < 4
⊢ alternatingGroup α ≤ G

case inr
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
⊢ alternatingGroup α ≤ G

State before:
case inr
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
⊢ alternatingGroup α ≤ G
Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le hα4
State after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = 4 + n
⊢ alternatingGroup α ≤ G

State before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = 4 + n
⊢ alternatingGroup α ≤ G
Tactic:
rw [add_comm] at hn
State after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ alternatingGroup α ≤ G

State before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ alternatingGroup α ≤ G
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_le_of_sub_two
State after:
case inr.intro.hmt
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)

State before:
case inr.intro.hmt
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ IsMultiplyPretransitive (↥G) α (Fintype.card α - 2)
Tactic:
apply IsMultiplyPreprimitive.toIsMultiplyPretransitive
State after:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 2)

State before:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 2)
Tactic:
have hn' : Fintype.card α - 2 = 1 + n.succ :=  by
  simp [hn, add_comm 1]
State after:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 2)

State before:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 2)
Tactic:
rw [hn']
State after:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsMultiplyPreprimitive (↥G) α (1 + Nat.succ n)

State before:
case inr.intro.hmt.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsMultiplyPreprimitive (↥G) α (1 + Nat.succ n)
Tactic:
refine' isMultiplyPreprimitive_jordan hG _ _ _
State after:
case inr.intro.hmt.h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set α

case inr.intro.hmt.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set.ncard ?inr.intro.hmt.h.refine'_1 = Nat.succ n

case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α

case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPreprimitive ↥(fixingSubgroup ↥G ?inr.intro.hmt.h.refine'_1)
    ↥(SubMulAction.ofFixingSubgroup ↥G ?inr.intro.hmt.h.refine'_1)

State before:
case inr.intro.hmt.h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set α

case inr.intro.hmt.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set.ncard ?inr.intro.hmt.h.refine'_1 = Nat.succ n

case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α

case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPreprimitive ↥(fixingSubgroup ↥G ?inr.intro.hmt.h.refine'_1)
    ↥(SubMulAction.ofFixingSubgroup ↥G ?inr.intro.hmt.h.refine'_1)
Tactic:
exact (g.supportᶜ : Set α)
State after:
case inr.intro.hmt.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n

case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α

case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)

State before:
case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
have : IsPretransitive _ _ := by
  apply isPretransitive_of_cycle hg
  exact Equiv.Perm.IsThreeCycle.isCycle h3g
State after:
case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)

State before:
case inr.intro.hmt.h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Tactic:
apply isPreprimitive_of_prime
State after:
case inr.intro.hmt.h.refine'_4.hp
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Nat.Prime (Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ))

State before:
case inr.intro.hmt.h.refine'_4.hp
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Nat.Prime (Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ))
Tactic:
convert Nat.prime_three
State after:
case h.e'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) = 3

State before:
case h.e'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) = 3
Tactic:
rw [Fintype.card_subtype, ← Equiv.Perm.IsThreeCycle.card_support h3g]
State after:
case h.e'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ (Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ).card =
    (Equiv.Perm.support g).card

State before:
case h.e'_1
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ (Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ).card =
    (Equiv.Perm.support g).card
Tactic:
apply congr_arg
State after:
case h.e'_1.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ =
    Equiv.Perm.support g

State before:
case h.e'_1.h
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ =
    Equiv.Perm.support g
Tactic:
ext x
State after:
case h.e'_1.h.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ ↔
    x ∈ Equiv.Perm.support g

State before:
case h.e'_1.h.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
x : α
⊢ x ∈ Finset.filter (fun x => x ∈ SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) Finset.univ ↔
    x ∈ Equiv.Perm.support g
Tactic:
simp [SubMulAction.mem_ofFixingSubgroup_iff]
State after:
no goals

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α < 4
⊢ alternatingGroup α ≤ G
Tactic:
rw [Nat.lt_succ_iff] at hα4
State after:
case inl
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ alternatingGroup α ≤ G

State before:
case inl
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ alternatingGroup α ≤ G
Tactic:
apply large_subgroup_of_perm_contains_alternating
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
Tactic:
rw [Fintype.card_perm]
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial (Fintype.card α) ≤ 2 * Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial (Fintype.card α) ≤ 2 * Fintype.card ↥G
Tactic:
apply le_trans (Nat.factorial_le hα4)
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial 3 ≤ 2 * Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ Nat.factorial 3 ≤ 2 * Fintype.card ↥G
Tactic:
change 2 * 3 ≤ _
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 2 * 3 ≤ 2 * Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 2 * 3 ≤ 2 * Fintype.card ↥G
Tactic:
simp only [mul_le_mul_left, Nat.succ_pos']
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ≤ Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ≤ Fintype.card ↥G
Tactic:
apply Nat.le_of_dvd Fintype.card_pos
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ∣ Fintype.card ↥G

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 ∣ Fintype.card ↥G
Tactic:
suffices 3 = orderOf (⟨g, hg⟩ : G) by
  rw [this]
  exact orderOf_dvd_card
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 = orderOf { val := g, property := hg }

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ 3 = orderOf { val := g, property := hg }
Tactic:
rw [← Equiv.Perm.IsThreeCycle.orderOf h3g]
State after:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ orderOf g = orderOf { val := g, property := hg }

State before:
case inl.hG
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ orderOf g = orderOf { val := g, property := hg }
Tactic:
convert orderOf_submonoid _
State after:
case h.e'_2.h.e'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ g = ↑{ val := g, property := hg }

State before:
case h.e'_2.h.e'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
⊢ g = ↑{ val := g, property := hg }
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ 3 ∣ Fintype.card ↥G
Tactic:
rw [this]
State after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≤ 3
this : 3 = orderOf { val := g, property := hg }
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G
Tactic:
exact orderOf_dvd_card
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
⊢ Fintype.card α - 2 = 1 + Nat.succ n
Tactic:
simp [hn, add_comm 1]
State after:
no goals

State before:
case inr.intro.hmt.h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
Tactic:
apply Nat.add_left_cancel
State after:
case inr.intro.hmt.h.refine'_2.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ?inr.intro.hmt.h.refine'_2.n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?inr.intro.hmt.h.refine'_2.n + Nat.succ n

case inr.intro.hmt.h.refine'_2.n
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ℕ

State before:
case inr.intro.hmt.h.refine'_2.a
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ?inr.intro.hmt.h.refine'_2.n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?inr.intro.hmt.h.refine'_2.n + Nat.succ n

case inr.intro.hmt.h.refine'_2.n
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl, Set.ncard_coe_Finset,
  Equiv.Perm.IsThreeCycle.card_support h3g,
  add_comm, Nat.card_eq_fintype_card, hn]
State after:
no goals

State before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α
Tactic:
rw [hn, Nat.succ_eq_add_one, add_comm, add_assoc]
State after:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ n + (1 + 1) < n + 4

State before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ n + (1 + 1) < n + 4
Tactic:
simp only [add_lt_add_iff_left]
State after:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + 1 < 4

State before:
case inr.intro.hmt.h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ 1 + 1 < 4
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ IsPretransitive ?m.354282 ?m.354283
Tactic:
apply isPretransitive_of_cycle hg
State after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g

State before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h3g : Equiv.Perm.IsThreeCycle g
hg : g ∈ G
hα4 : Fintype.card α ≥ 4
n : ℕ
hn : Fintype.card α = n + 4
hn' : Fintype.card α - 2 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g
Tactic:
exact Equiv.Perm.IsThreeCycle.isCycle h3g
State after:
no goals