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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : 2 < Set.ncard s
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [Set.two_lt_ncard_iff] at hs
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ g, Equiv.Perm.IsThreeCycle g ∧ g ∈ stabilizer (Equiv.Perm α) s
Tactic:
use Equiv.swap a b * Equiv.swap a c
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.Perm.IsThreeCycle (Equiv.swap a b * Equiv.swap a c) ∧
    Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.Perm.IsThreeCycle (Equiv.swap a b * Equiv.swap a c) ∧
    Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.Perm.IsThreeCycle (Equiv.swap a b * Equiv.swap a c)

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.Perm.IsThreeCycle (Equiv.swap a b * Equiv.swap a c)

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s
Tactic:
apply Equiv.Perm.isThreeCycle_swap_mul_swap_same hab hac hbc
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) s
Tactic:
rw [← stabilizer_compl]
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) sᶜ

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Equiv.swap a b * Equiv.swap a c ∈ stabilizer (Equiv.Perm α) sᶜ
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le _ _ sᶜ.toFinite]
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ (Equiv.swap a b * Equiv.swap a c) • sᶜ ⊆ sᶜ

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ (Equiv.swap a b * Equiv.swap a c) • sᶜ ⊆ sᶜ
Tactic:
rintro _ ⟨x, hx, rfl⟩
State after:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∈ sᶜ
⊢ (fun x => (Equiv.swap a b * Equiv.swap a c) • x) x ∈ sᶜ

State before:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∈ sᶜ
⊢ (fun x => (Equiv.swap a b * Equiv.swap a c) • x) x ∈ sᶜ
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∈ sᶜ
⊢ (Equiv.swap a b) ((Equiv.swap a c) x) ∈ sᶜ

State before:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∈ sᶜ
⊢ (Equiv.swap a b) ((Equiv.swap a c) x) ∈ sᶜ
Tactic:
rw [Set.mem_compl_iff] at hx
State after:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
⊢ (Equiv.swap a b) ((Equiv.swap a c) x) ∈ sᶜ

State before:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
⊢ (Equiv.swap a b) ((Equiv.swap a c) x) ∈ sᶜ
Tactic:
suffices h : ∀ u ∈ s, x ≠ u by
  rw [Equiv.swap_apply_of_ne_of_ne (h a ha) (h c hc)]
  rw [Equiv.swap_apply_of_ne_of_ne (h a ha) (h b hb)]
  exact hx
State after:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
⊢ ∀ u ∈ s, x ≠ u

State before:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
⊢ ∀ u ∈ s, x ≠ u
Tactic:
intro u hu
State after:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
u : α
hu : u ∈ s
⊢ x ≠ u

State before:
case h.right.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
u : α
hu : u ∈ s
⊢ x ≠ u
Tactic:
exact ne_of_prop_ne hx hu
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
h : ∀ u ∈ s, x ≠ u
⊢ (Equiv.swap a b) ((Equiv.swap a c) x) ∈ sᶜ
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (h a ha) (h c hc)]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
h : ∀ u ∈ s, x ≠ u
⊢ (Equiv.swap a b) x ∈ sᶜ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
h : ∀ u ∈ s, x ≠ u
⊢ (Equiv.swap a b) x ∈ sᶜ
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (h a ha) (h b hb)]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
h : ∀ u ∈ s, x ≠ u
⊢ x ∈ sᶜ

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
x : α
hx : x ∉ s
h : ∀ u ∈ s, x ≠ u
⊢ x ∈ sᶜ
Tactic:
exact hx
State after:
no goals