Theorem: alternatingGroup.has_three_cycle_of_stabilizer (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
cases' Nat.lt_or_ge 2 (Set.ncard s) with hs hs
State after:
case inl
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 < Set.ncard s
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
case inl
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 < Set.ncard s
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
exact has_three_cycle_of_stabilizer' s hs
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
suffices hs' : _ by
  obtain ⟨g, hg, hg'⟩ := has_three_cycle_of_stabilizer' (sᶜ) hs'
  use g
  rw [stabilizer_compl] at hg'
  exact ⟨hg, hg'⟩
State after:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
⊢ 2 < Set.ncard sᶜ

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
⊢ 2 < Set.ncard sᶜ
Tactic:
rw [lt_iff_not_le] at hα ⊢
State after:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
⊢ ¬Set.ncard sᶜ ≤ 2

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
⊢ ¬Set.ncard sᶜ ≤ 2
Tactic:
intro hs'
State after:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ False

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ False
Tactic:
apply hα
State after:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ Fintype.card α ≤ 4

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ Fintype.card α ≤ 4
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s]
State after:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ Set.ncard s + Set.ncard sᶜ ≤ 4

State before:
case inr
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : ¬Fintype.card α ≤ 4
hs : 2 ≥ Set.ncard s
hs' : Set.ncard sᶜ ≤ 2
⊢ Set.ncard s + Set.ncard sᶜ ≤ 4
Tactic:
exact Nat.add_le_add hs hs'
State after:
no goals

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : ?m.50651
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
obtain ⟨g, hg, hg'⟩ := has_three_cycle_of_stabilizer' (sᶜ) hs'
State after:
case intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) sᶜ
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
case intro.intro
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) sᶜ
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
use g
State after:
case h
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) sᶜ
⊢ Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
case h
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) sᶜ
⊢ Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [stabilizer_compl] at hg'
State after:
case h
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) s
⊢ Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
case h
α : Type u_1
inst✝² : Fintype α
inst✝¹ inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
hs : 2 ≥ Set.ncard s
hs' : 2 < Set.ncard sᶜ
g : Equiv.Perm α
hg : Equiv.Perm.IsThreeCycle g
hg' : g ∈ stabilizer (Equiv.Perm α) s
⊢ Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
exact ⟨hg, hg'⟩
State after:
no goals