α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
⊢ H = ⊤
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
⊢ H = ⊤
haveI : Fact (Fintype.card α).Prime := ⟨h0⟩
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
⊢ H = ⊤
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
⊢ H = ⊤
obtain ⟨σ, hσ⟩ := exists_prime_orderOf_dvd_card (Fintype.card α) h1
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
⊢ H = ⊤
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
⊢ H = ⊤
have hσ1 : orderOf (σ : Perm α) = Fintype.card α := (orderOf_subgroup σ).trans hσ
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
⊢ H = ⊤
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
⊢ H = ⊤
have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
⊢ H = ⊤
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
⊢ H = ⊤
have hσ3 : (σ : Perm α).support = ⊤ :=
  Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1)
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ H = ⊤
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
⊢ H = ⊤
have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ ↑σ ∈ ↑H ∧ τ ∈ ↑H
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ H = ⊤
rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset, Set.singleton_subset_iff]
no goals
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x => x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card { x // x ∈ H }
h2 : τ ∈ H
h3 : IsSwap τ
this : Fact (Nat.Prime (Fintype.card α))
σ : { x // x ∈ H }
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : IsCycle ↑σ
hσ3 : support ↑σ = ⊤
hσ4 : Subgroup.closure {↑σ, τ} = ⊤
⊢ ↑σ ∈ ↑H ∧ τ ∈ ↑H
exact ⟨Subtype.mem σ, h2⟩