Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
Tactic:
split_ifs with hm
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Nat.factorial (Fintype.card α)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    0

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Nat.factorial (Fintype.card α)
Tactic:
obtain ⟨g, hg⟩ := Equiv.permWithCycleType_nonempty_iff.mpr hm
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Nat.factorial (Fintype.card α)

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
⊢ Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
Tactic:
ext h
State after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ h ∈ Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ ↔
    h ∈ Finset.filter (fun h => IsConj g h) Finset.univ

State before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ h ∈ Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ ↔
    h ∈ Finset.filter (fun h => IsConj g h) Finset.univ
Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, Set.mem_toFinset, Set.mem_setOf_eq]
State after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj g h

State before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj g h
Tactic:
rw [isConj_comm]
State after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj h g

State before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj h g
Tactic:
rw [Equiv.Perm.isConj_iff_cycleType_eq]
State after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g

State before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
State after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g h : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g

State before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g h : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g
Tactic:
rw [hg.2]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [this, ← Equiv.Perm.conj_class_card_mul_eq g]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Fintype.card ↑{h | IsConj g h} * Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Fintype.card ↑{h | IsConj g h} * Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
simp only [Fintype.card_coe, ← Set.toFinset_card, mul_assoc]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Tactic:
rw [hg.2]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))))
Tactic:
apply congr_arg₂ _ _ rfl
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card = (Set.toFinset {h | IsConj g h}).card

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card = (Set.toFinset {h | IsConj g h}).card
Tactic:
apply congr_arg
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Finset.filter (fun h => IsConj g h) Finset.univ = Set.toFinset {h | IsConj g h}

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Finset.filter (fun h => IsConj g h) Finset.univ = Set.toFinset {h | IsConj g h}
Tactic:
ext σ
State after:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
σ : Equiv.Perm α
⊢ σ ∈ Finset.filter (fun h => IsConj g h) Finset.univ ↔ σ ∈ Set.toFinset {h | IsConj g h}

State before:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
σ : Equiv.Perm α
⊢ σ ∈ Finset.filter (fun h => IsConj g h) Finset.univ ↔ σ ∈ Set.toFinset {h | IsConj g h}
Tactic:
simp only [isConj_iff, Finset.mem_univ, forall_true_left, Finset.univ_filter_exists,
  Finset.mem_image, true_and, Set.toFinset_setOf]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    0
Tactic:
convert MulZeroClass.zero_mul _
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0
Tactic:
rw [Finset.card_eq_zero]
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ = ∅

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ = ∅
Tactic:
rw [← Finset.isEmpty_coe_sort]
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ IsEmpty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ IsEmpty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Tactic:
rw [← not_nonempty_iff]
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Tactic:
intro h
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ False

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ False
Tactic:
apply hm
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
simp only [Finset.nonempty_coe_sort] at h
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
rw [← Equiv.permWithCycleType_nonempty_iff]
State after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ (Equiv.permWithCycleType α m).Nonempty

State before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ (Equiv.permWithCycleType α m).Nonempty
Tactic:
exact h
State after:
no goals