-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem map_subtype_of_cycleType (m : Multiset ℕ) :
    ({g | (g : Perm α).cycleType = m} : Finset (alternatingGroup α)).map (Embedding.subtype _) =
      if Even (m.sum + m.card) then ({g | g.cycleType = m} : Finset (Perm α)) else ∅

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ sign g = 1
⊢ False

Tactic:
rcases hg with ⟨hg, hs⟩

Result:
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : sign g = 1
⊢ False

Proof state:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g.cycleType = m → sign g = 1

Tactic:
intro hg

Result:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
⊢ sign g = 1

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g ∈ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ)
⊢ False

Tactic:
simp only [Finset.mem_map, Finset.mem_filter, Finset.mem_univ, true_and,
  Embedding.coe_subtype, Subtype.exists, mem_alternatingGroup, exists_and_left,
  exists_prop, exists_eq_right_right] at hg

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ sign g = 1
⊢ False

Proof state:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
⊢ sign g = 1

Tactic:
rw [sign_of_cycleType, hg, Even.neg_one_pow hm]

Result:
no goals

Proof state:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g ∈ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) ↔
    g ∈ filter (fun g => g.cycleType = m) univ

Tactic:
simp only [Finset.mem_map, Finset.mem_filter, Finset.mem_univ, true_and,
  Embedding.coe_subtype, Subtype.exists, mem_alternatingGroup, exists_and_left,
  exists_prop, exists_eq_right_right, and_iff_left_iff_imp]

Result:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g.cycleType = m → sign g = 1

Proof state:
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) =
    filter (fun g => g.cycleType = m) univ

Tactic:
ext g

Result:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g ∈ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) ↔
    g ∈ filter (fun g => g.cycleType = m) univ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : (-1) ^ (m.sum + m.card) = 1
⊢ -1 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ ∀ (x : Perm α),
    x ∉ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ)

Tactic:
intro g hg

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g ∈ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ)
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) =
    if Even (m.sum + m.card) then filter (fun g => g.cycleType = m) univ else ∅

Tactic:
split_ifs with hm

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) =
    filter (fun g => g.cycleType = m) univ

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) = ∅

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ) = ∅

Tactic:
rw [Finset.eq_empty_iff_forall_not_mem]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ ∀ (x : Perm α),
    x ∉ map (Embedding.subtype fun x => x ∈ alternatingGroup α) (filter (fun g => (↑g).cycleType = m) univ)

Proof state:
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : sign g = 1
⊢ False

Tactic:
rw [g.sign_of_cycleType, hg, neg_one_pow_eq_one_iff_even (by simp)] at hs

Result:
case neg.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False