-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem count_le_one_of_centralizer_le_alternating
    (h : Subgroup.centralizer {g} ≤ alternatingGroup α) :
    ∀ i, g.cycleType.count i ≤ 1

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
⊢ sign ↑k = -1

Tactic:
have hk_cT : k.val.cycleType = Multiset.replicate k.val.cycleType.card 2 := by
  rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow,
    ← Subgroup.coe_one, Subtype.coe_inj, hk, ← map_pow]
  convert MonoidHom.map_one _
  rw [← Subtype.coe_inj]
  apply Equiv.swap_mul_self

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
⊢ sign ↑k = -1

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : { x // x ∈ g.cycleFactorsFinset }
hx : x = ⟨c, hc⟩
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
rw [hx, Equiv.swap_apply_left]

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : { x // x ∈ g.cycleFactorsFinset }
hx : x = ⟨c, hc⟩
⊢ #(↑⟨d, hd⟩).support = #(↑⟨c, hc⟩).support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
⊢ ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y

Tactic:
by_contra hm

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : ¬∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hsign_k : sign ↑k = -1
⊢ 1 = -1

Tactic:
rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : { x // x ∈ g.cycleFactorsFinset }
hx : ¬x = ⟨c, hc⟩
⊢ #(↑(τ x)).support = #(↑x).support

Tactic:
by_cases hx' : x = ⟨d, hd⟩

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : { x // x ∈ g.cycleFactorsFinset }
hx : ¬x = ⟨c, hc⟩
hx' : x = ⟨d, hd⟩
⊢ #(↑(τ x)).support = #(↑x).support

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : { x // x ∈ g.cycleFactorsFinset }
hx : ¬x = ⟨c, hc⟩
hx' : ¬x = ⟨d, hd⟩
⊢ #(↑(τ x)).support = #(↑x).support

Proof state:
case intro.intro.intro.intro.intro.intro.h.hi
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
⊢ (↑k).cycleType.card ∈ g.cycleType

Tactic:
have that : Multiset.card (k : Perm α).cycleType = (c : Perm α).support.card := by
  rw [← Nat.mul_left_inj (a := 2) (by norm_num), this]
  simp only [hk, toCentralizer, MonoidHom.coe_mk, OneHom.coe_mk, card_ofPermHom_support]
  have H : (⟨c, hc⟩ : g.cycleFactorsFinset) ≠ ⟨d, hd⟩ := Subtype.coe_ne_coe.mp hm'
  simp only [τ, support_swap H]
  rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
    Finset.sum_singleton, hm, mul_two]

Result:
case intro.intro.intro.intro.intro.intro.h.hi
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm { x // x ∈ g.cycleFactorsFinset } := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
that : (↑k).cycleType.card = #c.support
⊢ (↑k).cycleType.card ∈ g.cycleType