Theorem: MulAction.alternatingGroup.has_trivial_blocks (Jordan/MultipleTransitivity.lean)

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
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

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
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

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
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 α)) α

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
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

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
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 α
⊢ ℕ

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
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 α

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)
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 α

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
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 α

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]
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
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 = ⊤

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
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 = ⊤

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
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 = ⊤

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
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 = ⊤

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
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 = ⊤

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
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 = ⊤

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
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

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']
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

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}.card = 3
Tactic:
rw [Finset.card_insert_of_not_mem]
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, c}.card + 1 = 3

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}

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, c}.card + 1 = 3

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}
Tactic:
rw [Finset.card_pair (ne_comm.mp hc.right)]
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}

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}
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
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 ∧ ¬a = c

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 ∧ ¬a = c
Tactic:
apply And.intro hab
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 = c

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 = c
Tactic:
exact ne_comm.mp hc.left
State after:
no goals

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
⊢ ∃ c, c ∉ {a, b}
Tactic:
by_contra h
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ¬∃ c, c ∉ {a, b}
⊢ False

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ¬∃ c, c ∉ {a, b}
⊢ False
Tactic:
push_neg at h
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
⊢ False

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ False
Tactic:
rw [lt_iff_not_ge] at h2
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ False

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ False
Tactic:
apply h2
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ 2 ≥ Fintype.card α

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ 2 ≥ Fintype.card α
Tactic:
rw [ge_iff_le]
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ Fintype.card α ≤ 2

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b} = Finset.univ
⊢ Fintype.card α ≤ 2
Tactic:
rw [← Finset.card_eq_iff_eq_univ] at this
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b}.card = Fintype.card α
⊢ Fintype.card α ≤ 2

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b}.card = Fintype.card α
⊢ Fintype.card α ≤ 2
Tactic:
rw [← this]
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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b}.card = Fintype.card α
⊢ {a, b}.card ≤ 2

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
this : {a, b}.card = Fintype.card α
⊢ {a, b}.card ≤ 2
Tactic:
rw [Finset.card_pair hab]
State after:
no goals

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 α
h3 : Fintype.card α ≤ 3
h3' : Fintype.card α = 3
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
h : ∀ (c : α), c ∈ {a, b}
⊢ {a, b} = Finset.univ
Tactic:
ext c
State after:
case a
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ {a, b} ↔ c ∈ Finset.univ

State before:
case a
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ {a, b} ↔ c ∈ Finset.univ
Tactic:
constructor
State after:
case a.mp
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ {a, b} → c ∈ Finset.univ

case a.mpr
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ Finset.univ → c ∈ {a, b}

State before:
case a.mp
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ {a, b} → c ∈ Finset.univ
Tactic:
intro _
State after:
case a.mp
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
h : ∀ (c : α), c ∈ {a, b}
c : α
a✝ : c ∈ {a, b}
⊢ c ∈ Finset.univ

State before:
case a.mp
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
h : ∀ (c : α), c ∈ {a, b}
c : α
a✝ : c ∈ {a, b}
⊢ c ∈ Finset.univ
Tactic:
exact Finset.mem_univ c
State after:
no goals

State before:
case a.mpr
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
h : ∀ (c : α), c ∈ {a, b}
c : α
⊢ c ∈ Finset.univ → c ∈ {a, b}
Tactic:
intro _
State after:
case a.mpr
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
h : ∀ (c : α), c ∈ {a, b}
c : α
a✝ : c ∈ Finset.univ
⊢ c ∈ {a, b}

State before:
case a.mpr
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
h : ∀ (c : α), c ∈ {a, b}
c : α
a✝ : c ∈ Finset.univ
⊢ c ∈ {a, b}
Tactic:
exact h c
State after:
no goals

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 α
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
this : {a, b, c} = Finset.univ
⊢ B = ⊤
Tactic:
rw [eq_top_iff]
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 α
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
this : {a, b, c} = Finset.univ
⊢ ⊤ ≤ B

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 α
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
this : {a, b, c} = Finset.univ
⊢ ⊤ ≤ B
Tactic:
rw [Set.top_eq_univ, ← Finset.coe_univ, ← this]
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 α
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
this : {a, b, c} = Finset.univ
⊢ ↑{a, b, c} ≤ B

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 α
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
this : {a, b, c} = Finset.univ
⊢ ↑{a, b, c} ≤ B
Tactic:
intro x hx
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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x ∈ ↑{a, b, c}
⊢ x ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x ∈ ↑{a, b, c}
⊢ x ∈ B
Tactic:
simp only [Finset.coe_insert, Finset.coe_singleton, Set.mem_insert_iff,
  Set.mem_singleton_iff] at hx
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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ x ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = a ∨ x = b ∨ x = c
⊢ x ∈ B
Tactic:
cases' hx with hxa hx
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 : 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
this : {a, b, c} = Finset.univ
x : α
hxa : x = a
⊢ x ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B

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 : 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
this : {a, b, c} = Finset.univ
x : α
hxa : x = a
⊢ x ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B
Tactic:
rw [hxa]
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 : 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
this : {a, b, c} = Finset.univ
x : α
hxa : x = a
⊢ a ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B

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 : 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
this : {a, b, c} = Finset.univ
x : α
hxa : x = a
⊢ a ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B
Tactic:
exact ha
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hx : x = b ∨ x = c
⊢ x ∈ B
Tactic:
cases' hx with hxb hxc
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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this : {a, b, c} = Finset.univ
x : α
hxb : x = b
⊢ x ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B

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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this : {a, b, c} = Finset.univ
x : α
hxb : x = b
⊢ x ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B
Tactic:
rw [hxb]
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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this : {a, b, c} = Finset.univ
x : α
hxb : x = b
⊢ b ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B

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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this : {a, b, c} = Finset.univ
x : α
hxb : x = b
⊢ b ∈ 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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B
Tactic:
exact hb
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ x ∈ B
Tactic:
rw [hxc]
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ c ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ c ∈ B
Tactic:
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]⟩
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ c ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ c ∈ B
Tactic:
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]
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ g • B = B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ g • B = B
Tactic:
apply hB.def_mem ha
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ g • a ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ g • a ∈ B
Tactic:
change (Equiv.swap a b * Equiv.swap c b) • a ∈ B
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b * Equiv.swap c b) • a ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b * Equiv.swap c b) • a ∈ B
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b) ((Equiv.swap c b) a) ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b) ((Equiv.swap c b) a) ∈ B
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne (ne_comm.mp hc.left) hab]
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b) a ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ (Equiv.swap a b) a ∈ B
Tactic:
rw [Equiv.swap_apply_left]
State after:
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ b ∈ B

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
⊢ b ∈ B
Tactic:
exact hb
State after:
no goals

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ Equiv.swap a b * Equiv.swap c b ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b * Equiv.swap c b) = 1

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b * Equiv.swap c b) = 1
Tactic:
rw [Equiv.Perm.sign_mul]
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b) * Equiv.Perm.sign (Equiv.swap c b) = 1

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b) * Equiv.Perm.sign (Equiv.swap c b) = 1
Tactic:
rw [Equiv.Perm.sign_swap hab]
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ -1 * Equiv.Perm.sign (Equiv.swap c b) = 1

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ -1 * Equiv.Perm.sign (Equiv.swap c b) = 1
Tactic:
rw [Equiv.Perm.sign_swap hc.right]
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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ -1 * -1 = 1

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 α
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
this : {a, b, c} = Finset.univ
x : α
hxc : x = c
⊢ -1 * -1 = 1
Tactic:
simp only [Int.units_mul_self]
State after:
no goals

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 α
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
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ c ∈ B
Tactic:
rw [← this]
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 α
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
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ c ∈ g • B

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 α
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
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ c ∈ g • B
Tactic:
use b
State after:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ b ∈ B ∧ (fun x => (Submonoid.subtype (alternatingGroup α).toSubmonoid) g • x) b = c

State before:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ b ∈ B ∧ (fun x => (Submonoid.subtype (alternatingGroup α).toSubmonoid) g • x) b = c
Tactic:
apply And.intro hb
State after:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (fun x => (Submonoid.subtype (alternatingGroup α).toSubmonoid) g • x) b = c

State before:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (fun x => (Submonoid.subtype (alternatingGroup α).toSubmonoid) g • x) b = c
Tactic:
change (Equiv.swap a b * Equiv.swap c b) • b = c
State after:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b * Equiv.swap c b) • b = c

State before:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b * Equiv.swap c b) • b = c
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b) ((Equiv.swap c b) b) = c

State before:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b) ((Equiv.swap c b) b) = c
Tactic:
rw [Equiv.swap_apply_right]
State after:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b) c = c

State before:
case 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
a : α
ha : a ∈ B
b : α
hb : b ∈ B
hab : ¬a = b
c : α
hc : ¬c = a ∧ ¬c = b
this✝ : {a, b, c} = Finset.univ
x : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ (Equiv.swap a b) c = c
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hc.left hc.right]
State after:
no goals