internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap (swap x y)

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
exact ⟨x, y, hxy, rfl⟩
Proof state after:
case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Theorem: Equiv.Perm.is_prod_swap_list
Proof state before:
case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
exact hl s hs
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
⊢ alternatingGroup α = G
Tactic:
have hG' := Subgroup.normal_of_index_eq_two hG
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
⊢ alternatingGroup α = 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
⊢ alternatingGroup α = G
Tactic:
let s : Equiv.Perm α →* Equiv.Perm α ⧸ G := QuotientGroup.mk' G
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
⊢ alternatingGroup α = 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
⊢ alternatingGroup α = G
Tactic:
rw [alternatingGroup_eq_sign_ker, ← QuotientGroup.ker_mk' G]
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
⊢ MonoidHom.ker Equiv.Perm.sign = MonoidHom.ker (QuotientGroup.mk' 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
⊢ MonoidHom.ker Equiv.Perm.sign = MonoidHom.ker (QuotientGroup.mk' G)
Tactic:
ext g
Proof state after:
case h
α : 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 α
⊢ g ∈ MonoidHom.ker Equiv.Perm.sign ↔ g ∈ MonoidHom.ker (QuotientGroup.mk' G)
Theorem: is_alternating_of_index_2
Proof state before:
case h
α : 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 α
⊢ g ∈ MonoidHom.ker Equiv.Perm.sign ↔ g ∈ MonoidHom.ker (QuotientGroup.mk' G)
Tactic:
simp only [Equiv.Perm.sign.mem_ker, (QuotientGroup.mk' G).mem_ker]
Proof state after:
case h
α : 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 α
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h
α : 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 α
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
have h2 : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
Proof state after:
case h
α : 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)
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h
α : 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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
have : ∃ g : Equiv.Perm α, g.IsSwap ∧ g ∉ G := by
  by_contra h; push_neg at h
  suffices G = ⊤ by
    rw [this, Subgroup.index_top] at hG
    norm_num at hG
  rw [eq_top_iff, ← Equiv.Perm.closure_isSwap, Subgroup.closure_le G]
  intro g hg
  simp only [Set.mem_setOf_eq] at hg
  simp only [SetLike.mem_coe]
  exact h g hg
Proof state after:
case h
α : 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
this : ∃ g, Equiv.Perm.IsSwap g ∧ g ∉ G
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h
α : 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
this : ∃ g, Equiv.Perm.IsSwap g ∧ g ∉ G
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
obtain ⟨k, hk, hk'⟩ := this
Proof state after:
case h.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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
have this' : ∀ g : Equiv.Perm α, g.IsSwap → s g = s k := by
  intro g hg
  obtain ⟨a, b, hab, habg⟩ := hg
  obtain ⟨x, y, hxy, hxyk⟩ := hk
  obtain ⟨u, hu⟩ := Equiv.Perm.isConj_swap hab hxy
  let hu' := congr_arg s (SemiconjBy.eq hu)
  simp only [map_mul] at hu'
  apply mul_left_cancel (a := s u)
  rw [habg, hxyk, hu']
  apply hG''.comm
Proof state after:
case h.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
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
have hsk2 : s k ^ 2 = 1 := by
  rw [pow_two]; rw [← map_mul]
  obtain ⟨x, y, _, hxyk⟩ := hk
  rw [hxyk]
  rw [Equiv.swap_mul_self]
  rw [map_one]
Proof state after:
case h.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
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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
this' : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → s g = s k
hsk2 : s k ^ 2 = 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
obtain ⟨l, hl, hg⟩ := g.is_prod_swap_list
Proof state after:
case h.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 : 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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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 : 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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
let hsg := Equiv.Perm.sign_prod_list_swap hl
Proof state after:
case h.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 : 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 (List.prod l) = (-1) ^ List.length l := Equiv.Perm.sign_prod_list_swap hl
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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 : 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 (List.prod l) = (-1) ^ List.length l := Equiv.Perm.sign_prod_list_swap hl
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
rw [← hg] at hsg
Proof state after:
case h.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 : 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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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 : 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
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
have hsg' : s g = s k ^ l.length := by
  rw [hg]
  rw [map_list_prod]
  rw [List.prod_eq_pow_card (List.map s l) (s k) _]
  rw [List.length_map]
  intro x hx
  simp only [List.mem_map] at hx
  obtain ⟨y, hyl, hxy⟩ := hx
  rw [← hxy]
  apply this'; exact hl y hyl
Proof state after:
case h.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 : 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
hsg' : s g = s k ^ List.length l
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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 : 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
hsg' : s g = s k ^ List.length l
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
obtain ⟨m, hm⟩ := Nat.even_or_odd' l.length
Proof state after:
case h.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 : 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
hsg' : s g = s k ^ List.length l
m : ℕ
hm : List.length l = 2 * m ∨ List.length l = 2 * m + 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Theorem: is_alternating_of_index_2
Proof state before:
case h.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 : 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
hsg' : s g = s k ^ List.length l
m : ℕ
hm : List.length l = 2 * m ∨ List.length l = 2 * m + 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
cases' hm with hm hm
Proof state after:
case h.intro.intro.intro.intro.intro.inl
α : 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
hsg' : s g = s k ^ List.length l
m : ℕ
hm : List.length l = 2 * m
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1

case h.intro.intro.intro.intro.intro.inr
α : 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
hsg' : s g = s k ^ List.length l
m : ℕ
hm : List.length l = 2 * m + 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 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)
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
refine' isCommutative_of_prime_order (hp := h2) _
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)
⊢ Fintype.card (Equiv.Perm α ⧸ G) = 2
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)
⊢ Fintype.card (Equiv.Perm α ⧸ G) = 2
Tactic:
rw [← Nat.card_eq_fintype_card]
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)
⊢ Nat.card (Equiv.Perm α ⧸ G) = 2
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)
⊢ Nat.card (Equiv.Perm α ⧸ G) = 2
Tactic:
exact 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
⊢ ∃ g, Equiv.Perm.IsSwap g ∧ g ∉ G
Tactic:
by_contra h
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.IsSwap g ∧ g ∉ G
⊢ False
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.IsSwap g ∧ g ∉ G
⊢ False
Tactic:
push_neg at h
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
⊢ False
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
⊢ False
Tactic:
suffices G = ⊤ by
  rw [this, Subgroup.index_top] at hG
  norm_num 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 = ⊤
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 = ⊤
Tactic:
rw [eq_top_iff, ← Equiv.Perm.closure_isSwap, Subgroup.closure_le G]
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
⊢ {σ | Equiv.Perm.IsSwap σ} ⊆ ↑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
⊢ {σ | Equiv.Perm.IsSwap σ} ⊆ ↑G
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
h : ∀ (g : Equiv.Perm α), Equiv.Perm.IsSwap g → g ∈ G
g : Equiv.Perm α
hg : g ∈ {σ | Equiv.Perm.IsSwap σ}
⊢ g ∈ ↑G