Theorem: Equiv.permWithCycleType_empty (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
⊢ permWithCycleType α c = ∅
Tactic:
apply Finset.eq_empty_of_forall_not_mem
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
⊢ ∀ (x : Perm α), x ∉ permWithCycleType α c

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
⊢ ∀ (x : Perm α), x ∉ permWithCycleType α c
Tactic:
intro g
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ g ∉ permWithCycleType α c

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ g ∉ permWithCycleType α c
Tactic:
unfold Equiv.permWithCycleType
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ g ∉ Finset.filter (fun g => Perm.cycleType g = c) Finset.univ

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ g ∉ Finset.filter (fun g => Perm.cycleType g = c) Finset.univ
Tactic:
simp only [Set.toFinset_univ, Finset.mem_filter, Finset.mem_univ, true_and_iff]
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ ¬Perm.cycleType g = c

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ ¬Perm.cycleType g = c
Tactic:
intro hg
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ False

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ False
Tactic:
apply lt_iff_not_le.mp hc
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ Multiset.sum c ≤ Fintype.card α

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ Multiset.sum c ≤ Fintype.card α
Tactic:
rw [← hg]
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ Multiset.sum (Perm.cycleType g) ≤ Fintype.card α

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ Multiset.sum (Perm.cycleType g) ≤ Fintype.card α
Tactic:
rw [Equiv.Perm.sum_cycleType]
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ (Perm.support g).card ≤ Fintype.card α

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
hg : Perm.cycleType g = c
⊢ (Perm.support g).card ≤ Fintype.card α
Tactic:
refine' (Equiv.Perm.support g).card_le_univ
State after:
no goals