-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem centralizer_le_alternating_iff :
    Subgroup.centralizer {g} ≤ alternatingGroup α ↔
      (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧
        ∀ i, g.cycleType.count i ≤ 1

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x => ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ sign ↑⟨c, hc⟩ = 1

Tactic:
rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]

Result:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x => ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ Odd #(↑⟨c, hc⟩).support

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x => ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ (kerParam g).range
⊢ x ∈ alternatingGroup α

Tactic:
obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx

Result:
case mpr.intro.intro.intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
⊢ (kerParam g) (y, uv) ∈ alternatingGroup α

Proof state:
case h.e'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
⊢ y = 1

Tactic:
have := card_fixedPoints g

Result:
case h.e'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
this : Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - g.cycleType.sum
⊢ y = 1

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α
⊢ (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
exact ⟨odd_of_centralizer_le_alternatingGroup h,
  card_le_of_centralizer_le_alternating h,
  count_le_one_of_centralizer_le_alternating h⟩

Result:
no goals

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x => ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ (↑⟨c, hc⟩).IsCycle

Tactic:
rw [mem_cycleFactorsFinset_iff] at hc

Result:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc✝ : c ∈ g.cycleFactorsFinset
hc : c.IsCycle ∧ ∀ a ∈ c.support, c a = g a
a✝ : ⟨c, hc✝⟩ ∈ univ
k : ℤ
hk : (fun x => ↑⟨c, hc✝⟩ ^ x) k = ↑(uv ⟨c, hc✝⟩)
⊢ (↑⟨c, hc✝⟩).IsCycle

Proof state:
case h.e'_2.h.e'_6.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
⊢ ∀ x ∈ univ, sign ↑(uv x) = 1

Tactic:
rintro ⟨c, hc⟩ _

Result:
case h.e'_2.h.e'_6.h.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
⊢ sign ↑(uv ⟨c, hc⟩) = 1

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) →
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α
⊢ (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1