internlm/Lean-Github huggingface dataset:
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}.card = 3
Tactic:
rw [Finset.card_insert_of_not_mem]
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, 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}
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, 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)]
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}
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}
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, not_or]
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 ∧ ¬a = c
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 ∧ ¬a = c
Tactic:
apply And.intro hab
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 = c
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 = c
Tactic:
exact ne_comm.mp hc.left
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
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
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 α
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
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 α
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
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 α
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
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 α
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
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 α
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
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 α
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
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 α
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 α
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 α
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]
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 α
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
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 α
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
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 α
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
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 α
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]
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 α
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
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 α
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]
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
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
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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
Proof 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}
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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 _
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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
Proof state after:
no goals
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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 _
Proof 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}
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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
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
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]
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 α
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
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 α
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]
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 α
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
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 α
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
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 α
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
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 α
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
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 α
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
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 α
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
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 : 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
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 : 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]
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 : 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
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 : 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
Proof 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
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 α
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
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
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