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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Fintype.card ↥(alternatingGroup α) = 12
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial, hα4]
  norm_num
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 12

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 12
Tactic:
apply mul_right_injective₀ (_: 2 ≠ 0)
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
dsimp
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 * Fintype.card ↥(alternatingGroup α) = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 * Fintype.card ↥(alternatingGroup α) = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
rw [two_mul_card_alternatingGroup, Fintype.card_perm, hα4]
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
all_goals
  norm_num
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 24

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 24
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, hα4]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ 1 < 4

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ 1 < 4
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals