internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.moves_in'
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Tactic:
use! g
Proof state after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Theorem: alternatingGroup.moves_in'
Proof state before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Tactic:
exact hGt hg
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Theorem: alternatingGroup.moves_in'
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Tactic:
exact H
Proof state after:
no goals
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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]
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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]
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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⟩
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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]
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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)]
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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)]
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer'
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'⟩
Proof 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ᶜ
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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α ⊢
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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α
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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]
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'
Proof state after:
no goals
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'
Proof 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
Theorem: alternatingGroup.has_three_cycle_of_stabilizer
Proof 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'⟩
Proof state after:
no goals
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
⊢ IsPreprimitive (↥G) α → alternatingGroup α ≤ G
Tactic:
intro hG'
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
⊢ alternatingGroup α ≤ G
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
⊢ alternatingGroup α ≤ G
Tactic:
obtain ⟨g, hg3, hg⟩ := has_three_cycle_of_stabilizer s hα
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ alternatingGroup α ≤ G
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ alternatingGroup α ≤ G
Tactic:
apply jordan_three_cycle hG' hg3
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ G
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ G
Tactic:
apply hG
Proof state after:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α
Tactic:
simp only [Subgroup.mem_inf, hg, true_and_iff]
Proof state after:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ alternatingGroup α
Theorem: alternatingGroup.le_of_isPreprimitive
Proof state before:
case intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α ≤ G
hG' : IsPreprimitive (↥G) α
g : Equiv.Perm α
hg3 : Equiv.Perm.IsThreeCycle g
hg : g ∈ stabilizer (Equiv.Perm α) s
⊢ g ∈ alternatingGroup α
Tactic:
exact Equiv.Perm.IsThreeCycle.mem_alternatingGroup hg3
Proof state after:
no goals
Theorem: alternatingGroup.isPreprimitive_of_stabilizer_lt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
⊢ IsPreprimitive (↥G) α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
h1 : Set.Nontrivial sᶜ
hα : Set.ncard s < Set.ncard sᶜ
h4 : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
hG : stabilizer (Equiv.Perm α) s ⊓ alternatingGroup α < G ⊓ alternatingGroup α
this : IsPretransitive (↥G) α
⊢ ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B