Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
    else ∅
Tactic:
split_ifs with hm
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    ∅

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
ext g
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
simp only [Finset.mem_image, Finset.mem_filter]
State after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m

State before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
constructor
State after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) →
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m

case pos.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m →
    g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)

State before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) →
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
intro hg
State after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m

State before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
rw [Finset.mem_map] at hg
State after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  ∃ a ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ,
    { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } a = g
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m

State before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  ∃ a ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ,
    { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } a = g
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
obtain ⟨⟨k, hk⟩, hk', rfl⟩ := hg
State after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk } ∈ Finset.univ ∧
    Equiv.Perm.cycleType
        ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
      m

State before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk } ∈ Finset.univ ∧
    Equiv.Perm.cycleType
        ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
      m
Tactic:
apply And.intro (Finset.mem_univ _)
State after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m

State before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, Subgroup.coe_mk, true_and_iff] at hk'
State after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m

State before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Tactic:
simp only [Subgroup.coeSubtype, Function.Embedding.coeFn_mk, Subgroup.coe_mk]
State after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType k = m

State before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType k = m
Tactic:
exact hk'
State after:
no goals

State before:
case pos.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m →
    g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
rintro ⟨_, hg⟩
State after:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)

State before:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
simp only [Subgroup.coeSubtype, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Function.Embedding.coeFn_mk, exists_prop]
State after:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g

State before:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
Tactic:
use! g
State after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈ alternatingGroup α

State before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_of_cycleType, hg, Even.neg_one_pow hm]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    ∅
Tactic:
rw [Finset.eq_empty_iff_forall_not_mem]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ∀ (x : Equiv.Perm α),
    x ∉
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ∀ (x : Equiv.Perm α),
    x ∉
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
intro g hg
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ False

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ False
Tactic:
simp only [Subgroup.coeSubtype, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Function.Embedding.coeFn_mk, exists_prop] at hg
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg : ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
⊢ False

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg : ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
⊢ False
Tactic:
obtain ⟨⟨k, hk⟩, hkm, rfl⟩ := hg
State after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False

State before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Tactic:
rw [← Nat.odd_iff_not_even] at hm
State after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False

State before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Tactic:
simp only [Subgroup.coe_mk] at hkm
State after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType k = m
⊢ False

State before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType k = m
⊢ False
Tactic:
simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_of_cycleType, hkm, Odd.neg_one_pow hm, ← Units.eq_iff] at hk
State after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hkm : Equiv.Perm.cycleType k = m
hk : ↑(-1) = ↑1
⊢ False

State before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hkm : Equiv.Perm.cycleType k = m
hk : ↑(-1) = ↑1
⊢ False
Tactic:
norm_num at hk
State after:
no goals