Theorem: three_cycle_is_commutator' (Jordan/Mathlib/Alternating.lean)

State before:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg : IsThreeCycle g
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
rw [← Subgroup.coe_mk (alternatingGroup α) g (Equiv.Perm.IsThreeCycle.sign hg)] at hg
State after:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹

State before:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
obtain ⟨p, q, h⟩ := three_cycle_is_commutator h5 hg
State after:
case intro.intro
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹

State before:
case intro.intro
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
use p
State after:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹

State before:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
use q
State after:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹

State before:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
simp only [← Subgroup.coe_mul, ← Subgroup.coe_inv, ← commutatorElement_def, h, coe_mk]
State after:
no goals