internlm/Lean-Github huggingface dataset:
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
⊢ n + 3 - 1 = Nat.succ n + 1
Tactic:
simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, add_eq_zero, and_false, tsub_zero]
Proof state after:
no goals
Theorem: jordan_swap
Proof 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 α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ 1 + Nat.succ n < Fintype.card α
Tactic:
rw [← hn']
Proof 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 α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ Fintype.card α - 1 < Fintype.card α
Theorem: jordan_swap
Proof 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 α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ Fintype.card α - 1 < Fintype.card α
Tactic:
apply Nat.sub_lt _ (by norm_num)
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ 0 < Fintype.card α
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ 0 < Fintype.card α
Tactic:
apply lt_of_lt_of_le (by norm_num) hα3
Proof state after:
no goals
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ IsPretransitive ?m.318640 ?m.318641
Tactic:
apply isPretransitive_of_cycle hg
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g
Theorem: jordan_swap
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
G : Subgroup (Equiv.Perm α)
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Equiv.Perm α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
hsc : Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
hn' : Fintype.card α - 1 = 1 + Nat.succ n
⊢ Equiv.Perm.IsCycle g
Tactic:
exact Equiv.Perm.IsSwap.isCycle h2g
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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)
Theorem: jordan_three_cycle
Proof 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
Proof 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)
Theorem: jordan_three_cycle
Proof 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]
Proof 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)
Theorem: jordan_three_cycle
Proof 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']
Proof 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)
Theorem: jordan_three_cycle
Proof 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 _ _ _
Proof 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)
Theorem: jordan_three_cycle
Proof 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 α)
Proof 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))ᶜ)
Theorem: jordan_three_cycle
Proof 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
Proof 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))ᶜ)
Theorem: jordan_three_cycle
Proof 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
Proof 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))ᶜ))
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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]
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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]
Proof state after:
no goals
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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
Proof 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
Theorem: jordan_three_cycle
Proof 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]
Proof 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