Theorem: is_alternating_of_index_2 (Jordan/IndexNormal.lean)

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
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Subgroup.index G = 2
hG' : Subgroup.Normal G
⊢ alternatingGroup α = G

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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
Tactic:
rw [List.length_map]
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
⊢ ∀ x ∈ List.map (⇑s) l, x = s k

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
⊢ ∀ x ∈ List.map (⇑s) l, x = s k
Tactic:
intro x hx
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
x : Equiv.Perm α ⧸ G
hx : x ∈ List.map (⇑s) l
⊢ x = s k

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
x : Equiv.Perm α ⧸ G
hx : x ∈ List.map (⇑s) l
⊢ x = s k
Tactic:
simp only [List.mem_map] at hx
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
x : Equiv.Perm α ⧸ G
hx : ∃ a ∈ l, s a = x
⊢ x = s k

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
x : Equiv.Perm α ⧸ G
hx : ∃ a ∈ l, s a = x
⊢ x = s k
Tactic:
obtain ⟨y, hyl, hxy⟩ := hx
State after:
case 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
x : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ x = s k

State before:
case 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
x : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ x = s k
Tactic:
rw [← hxy]
State after:
case 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
x : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ s y = s k

State before:
case 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
x : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ s y = s k
Tactic:
apply this'
State after:
case intro.intro.a
α : 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 : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ Equiv.Perm.IsSwap y

State before:
case intro.intro.a
α : 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 : Equiv.Perm α ⧸ G
y : Equiv.Perm α
hyl : y ∈ l
hxy : s y = x
⊢ Equiv.Perm.IsSwap y
Tactic:
exact hl y hyl
State after:
no goals

State before:
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
Tactic:
simp only [hm, pow_mul, hsk2, Int.units_sq, one_pow] at hsg hsg'
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
m : ℕ
hm : List.length l = 2 * m
hsg : Equiv.Perm.sign g = 1
hsg' : s g = 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1

State before:
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
m : ℕ
hm : List.length l = 2 * m
hsg : Equiv.Perm.sign g = 1
hsg' : s g = 1
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
simp only [hsg, hsg']
State after:
no goals

State before:
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
Tactic:
simp only [hm, pow_add, pow_mul, pow_one, hsk2, Int.units_sq, one_pow, one_mul] at hsg hsg'
State after:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1

State before:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ Equiv.Perm.sign g = 1 ↔ (QuotientGroup.mk' G) g = 1
Tactic:
simp only [hsg, hsg', neg_units_ne_self, false_iff, ne_eq]
State after:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ ¬s k = 1

State before:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ ¬s k = 1
Tactic:
simp only [QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff, s]
State after:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ k ∉ G

State before:
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
m : ℕ
hm : List.length l = 2 * m + 1
hsg : Equiv.Perm.sign g = -1
hsg' : s g = s k
⊢ k ∉ G
Tactic:
exact hk'
State after:
no goals