internlm/Lean-Github huggingface dataset:
Theorem: jordan_swap
Proof state before:
case inr
α : 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
⊢ G = ⊤
Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le hα3
Proof state after:
case inr.intro
α : 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 α = 3 + n
⊢ G = ⊤
Theorem: jordan_swap
Proof state before:
case inr.intro
α : 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 α = 3 + n
⊢ 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 α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α ≥ 3
n : ℕ
hn : Fintype.card α = n + 3
⊢ G = ⊤
Theorem: jordan_swap
Proof state before:
case inr.intro
α : 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
⊢ G = ⊤
Tactic:
have hsc : Set.ncard ((g.support)ᶜ : Set α) = n.succ := by
  apply Nat.add_left_cancel
  rw [Set.ncard_add_ncard_compl, Nat.card_eq_fintype_card, Set.ncard_coe_Finset, Equiv.Perm.card_support_eq_two.mpr h2g, add_comm, hn]
Proof state after:
case inr.intro
α : 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
⊢ G = ⊤
Theorem: jordan_swap
Proof state before:
case inr.intro
α : 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
⊢ G = ⊤
Tactic:
apply IsMultiplyPretransitive.eq_top_of_is_full_minus_one_pretransitive
Proof state after:
case inr.intro.hmt
α : 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
⊢ IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
Theorem: jordan_swap
Proof state before:
case inr.intro.hmt
α : 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
⊢ IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
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 α
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
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 1)
Theorem: jordan_swap
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 α
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
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 1)
Tactic:
have hn' : Fintype.card α - 1 = 1 + n.succ := by
  rw [hn, add_comm 1]
  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:
case inr.intro.hmt.h
α : 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
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 1)
Theorem: jordan_swap
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 α
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
⊢ IsMultiplyPreprimitive (↥G) α (Fintype.card α - 1)
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 α
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
⊢ IsMultiplyPreprimitive (↥G) α (1 + Nat.succ n)
Theorem: jordan_swap
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 α
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
⊢ IsMultiplyPreprimitive (↥G) α (1 + Nat.succ n)
Tactic:
refine' isMultiplyPreprimitive_jordan hG hsc _ _
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
⊢ 1 + Nat.succ n < Fintype.card α

case inr.intro.hmt.h.refine'_2
α : 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
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
Theorem: jordan_swap
Proof 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 α
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
⊢ 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.IsSwap.isCycle h2g
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 α
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
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_swap
Proof 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 α
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
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'_2.hp
α : 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
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_swap
Proof state before:
case inr.intro.hmt.h.refine'_2.hp
α : 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
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_two
Proof state after:
case h.e'_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
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) = 2
Theorem: jordan_swap
Proof state before:
case h.e'_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
this :
  IsPretransitive ↥(fixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
    ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ)
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup (↥G) (↑(Equiv.Perm.support g))ᶜ) = 2
Tactic:
rw [Fintype.card_subtype]
Proof state after:
case h.e'_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
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 = 2
Theorem: jordan_swap
Proof state before:
case h.e'_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
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 = 2
Tactic:
rw [← Equiv.Perm.card_support_eq_two.mpr h2g]
Proof state after:
case h.e'_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
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_swap
Proof state before:
case h.e'_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
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 α
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
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_swap
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 α
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
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 α
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
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_swap
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 α
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
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 only [SubMulAction.mem_ofFixingSubgroup_iff, Set.mem_compl_iff, Finset.mem_coe,
  Equiv.Perm.mem_support, ne_eq, not_not, Finset.mem_univ, forall_true_left,
  Finset.mem_filter, true_and]
Proof state after:
no goals
Theorem: jordan_swap
Proof state before:
case inl
α : 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
⊢ G = ⊤
Tactic:
rw [Nat.lt_succ_iff] at hα3
Proof state after:
case inl
α : 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 α ≤ 2
⊢ G = ⊤
Theorem: jordan_swap
Proof state before:
case inl
α : 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 α ≤ 2
⊢ G = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ Fintype.card ↥G = Fintype.card (Equiv.Perm α)
Tactic:
apply le_antisymm (Fintype.card_subtype_le _)
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ Fintype.card (Equiv.Perm α) ≤ Fintype.card ↥G
Tactic:
rw [Fintype.card_equiv (Equiv.cast rfl)]
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ Nat.factorial (Fintype.card α) ≤ Fintype.card ↥G
Tactic:
refine' le_trans (Nat.factorial_le hα3) _
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ Nat.factorial 2 ≤ Fintype.card ↥G
Tactic:
rw [Nat.factorial_two]
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ 2 ≤ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ 2 ≤ Fintype.card ↥G
Tactic:
apply Nat.le_of_dvd Fintype.card_pos
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ 2 ∣ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ 2 ∣ Fintype.card ↥G
Tactic:
rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
Proof state after:
case inl.h
α : 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 α ≤ 2
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G
Theorem: jordan_swap
Proof state before:
case inl.h
α : 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 α ≤ 2
⊢ orderOf { val := g, property := hg } ∣ Fintype.card ↥G
Tactic:
exact orderOf_dvd_card
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
⊢ Set.ncard (↑(Equiv.Perm.support g))ᶜ = Nat.succ n
Tactic:
apply Nat.add_left_cancel
Proof state after:
case a
α : 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
⊢ ?n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?n + Nat.succ n

case n
α : 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
⊢ ℕ
Theorem: jordan_swap
Proof state before:
case a
α : 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
⊢ ?n + Set.ncard (↑(Equiv.Perm.support g))ᶜ = ?n + Nat.succ n

case n
α : 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
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl, Nat.card_eq_fintype_card, Set.ncard_coe_Finset, Equiv.Perm.card_support_eq_two.mpr h2g, add_comm, hn]
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
⊢ Fintype.card α - 1 = 1 + Nat.succ n
Tactic:
rw [hn, add_comm 1]
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
⊢ n + 3 - 1 = Nat.succ n + 1