internlm/Lean-Github huggingface dataset:
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
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]
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
⊢ 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
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
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
Proof 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
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 α
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]
Proof 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
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 α
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]⟩
Proof 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
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 α
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]
Proof 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
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 α
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
Proof 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
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 α
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
Proof 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
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 α
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]
Proof 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
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 α
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]
Proof 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
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 α
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]
Proof 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
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 α
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
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
x : α
hxc : x = c
⊢ Equiv.swap a b * Equiv.swap c b ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
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 : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b * Equiv.swap c b) = 1
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 : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b * Equiv.swap c b) = 1
Tactic:
rw [Equiv.Perm.sign_mul]
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 : α
hxc : x = c
⊢ Equiv.Perm.sign (Equiv.swap a b) * Equiv.Perm.sign (Equiv.swap c b) = 1
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 : α
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]
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 : α
hxc : x = c
⊢ -1 * Equiv.Perm.sign (Equiv.swap c b) = 1
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 : α
hxc : x = c
⊢ -1 * Equiv.Perm.sign (Equiv.swap c b) = 1
Tactic:
rw [Equiv.Perm.sign_swap hc.right]
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 : α
hxc : x = c
⊢ -1 * -1 = 1
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 : α
hxc : x = c
⊢ -1 * -1 = 1
Tactic:
simp only [Int.units_mul_self]
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
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]
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 : α
hxc : x = c
g : ↥(alternatingGroup α) := { val := Equiv.swap a b * Equiv.swap c b, property := ⋯ }
this : g • B = B
⊢ c ∈ g • 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 : α
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
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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]
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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]
Proof 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
Theorem: MulAction.alternatingGroup.has_trivial_blocks
Proof 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]
Proof state after:
no goals