Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType (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 =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      Nat.factorial (Fintype.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)))
    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 α) /
      (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)))

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 = 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 α) /
      (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:
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 α) /
      (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:
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 α) /
      (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:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    Nat.factorial (Fintype.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:
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    Nat.factorial (Fintype.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:
rw [← Equiv.Perm.conj_class_card_mul_eq g]
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    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))) /
      (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:
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    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))) /
      (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:
simp only [mul_assoc]
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    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))))) /
      (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:
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    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))))) /
      (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:
simp only [Fintype.card_coe, ← Set.toFinset_card, mul_assoc]
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    (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))))) /
      (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:
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    (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))))) /
      (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:
rw [Nat.div_eq_of_eq_mul_left _]
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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))))) =
    (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))))

α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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:
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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))))) =
    (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))))

α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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₂
State after:
case pos.intro.hx
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Set.toFinset {h | IsConj g h}).card = (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card

case pos.intro.hy
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 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)))) =
    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)))

α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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:
case pos.intro.hy
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 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)))) =
    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)))

α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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:
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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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:
case pos.intro.hx
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Set.toFinset {h | IsConj g h}).card = (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
Tactic:
apply congr_arg
State after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Set.toFinset {h | IsConj g h} = Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ

State before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Set.toFinset {h | IsConj g h} = Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
ext h
State after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ h ∈ Set.toFinset {h | IsConj g h} ↔ h ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ

State before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ h ∈ Set.toFinset {h | IsConj g h} ↔ h ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
simp only [Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
  Finset.univ_filter_exists, Finset.mem_image, true_and, Finset.mem_filter]
State after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ IsConj g h ↔ Equiv.Perm.cycleType h = m

State before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ IsConj g h ↔ Equiv.Perm.cycleType h = m
Tactic:
rw [isConj_comm, Equiv.Perm.isConj_iff_cycleType_eq, 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ 0 <
    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 Nat.mul_pos
State after:
case ha
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Nat.factorial (Fintype.card α - Multiset.sum m) > 0

case hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0

State before:
case ha
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Nat.factorial (Fintype.card α - Multiset.sum m) > 0

case hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
exact Nat.factorial_pos (Fintype.card α - Multiset.sum m)
State after:
case hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0

State before:
case hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
apply Nat.mul_pos
State after:
case hb.ha
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m > 0

case hb.hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0

State before:
case hb.ha
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod m > 0
Tactic:
apply Multiset.prod_pos
State after:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ m, 0 < a

State before:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ m, 0 < a
Tactic:
intro a ha
State after:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < a

State before:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < a
Tactic:
exact lt_of_lt_of_le (by norm_num) (hm.2 a ha)
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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case hb.hb
α : 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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
apply Multiset.prod_pos
State after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m), 0 < a

State before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m), 0 < a
Tactic:
intro a
State after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m) → 0 < a

State before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m) → 0 < a
Tactic:
rw [Multiset.mem_map]
State after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ (∃ a_1 ∈ Multiset.dedup m, Nat.factorial (Multiset.count a_1 m) = a) → 0 < a

State before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ (∃ a_1 ∈ Multiset.dedup m, Nat.factorial (Multiset.count a_1 m) = a) → 0 < a
Tactic:
rintro ⟨b, _, rfl⟩
State after:
case hb.hb.h.intro.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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
b : ℕ
left✝ : b ∈ Multiset.dedup m
⊢ 0 < Nat.factorial (Multiset.count b m)

State before:
case hb.hb.h.intro.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 ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
b : ℕ
left✝ : b ∈ Multiset.dedup m
⊢ 0 < Nat.factorial (Multiset.count b m)
Tactic:
apply Nat.factorial_pos
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 = 0
Tactic:
rw [Finset.card_eq_zero, ← Finset.not_nonempty_iff_eq_empty]
State after:
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).Nonempty

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).Nonempty
Tactic:
rw [← Equiv.permWithCycleType_nonempty_iff] at hm
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Equiv.permWithCycleType α m).Nonempty
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Equiv.permWithCycleType α m).Nonempty
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
Tactic:
exact hm
State after:
no goals