-- 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'_6.h.mk.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
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⟩ ^ k = 1

Tactic:
convert one_zpow k

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⟩)
⊢ sign ↑⟨c, hc⟩ = 1

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
this : Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - g.cycleType.sum
⊢ y = 1

Tactic:
exact card_support_le_one.mp <| le_trans (Finset.card_le_univ _) (by omega)

Result:
no goals

Proof state:
α : 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
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.h.mk.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
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 => ↑?m.59695 ^ x) k = ↑(uv ?m.59695)
⊢ sign ↑(uv ⟨c, hc⟩) = 1

Tactic:
rw [← hk, map_zpow]

Result:
case h.e'_2.h.e'_6.h.mk.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
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⟩ ^ k = 1

Proof state:
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 α

Tactic:
rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]

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
⊢ sign y * ∏ c : { x // x ∈ g.cycleFactorsFinset }, sign ↑(uv c) = 1

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 ∈ Subgroup.centralizer {g}
⊢ x ∈ alternatingGroup α

Tactic:
rw [← kerParam_range_eq_centralizer_of_count_le_one h_count] at hx

Result:
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 α

Proof state:
case h.e'_2.h.e'_5.a
α : 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⟩)
⊢ ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #(↑⟨c, hc⟩).support

Tactic:
exact ⟨c, hc, rfl⟩

Result:
no goals

Proof state:
α : 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 : y = 1
⊢ 1 = sign y

Tactic:
simp [this]

Result:
no goals

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
⊢ 1 = sign y

Tactic:
suffices y = 1 by simp [this]

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
⊢ y = 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
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

Tactic:
exact hc.left

Result:
no goals