Theorem: alternatingGroup.isCommutative_of_order_three (Jordan/IndexNormal.lean)

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply @isCommutative_of_prime_order _ _ _ 3 _
State after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Fintype.card ↥(alternatingGroup α) = 3

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Fintype.card ↥(alternatingGroup α) = 3
Tactic:
have hα' : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial, hα]
  norm_num
State after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 3

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 3
Tactic:
apply mul_right_injective₀ (a := 2) (by norm_num)
State after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 3

State before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 3
Tactic:
simp only [two_mul_card_alternatingGroup, Fintype.card_perm, hα]
State after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 2 * 3

State before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 2 * 3
Tactic:
norm_num
State after:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 6

State before:
case a
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ Nat.factorial 3 = 6
Tactic:
rfl
State after:
no goals

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, hα]
State after:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ 1 < 3

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
⊢ 1 < 3
Tactic:
norm_num
State after:
no goals

State before:
α✝ : Type ?u.15286
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Fintype.card α = 3
hα' : Nontrivial α
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals