-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one
    (h_count : ∀ i, g.cycleType.count i ≤ 1) :
    (kerParam g).range = Subgroup.centralizer {g}

Proof state:
case h.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Tactic:
rw [← Multiset.nodup_iff_count_le_one, cycleType_def,
  Multiset.nodup_map_iff_inj_on (cycleFactorsFinset g).nodup] at h_count

Result:
case h.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (toPermHom g) ⟨x, ⋯⟩ ∈ (toPermHom g).range

Tactic:
simp

Result:
no goals

Proof state:
case h.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Tactic:
exact h_count _ (by simp) _ c.prop ((mem_range_toPermHom_iff).mp (by simp) c)

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ ∃ (x_1 : x ∈ Subgroup.centralizer {g}), (toPermHom g) ⟨x, ⋯⟩ = 1

Tactic:
use hx

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ (toPermHom g) ⟨x, ⋯⟩ = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
⊢ (kerParam g).range = Subgroup.centralizer {g}

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
⊢ x ∈ (kerParam g).range ↔ x ∈ Subgroup.centralizer {g}

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
⊢ x ∈ (kerParam g).range ↔ x ∈ Subgroup.centralizer {g}

Tactic:
refine ⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range

Tactic:
simp_rw [kerParam_range_eq, Subgroup.mem_map, MonoidHom.mem_ker, Subgroup.coe_subtype,
  Subtype.exists, exists_and_right, exists_eq_right]

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ ∃ (x_1 : x ∈ Subgroup.centralizer {g}), (toPermHom g) ⟨x, ⋯⟩ = 1

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ (toPermHom g) ⟨x, ⋯⟩ = 1

Tactic:
ext c : 2

Result:
case h.H.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) ∈ g.cycleFactorsFinset.val

Tactic:
simp

Result:
no goals