Theorem: jordan_swap (Jordan/Jordan.lean)

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
⊢ G = ⊤
Tactic:
cases' Nat.lt_or_ge (Fintype.card α) 3 with hα3 hα3
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 α < 3
⊢ G = ⊤

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 = ⊤

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
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 = ⊤

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
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 = ⊤

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]
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 = ⊤

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
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)

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
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)

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]
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)

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']
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)

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 _ _
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))ᶜ)

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
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))ᶜ)

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
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))ᶜ))

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
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

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]
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

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]
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

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
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

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
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

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]
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 α
h2g : Equiv.Perm.IsSwap g
hg : g ∈ G
hα3 : Fintype.card α < 3
⊢ G = ⊤
Tactic:
rw [Nat.lt_succ_iff] at hα3
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 = ⊤

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
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 α)

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 _)
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

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)]
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

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) _
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

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]
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

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
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

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⟩]
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

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
State after:
no goals

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
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
⊢ ℕ

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]
State after:
no goals

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]
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

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]
State after:
no goals

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']
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 α

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)
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 α

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals