internlm/Lean-Github huggingface dataset:
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : g ∈ {σ | Equiv.Perm.IsSwap σ}
⊢ g ∈ ↑G
Tactic:
simp only [Set.mem_setOf_eq] at hg
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ g ∈ ↑G
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ g ∈ ↑G
Tactic:
simp only [SetLike.mem_coe]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ g ∈ G
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ g ∈ G
Tactic:
exact h g hg
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
this : G = ⊤
⊢ False
Tactic:
rw [this, Subgroup.index_top] at hG
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : 1 = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
this : G = ⊤
⊢ False
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : 1 = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
this : G = ⊤
⊢ False
Tactic:
norm_num at hG
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
⊢ ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
Tactic:
intro g hg
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
g : Equiv.Perm α
hg : Equiv.Perm.IsSwap g
⊢ s g = s k
Tactic:
obtain ⟨a, b, hab, habg⟩ := hg
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
⊢ s g = s k
Tactic:
obtain ⟨x, y, hxy, hxyk⟩ := hk
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s g = s k
Tactic:
obtain ⟨u, hu⟩ := Equiv.Perm.isConj_swap hab hxy
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
⊢ s g = s k
Tactic:
let hu' := congr_arg s (SemiconjBy.eq hu)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s (↑u * Equiv.swap a b) = s (Equiv.swap x y * ↑u) := congr_arg (⇑s) (SemiconjBy.eq hu)
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s (↑u * Equiv.swap a b) = s (Equiv.swap x y * ↑u) := congr_arg (⇑s) (SemiconjBy.eq hu)
⊢ s g = s k
Tactic:
simp only [map_mul] at hu'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s g = s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s g = s k
Tactic:
apply mul_left_cancel (a := s u)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s ↑u * s g = s ↑u * s k
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s ↑u * s g = s ↑u * s k
Tactic:
rw [habg, hxyk, hu']
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s (Equiv.swap x y) * s ↑u = s ↑u * s (Equiv.swap x y)
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g✝ : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
g : Equiv.Perm α
a b : α
hab : a ≠ b
habg : g = Equiv.swap a b
x y : α
hxy : x ≠ y
hxyk : k = Equiv.swap x y
u : (Equiv.Perm α)ˣ
hu : SemiconjBy (↑u) (Equiv.swap a b) (Equiv.swap x y)
hu' : s ↑u * s (Equiv.swap a b) = s (Equiv.swap x y) * s ↑u
⊢ s (Equiv.swap x y) * s ↑u = s ↑u * s (Equiv.swap x y)
Tactic:
apply hG''.comm
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ s k ^ 2 = 1
Tactic:
rw [pow_two]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ s k * s k = 1
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ s k * s k = 1
Tactic:
rw [← map_mul]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ s (k * k) = 1
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ s (k * k) = 1
Tactic:
obtain ⟨x, y, _, hxyk⟩ := hk
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s (k * k) = 1
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s (k * k) = 1
Tactic:
rw [hxyk]
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s (Equiv.swap x y * Equiv.swap x y) = 1
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s (Equiv.swap x y * Equiv.swap x y) = 1
Tactic:
rw [Equiv.swap_mul_self]
Proof state after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s 1 = 1
Theorem: is_alternating_of_index_2
Proof state before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
x y : α
left✝ : x ≠ y
hxyk : k = Equiv.swap x y
⊢ s 1 = 1
Tactic:
rw [map_one]
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ s g = s k ^ List.length l
Tactic:
rw [hg]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ s (List.prod l) = s k ^ List.length l
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ s (List.prod l) = s k ^ List.length l
Tactic:
rw [map_list_prod]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ List.prod (List.map (⇑s) l) = s k ^ List.length l
Theorem: is_alternating_of_index_2
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ List.prod (List.map (⇑s) l) = s k ^ List.length l
Tactic:
rw [List.prod_eq_pow_card (List.map s l) (s k) _]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ s k ^ List.length (List.map (⇑s) l) = s k ^ List.length l

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
g : Equiv.Perm α
h2 : Fact (Nat.Prime 2)
hG'' : Std.Commutative fun x x_1 => x * x_1
k : Equiv.Perm α
hk : Equiv.Perm.IsSwap k
hk' : k ∉ G
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
l : List (Equiv.Perm α)
hl : ∀ s ∈ l, Equiv.Perm.IsSwap s
hg : g = List.prod l
hsg : Equiv.Perm.sign g = (-1) ^ List.length l
⊢ ∀ x ∈ List.map (⇑s) l, x = s k