-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem card_le_of_centralizer_le_alternating (h : Subgroup.centralizer {g} ≤ alternatingGroup α) :
    Fintype.card α ≤ g.cycleType.sum + 1

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
⊢ False

Tactic:
suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 by
  exact this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))

Result:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
⊢ sign ((kerParam g) (swap a b, 1)) ≠ 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ 1 < Fintype.card ↑(Function.fixedPoints ⇑g)

Tactic:
rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ g.cycleType.sum ≤ Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ False

Tactic:
suffices 1 < Fintype.card (Function.fixedPoints g) by
  obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
  suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 by
    exact this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
  simp [sign_kerParam_apply_apply, hab]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ 1 < Fintype.card ↑(Function.fixedPoints ⇑g)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ 2 + g.cycleType.sum ≤ Fintype.card α

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
⊢ sign ((kerParam g) (swap a b, 1)) ≠ 1

Tactic:
simp [sign_kerParam_apply_apply, hab]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this✝ : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
this : sign ((kerParam g) (swap a b, 1)) ≠ 1
⊢ False

Tactic:
exact this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ #g.support ≤ Fintype.card α

Tactic:
exact Finset.card_le_univ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
⊢ Fintype.card α ≤ g.cycleType.sum + 1

Tactic:
by_contra! hm

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ False

Tactic:
replace hm : 2 + g.cycleType.sum ≤ Fintype.card α := by omega

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ g.cycleType.sum ≤ Fintype.card α

Tactic:
rw [sum_cycleType]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ #g.support ≤ Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
⊢ False

Tactic:
obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this

Result:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card ↑(Function.fixedPoints ⇑g)
a b : ↑(Function.fixedPoints ⇑g)
hab : a ≠ b
⊢ False