Theorem: alternatingGroup.commutator_group_le (Jordan/Mathlib/Alternating.lean)

State before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ _root_.commutator (Perm α) ≤ alternatingGroup α
Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]
State after:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ commutatorSet (Perm α) ⊆ ↑(alternatingGroup α)

State before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ commutatorSet (Perm α) ⊆ ↑(alternatingGroup α)
Tactic:
intro x
State after:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : Perm α
⊢ x ∈ commutatorSet (Perm α) → x ∈ ↑(alternatingGroup α)

State before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : Perm α
⊢ x ∈ commutatorSet (Perm α) → x ∈ ↑(alternatingGroup α)
Tactic:
rintro ⟨p, q, rfl⟩
State after:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ ⁅p, q⁆ ∈ ↑(alternatingGroup α)

State before:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ ⁅p, q⁆ ∈ ↑(alternatingGroup α)
Tactic:
simp only [SetLike.mem_coe, mem_alternatingGroup, map_commutatorElement,
  commutatorElement_eq_one_iff_commute]
State after:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ Commute (sign p) (sign q)

State before:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ Commute (sign p) (sign q)
Tactic:
apply Commute.all
State after:
no goals