internlm/Lean-Github huggingface dataset:
Theorem: Set.ncard_filter_eq_count
Proof state before:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
⊢ f x = k → x = a → x ∈ s
Tactic:
intro hx hxa
Proof state after:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ x ∈ s
Theorem: Set.ncard_filter_eq_count
Proof state before:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ x ∈ s
Tactic:
exfalso
Proof state after:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ False
Theorem: Set.ncard_filter_eq_count
Proof state before:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ False
Tactic:
apply h
Proof state after:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ f a = k
Theorem: Set.ncard_filter_eq_count
Proof state before:
case neg
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
a : ι
s : Finset ι
has : a ∉ s
ih : ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
x : ι
h : ¬f a = k
hx : f x = k
hxa : x = a
⊢ f a = k
Tactic:
rw [← hxa, hx]
Proof state after:
no goals
Theorem: Multiset.prod_toFinset
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
m : Multiset α
hm : Nodup m
⊢ Finset.prod (toFinset m) f = prod (map f m)
Tactic:
induction' m using Multiset.induction with a m ih
Proof state after:
case empty
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
hm : Nodup 0
⊢ Finset.prod (toFinset 0) f = prod (map f 0)

case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Theorem: Multiset.prod_toFinset
Proof state before:
case empty
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
hm : Nodup 0
⊢ Finset.prod (toFinset 0) f = prod (map f 0)

case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
simp
Proof state after:
case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Theorem: Multiset.prod_toFinset
Proof state before:
case cons
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm : Nodup (a ::ₘ m)
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
obtain ⟨not_mem, hm⟩ := Multiset.nodup_cons.mp hm
Proof state after:
case cons.intro
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm✝ : Nodup (a ::ₘ m)
not_mem : a ∉ m
hm : Nodup m
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Theorem: Multiset.prod_toFinset
Proof state before:
case cons.intro
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
m : Multiset α
ih : Nodup m → Finset.prod (toFinset m) f = prod (map f m)
hm✝ : Nodup (a ::ₘ m)
not_mem : a ∉ m
hm : Nodup m
⊢ Finset.prod (toFinset (a ::ₘ m)) f = prod (map f (a ::ₘ m))
Tactic:
simp [Finset.prod_insert (mt Multiset.mem_toFinset.mp not_mem), ih hm]
Proof state after:
no goals
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
⊢ ∀ (x : Perm α), x ∉ permWithCycleType α c
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof state after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Multiset ℕ
hc : Fintype.card α < Multiset.sum c
g : Perm α
⊢ g ∉ permWithCycleType α c
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof 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
Theorem: Equiv.permWithCycleType_empty
Proof 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]
Proof 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
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof 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
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof 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 α
Theorem: Equiv.permWithCycleType_empty
Proof 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]
Proof 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 α
Theorem: Equiv.permWithCycleType_empty
Proof 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]
Proof 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 α
Theorem: Equiv.permWithCycleType_empty
Proof 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
Proof state after:
no goals
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty ↔ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty → Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → (permWithCycleType α m).Nonempty
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (permWithCycleType α m).Nonempty → Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
h : (permWithCycleType α m).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
h : (permWithCycleType α m).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
obtain ⟨g, hg⟩ := h
Proof state after:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g ∈ permWithCycleType α m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g ∈ permWithCycleType α m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
simp only [Equiv.permWithCycleType, Set.toFinset_univ, Finset.mem_filter,
  Finset.mem_univ, true_and_iff] at hg
Proof state after:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
constructor
Proof state after:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ Multiset.sum m ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
rw [← hg, Equiv.Perm.sum_cycleType]
Proof state after:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ (Perm.support g).card ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ (Perm.support g).card ≤ Fintype.card α

case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
exact (Equiv.Perm.support g).card_le_univ
Proof state after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
⊢ ∀ a ∈ m, 2 ≤ a
Tactic:
intro a
Proof state after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ m → 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ m → 2 ≤ a
Tactic:
rw [← hg]
Proof state after:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ Perm.cycleType g → 2 ≤ a
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mp.intro.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : Perm.cycleType g = m
a : ℕ
⊢ a ∈ Perm.cycleType g → 2 ≤ a
Tactic:
exact Equiv.Perm.two_le_of_mem_cycleType
Proof state after:
no goals
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → (permWithCycleType α m).Nonempty
Tactic:
rintro ⟨hc, h2c⟩
Proof state after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ (permWithCycleType α m).Nonempty
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ (permWithCycleType α m).Nonempty
Tactic:
have hc' : m.toList.sum ≤ Fintype.card α := by
  simp only [Multiset.sum_toList]
  exact hc
Proof state after:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
⊢ (permWithCycleType α m).Nonempty
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
⊢ (permWithCycleType α m).Nonempty
Tactic:
obtain ⟨p, hp_length, hp_nodup, hp_disj⟩ := List.exists_pw_disjoint_with_card hc'
Proof state after:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ (permWithCycleType α m).Nonempty
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case mpr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ (permWithCycleType α m).Nonempty
Tactic:
use List.prod (List.map (fun l => List.formPerm l) p)
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ List.prod (List.map (fun l => List.formPerm l) p) ∈ permWithCycleType α m
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ List.prod (List.map (fun l => List.formPerm l) p) ∈ permWithCycleType α m
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter, Set.toFinset_univ,
  Finset.mem_univ, true_and_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Tactic:
have hp2 : ∀ x ∈ p, 2 ≤ x.length :=
  by
  intro x hx
  apply h2c x.length
  rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
  exact ⟨x, hx, rfl⟩
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ Perm.cycleType (List.prod (List.map (fun l => List.formPerm l) p)) = m
Tactic:
rw [Equiv.Perm.cycleType_eq _ rfl]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ↑(List.map (Finset.card ∘ Perm.support) (List.map (fun l => List.formPerm l) p)) = m

case h.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ ∀ σ ∈ List.map (fun l => List.formPerm l) p, Perm.IsCycle σ

case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ List.length x
⊢ List.Pairwise Perm.Disjoint (List.map (fun l => List.formPerm l) p)
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ List.sum (Multiset.toList m) ≤ Fintype.card α
Tactic:
simp only [Multiset.sum_toList]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ Multiset.sum m ≤ Fintype.card α
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ Multiset.sum m ≤ Fintype.card α
Tactic:
exact hc
Proof state after:
no goals
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
⊢ ∀ x ∈ p, 2 ≤ List.length x
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ 2 ≤ List.length x
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ 2 ≤ List.length x
Tactic:
apply h2c x.length
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ List.length x ∈ m
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ List.length x ∈ m
Tactic:
rw [← Multiset.mem_toList, ← hp_length, List.mem_map]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, List.length a = List.length x
Theorem: Equiv.permWithCycleType_nonempty_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : Multiset.sum m ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : List.sum (Multiset.toList m) ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = Multiset.toList m
hp_nodup : ∀ s ∈ p, List.Nodup s
hp_disj : List.Pairwise List.Disjoint p
x : List α
hx : x ∈ p
⊢ ∃ a ∈ p, List.length a = List.length x
Tactic:
exact ⟨x, hx, rfl⟩
Proof state after:
no goals