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
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]
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
⊢ ∀ x ∈ List.map (⇑s) l, x = 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
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
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
x : Equiv.Perm α ⧸ G
hx : x ∈ List.map (⇑s) l
⊢ x = 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
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
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
x : Equiv.Perm α ⧸ G
hx : ∃ a ∈ l, s a = x
⊢ x = 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
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
Proof 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
Theorem: is_alternating_of_index_2
Proof 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]
Proof 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
Theorem: is_alternating_of_index_2
Proof 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'
Proof 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
Theorem: is_alternating_of_index_2
Proof 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
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof 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'
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
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
Theorem: is_alternating_of_index_2
Proof 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']
Proof state after:
no goals
Theorem: is_alternating_of_index_2
Proof 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'
Proof 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
Theorem: is_alternating_of_index_2
Proof 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]
Proof 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
Theorem: is_alternating_of_index_2
Proof 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]
Proof 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
Theorem: is_alternating_of_index_2
Proof 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'
Proof state after:
no goals
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
⊢ alternatingGroup α ≤ G
Tactic:
cases' Nat.eq_zero_or_pos G.index with h h
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G = 0
⊢ alternatingGroup α ≤ G

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G > 0
⊢ alternatingGroup α ≤ G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h : Subgroup.index G > 0
⊢ alternatingGroup α ≤ G
Tactic:
cases' eq_or_gt_of_le (Nat.succ_le_iff.mpr h) with h h
Proof state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Subgroup.index G = Nat.succ 0
⊢ alternatingGroup α ≤ G

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ 0 < Subgroup.index G
⊢ alternatingGroup α ≤ G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ 0 < Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
rw [← Nat.succ_le_iff] at h
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ (Nat.succ 0) ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : Nat.succ (Nat.succ 0) ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
norm_num at h
Proof state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α ≤ G
Tactic:
apply le_of_eq
Proof state after:
case inr.inr.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α = G
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ alternatingGroup α = G
Tactic:
apply is_alternating_of_index_2
Proof state after:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G = 2
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G = 2
Tactic:
refine' le_antisymm _ h
Proof state after:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G ≤ 2
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ Subgroup.index G ≤ 2
Tactic:
refine' Nat.le_of_mul_le_mul_left _ _
Proof state after:
case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1
Tactic:
swap
Proof state after:
case inr.inr.a.hG.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ?inr.inr.a.hG.refine'_1 * Subgroup.index G ≤ ?inr.inr.a.hG.refine'_1 * 2

case inr.inr.a.hG.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ ℕ

case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < ?inr.inr.a.hG.refine'_1
Theorem: large_subgroup_of_perm_contains_alternating
Proof state before:
case inr.inr.a.hG.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hG : Fintype.card (Equiv.Perm α) ≤ 2 * Fintype.card ↥G
h✝ : Subgroup.index G > 0
h : 2 ≤ Subgroup.index G
⊢ 0 < Fintype.card ↥G
Tactic:
exact Fintype.card_pos
Proof state after:
no goals