Theorem: alternatingGroup.V4_is_of_exponent_two (Jordan/V4.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ ∀ (g : ↥(V4 α)), g ^ 2 = 1
Tactic:
rintro ⟨⟨g, hg⟩, hg'⟩
State after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ { val := { val := g, property := hg }, property := hg' } ^ 2 = 1

State before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ { val := { val := g, property := hg }, property := hg' } ^ 2 = 1
Tactic:
simp only [← Subtype.coe_inj, SubmonoidClass.mk_pow, Subgroup.coe_mk, Subgroup.coe_one]
State after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ g ^ 2 = 1

State before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ g ^ 2 = 1
Tactic:
rw [← Subgroup.mem_carrier, V4_carrier_eq α hα4] at hg'
State after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ^ 2 = 1

State before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ^ 2 = 1
Tactic:
cases' hg' with hg' hg'
State after:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = 0
⊢ g ^ 2 = 1

case mk.mk.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ g ^ 2 = 1

State before:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = 0
⊢ g ^ 2 = 1
Tactic:
simp only [Subgroup.coe_mk, Equiv.Perm.cycleType_eq_zero] at hg'
State after:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : g = 1
⊢ g ^ 2 = 1

State before:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : g = 1
⊢ g ^ 2 = 1
Tactic:
simp only [hg', one_pow]
State after:
no goals

State before:
case mk.mk.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ g ^ 2 = 1
Tactic:
convert pow_orderOf_eq_one g
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ 2 = orderOf g

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ 2 = orderOf g
Tactic:
simp only [Subgroup.coe_mk] at hg'
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = orderOf g

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = orderOf g
Tactic:
rw [← Equiv.Perm.lcm_cycleType, hg']
State after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = Multiset.lcm {2, 2}

State before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = Multiset.lcm {2, 2}
Tactic:
norm_num
State after:
no goals