Theorem: Equiv.Perm.isCommutative_iff (Jordan/Mathlib/GroupTheory/Subgroup/Basic.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
cases' Nat.lt_or_ge 2 (Fintype.card α) with hα hα
State after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2

State before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
rw [← not_lt]
State after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ ¬2 < Fintype.card α

State before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ ¬2 < Fintype.card α
Tactic:
simp only [hα, not_true_eq_false, iff_false]
State after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ ¬Std.Commutative fun x x_1 => x * x_1

State before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
⊢ ¬Std.Commutative fun x x_1 => x * x_1
Tactic:
intro h
State after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
h : Std.Commutative fun x x_1 => x * x_1
⊢ False

State before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 < Fintype.card α
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Tactic:
rw [Fintype.two_lt_card_iff] at hα
State after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
h : Std.Commutative fun x x_1 => x * x_1
⊢ False

State before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
h : Std.Commutative fun x x_1 => x * x_1
⊢ False
Tactic:
obtain ⟨a, b, c, hab, hac, hbc⟩ := hα
State after:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False

State before:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ False
Tactic:
apply hbc
State after:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c

State before:
case inl.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = c
Tactic:
convert Equiv.ext_iff.mp (h.comm (Equiv.swap a c) (Equiv.swap a b)) a
State after:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = (swap a c * swap a b) a

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a

State before:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ b = (swap a c * swap a b) a

case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Tactic:
rw [coe_mul, Function.comp_apply,
  Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne hab.symm hbc]
State after:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a

State before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : Std.Commutative fun x x_1 => x * x_1
a b c : α
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ c = (swap a b * swap a c) a
Tactic:
rw [coe_mul, Function.comp_apply,
  Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne hac.symm hbc.symm]
State after:
no goals

State before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ (Std.Commutative fun x x_1 => x * x_1) ↔ Fintype.card α ≤ 2
Tactic:
simp only [hα, iff_true]
State after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Std.Commutative fun x x_1 => x * x_1

State before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
apply Monoid.isCommutative_of_fintype_card_le_2
State after:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Fintype.card (Perm α) ≤ 2

State before:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Fintype.card (Perm α) ≤ 2
Tactic:
rw [← Nat.factorial_two, Fintype.card_perm]
State after:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2

State before:
case inr.hG
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 2 ≥ Fintype.card α
⊢ Nat.factorial (Fintype.card α) ≤ Nat.factorial 2
Tactic:
exact Nat.factorial_le hα
State after:
no goals