internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.V4_isCommutative
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.IsCommutative (V4 α)
Tactic:
refine' { is_comm := isCommutative_of_exponent_two (V4_is_of_exponent_two α hα4) }
Proof state after:
no goals
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ commutator G ≤ H
Tactic:
constructor
Proof state after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) → commutator G ≤ H

case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ commutator G ≤ H → Std.Commutative fun x x_1 => x * x_1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ (Std.Commutative fun x x_1 => x * x_1) → commutator G ≤ H
Tactic:
intro h
Proof state after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutator G ≤ H
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutator G ≤ H
Tactic:
simp only [commutator_eq_closure, Subgroup.closure_le]
Proof state after:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑H
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
⊢ commutatorSet G ⊆ ↑H
Tactic:
rintro g ⟨g1, g2, rfl⟩
Proof state after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ ↑H
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ ↑H
Tactic:
simp only [SetLike.mem_coe, ← QuotientGroup.eq_one_iff]
Proof state after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Tactic:
rw [← QuotientGroup.mk'_apply, map_commutatorElement (QuotientGroup.mk' H) g1 g2]
Proof state after:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mp.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : Std.Commutative fun x x_1 => x * x_1
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Tactic:
simp only [QuotientGroup.mk'_apply, commutatorElement_eq_one_iff_mul_comm, h.comm]
Proof state after:
no goals
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
⊢ commutator G ≤ H → Std.Commutative fun x x_1 => x * x_1
Tactic:
intro h
Proof state after:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ Std.Commutative fun x x_1 => x * x_1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
Proof state after:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ ∀ (a b : G ⧸ H), a * b = b * a
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
⊢ ∀ (a b : G ⧸ H), a * b = b * a
Tactic:
intro a b
Proof state after:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
a b : G ⧸ H
⊢ a * b = b * a
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
a b : G ⧸ H
⊢ a * b = b * a
Tactic:
obtain ⟨g1, rfl⟩ := QuotientGroup.mk'_surjective H a
Proof state after:
case mpr.comm.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
b : G ⧸ H
g1 : G
⊢ (QuotientGroup.mk' H) g1 * b = b * (QuotientGroup.mk' H) g1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
b : G ⧸ H
g1 : G
⊢ (QuotientGroup.mk' H) g1 * b = b * (QuotientGroup.mk' H) g1
Tactic:
obtain ⟨g2, rfl⟩ := QuotientGroup.mk'_surjective H b
Proof state after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) g1 * (QuotientGroup.mk' H) g2 = (QuotientGroup.mk' H) g2 * (QuotientGroup.mk' H) g1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) g1 * (QuotientGroup.mk' H) g2 = (QuotientGroup.mk' H) g2 * (QuotientGroup.mk' H) g1
Tactic:
rw [← commutatorElement_eq_one_iff_mul_comm]
Proof state after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅(QuotientGroup.mk' H) g1, (QuotientGroup.mk' H) g2⁆ = 1
Tactic:
rw [← map_commutatorElement _ g1 g2]
Proof state after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) ⁅g1, g2⁆ = 1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ (QuotientGroup.mk' H) ⁅g1, g2⁆ = 1
Tactic:
rw [QuotientGroup.mk'_apply]
Proof state after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ↑⁅g1, g2⁆ = 1
Tactic:
rw [QuotientGroup.eq_one_iff]
Proof state after:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ H
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ H
Tactic:
apply h
Proof state after:
case mpr.comm.intro.intro.a
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ commutator G
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro.a
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ ⁅g1, g2⁆ ∈ commutator G
Tactic:
apply Subgroup.commutator_mem_commutator
Proof state after:
case mpr.comm.intro.intro.a.h₁
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g1 ∈ ⊤

case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro.a.h₁
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g1 ∈ ⊤

case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Tactic:
refine' Subgroup.mem_top g1
Proof state after:
case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Theorem: alternatingGroup.Subgroup.quotient_isCommutative_iff_commutator_le
Proof state before:
case mpr.comm.intro.intro.a.h₂
α : Type ?u.69108
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : Subgroup.Normal H
h : commutator G ≤ H
g1 g2 : G
⊢ g2 ∈ ⊤
Tactic:
refine' Subgroup.mem_top g2
Proof state after:
no goals
Theorem: alternatingGroup.center_bot
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) = ⊥
Tactic:
rw [eq_bot_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) ≤ ⊥
Theorem: alternatingGroup.center_bot
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
⊢ Subgroup.center ↥(alternatingGroup α) ≤ ⊥
Tactic:
rintro ⟨g, hg⟩ hg'
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } ∈ ⊥
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } ∈ ⊥
Tactic:
simp only [Subgroup.mem_bot]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } = 1
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ { val := g, property := hg } = 1
Tactic:
simp only [← Subtype.coe_inj, Subgroup.coe_mk, Subgroup.coe_one]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ g = 1
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ g = 1
Tactic:
rw [← Equiv.Perm.support_eq_empty_iff]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ Equiv.Perm.support g = ∅
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ Equiv.Perm.support g = ∅
Tactic:
rw [Finset.eq_empty_iff_forall_not_mem]
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ ∀ (x : α), x ∉ Equiv.Perm.support g
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
⊢ ∀ (x : α), x ∉ Equiv.Perm.support g
Tactic:
intro a ha
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
⊢ False
Tactic:
let b := g a
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
⊢ False
Tactic:
have hab : b ≠ a := by simp only [b]; rw [← Equiv.Perm.mem_support]; exact ha
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
⊢ False
Tactic:
have : ({a, b} : Finset α)ᶜ.Nonempty :=
  by
  rw [← Finset.card_compl_lt_iff_nonempty, compl_compl, Finset.card_pair hab.symm]
  refine' lt_of_lt_of_le (by norm_num) hα4
Proof state after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
this : {a, b}ᶜ.Nonempty
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
this : {a, b}ᶜ.Nonempty
⊢ False
Tactic:
obtain ⟨c, hc⟩ := this
Proof state after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : c ∈ {a, b}ᶜ
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : c ∈ {a, b}ᶜ
⊢ False
Tactic:
simp only [Finset.compl_insert, Finset.mem_erase, Ne.def, Finset.mem_compl,
  Finset.mem_singleton] at hc
Proof state after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
⊢ False
Tactic:
have h2trans : MulAction.IsMultiplyPretransitive (alternatingGroup α) α 2 := by
  refine' MulAction.isMultiplyPretransitive_of_higher (alternatingGroup α) α
    (MulAction.IsMultiplyPretransitive.alternatingGroup_of_sub_two α) _ _
  exact Nat.le_sub_of_add_le hα4
  simp
Proof state after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α 2
⊢ False
Tactic:
rw [MulAction.is_two_pretransitive_iff] at h2trans
Proof state after:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
⊢ False
Tactic:
obtain ⟨k, hk, hk'⟩ := h2trans a b a c hab.symm (Ne.symm hc.left)
Proof state after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ False
Theorem: alternatingGroup.center_bot
Proof state before:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ False
Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a ≠ c by
  apply this; rw [← hk']; rfl
Proof state after:
case mk.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : 4 ≤ Fintype.card α
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ Subgroup.center ↥(alternatingGroup α)
a : α
ha : a ∈ Equiv.Perm.support g
b : α := g a
hab : b ≠ a
c : α
hc : ¬c = a ∧ ¬c = b
h2trans : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
k : ↥(alternatingGroup α)
hk : k • a = a
hk' : k • b = c
⊢ k • { val := g, property := hg } • a ≠ c