internlm/Lean-Github huggingface dataset:
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
case hn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ ?n

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑?n ≤ PartENat.card α

case n
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ℕ
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state after:
case hmn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ Fintype.card α - 2

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
case hmn
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ Fintype.card α - 2

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
apply le_trans _ (Nat.sub_le_sub_right h 2)
Proof state after:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ 3 - 2

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 1 ≤ 3 - 2

case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
norm_num
Proof state after:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
simp only [ge_iff_le, PartENat.card_eq_coe_fintype_card, PartENat.coe_le_coe,
  tsub_le_iff_right, le_add_iff_nonneg_right]
Proof state after:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 0 ≤ 2
Theorem: MulAction.alternatingGroup.isPretransitive
Proof state before:
case hα
M : Type ?u.287770
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Fintype.card α
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
⊢ IsTrivialBlock B
Tactic:
cases' le_or_lt (Fintype.card α) 2 with h2 h2
Proof state after:
case inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Fintype.card α ≤ 2
⊢ IsTrivialBlock B

case inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
⊢ IsTrivialBlock B
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
⊢ IsTrivialBlock B
Tactic:
cases' le_or_lt (Fintype.card α) 3 with h3 h4
Proof state after:
case inr.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
⊢ IsTrivialBlock B

case inr.inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsTrivialBlock B
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsTrivialBlock B
Tactic:
apply IsPreprimitive.has_trivial_blocks ?_ hB
Proof state after:
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
apply IsMultiplyPretransitive.isPreprimitive_of_two
Proof state after:
case h2
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case h2
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
Tactic:
apply isMultiplyPretransitive_of_higher
Proof state after:
case h2.hn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?h2.n

case h2.hmn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ ?h2.n

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑?h2.n ≤ PartENat.card α

case h2.n
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ℕ
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case h2.hn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?h2.n

case h2.hmn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ ?h2.n

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑?h2.n ≤ PartENat.card α

case h2.n
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ℕ
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state after:
case h2.hmn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ Fintype.card α - 2

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case h2.hmn
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ Fintype.card α - 2

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
apply le_trans _ (Nat.sub_le_sub_right h4 2)
Proof state after:
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ succ 3 - 2

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ 2 ≤ succ 3 - 2

case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
norm_num
Proof state after:
case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case h2.hα
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h4 : 3 < Fintype.card α
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
simp only [PartENat.card_eq_coe_fintype_card, cast_le, tsub_le_iff_right, le_add_iff_nonneg_right,
  _root_.zero_le]
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Fintype.card α ≤ 2
⊢ IsTrivialBlock B
Tactic:
exact IsTrivialBlock.of_card_le_2 h2 B
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
⊢ IsTrivialBlock B
Tactic:
have h3' : Fintype.card α = 3 := le_antisymm h3 h2
Proof state after:
case inr.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
⊢ IsTrivialBlock B
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
⊢ IsTrivialBlock B
Tactic:
cases' le_or_lt (Fintype.card B) 1 with h1 h2
Proof state after:
case inr.inl.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B

case inr.inl.inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inl
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
Proof state after:
case inr.inl.inl.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inl.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B
Tactic:
rw [← Set.subsingleton_coe, ← Fintype.card_le_one_iff_subsingleton]
Proof state after:
case inr.inl.inl.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inl.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1
Tactic:
exact h1
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_right
Proof state after:
case inr.inl.inr.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : 1 < Fintype.card ↑B
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : 1 < Fintype.card ↑B
⊢ B = ⊤
Tactic:
rw [Fintype.one_lt_card_iff] at h2
Proof state after:
case inr.inl.inr.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : ∃ a b, a ≠ b
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2✝ : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
h2 : ∃ a b, a ≠ b
⊢ B = ⊤
Tactic:
obtain ⟨⟨a, ha⟩, ⟨b, hb⟩, hab⟩ := h2
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : { val := a, property := ha } ≠ { val := b, property := hb }
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h.intro.mk.intro.mk
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : { val := a, property := ha } ≠ { val := b, property := hb }
⊢ B = ⊤
Tactic:
simp only [Ne.def, Subtype.mk_eq_mk] at hab
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h.intro.mk.intro.mk
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
this : ∃ c, c ∉ {a, b}
⊢ B = ⊤
Tactic:
obtain ⟨c, hc⟩ := this
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : c ∉ {a, b}
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : c ∉ {a, b}
⊢ B = ⊤
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hc
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
⊢ B = ⊤
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
⊢ B = ⊤
Tactic:
suffices ({a, b, c} : Finset α) = Finset.univ by
  rw [eq_top_iff]
  rw [Set.top_eq_univ, ← Finset.coe_univ, ← this]
  intro x hx
  simp only [Finset.coe_insert, Finset.coe_singleton, Set.mem_insert_iff,
    Set.mem_singleton_iff] at hx
  cases' hx with hxa hx
  rw [hxa]; exact ha
  cases' hx with hxb hxc
  rw [hxb]; exact hb
  rw [hxc]
  let g : alternatingGroup α :=
    ⟨Equiv.swap a b * Equiv.swap c b,by  rw [Equiv.Perm.mem_alternatingGroup]
        rw [Equiv.Perm.sign_mul]
        rw [Equiv.Perm.sign_swap hab]
        rw [Equiv.Perm.sign_swap hc.right]
        simp only [Int.units_mul_self]⟩
  suffices g • B = B by
    rw [← this]
    use b
    apply And.intro hb
    change (Equiv.swap a b * Equiv.swap c b) • b = c
    simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
    rw [Equiv.swap_apply_right]
    rw [Equiv.swap_apply_of_ne_of_ne hc.left hc.right]
  apply hB.def_mem ha
  change (Equiv.swap a b * Equiv.swap c b) • a ∈ B
  simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
  rw [Equiv.swap_apply_of_ne_of_ne (ne_comm.mp hc.left) hab]
  rw [Equiv.swap_apply_left]
  exact hb
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
⊢ {a, b, c} = Finset.univ
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof state before:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
⊢ {a, b, c} = Finset.univ
Tactic:
rw [← Finset.card_eq_iff_eq_univ, h3']
Proof state after:
case inr.inl.inr.h.intro.mk.intro.mk.intro
M : Type ?u.291196
α : Type u_1
inst✝³ : Group M
inst✝² : MulAction M α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Fintype.card α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
⊢ {a, b, c}.card = 3