internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ x ∈ support c
Tactic:
rw [Equiv.Perm.mem_support, hcx, Equiv.Perm.cycleOf_apply_self,
  Ne.def, ← Equiv.Perm.cycleOf_eq_one_iff, ← hcx]
Proof state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ ¬c = 1
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hcx : c = cycleOf g x
⊢ ¬c = 1
Tactic:
exact Equiv.Perm.IsCycle.ne_one (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
Proof state after:
no goals
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
⊢ x ∈ support c → c = cycleOf g x
Tactic:
intro hx
Proof state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ c = cycleOf g x
Theorem: Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
x : α
hx : x ∈ support c
⊢ c = cycleOf g x
Tactic:
exact Equiv.Perm.cycle_is_cycleOf hx hc
Proof state after:
no goals
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
s : Finset ι
k : κ
⊢ ncard {x | x ∈ s ∧ f x = k} = Multiset.count k (Multiset.map f s.val)
Tactic:
induction' s using Finset.induction with a s has ih
Proof state after:
case empty
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
⊢ ncard {x | x ∈ ∅ ∧ f x = k} = Multiset.count k (Multiset.map f ∅.val)

case insert
ι : 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)
⊢ ncard {x | x ∈ insert a s ∧ f x = k} = Multiset.count k (Multiset.map f (insert a s).val)
Theorem: Set.ncard_filter_eq_count
Proof state before:
case empty
ι : Type u_1
κ : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
f : ι → κ
k : κ
⊢ ncard {x | x ∈ ∅ ∧ f x = k} = Multiset.count k (Multiset.map f ∅.val)
Tactic:
simp
Proof state after:
no goals
Theorem: Set.ncard_filter_eq_count
Proof state before:
case insert
ι : 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 | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Tactic:
ext x
Proof state after:
case insert.h
ι : 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 : ι
⊢ x ∈ {x | x ∈ insert a s ∧ f x = k} ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Theorem: Set.ncard_filter_eq_count
Proof state before:
case insert.h
ι : 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 : ι
⊢ x ∈ {x | x ∈ insert a s ∧ f x = k} ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Tactic:
simp only [Finset.mem_insert, Set.mem_setOf_eq]
Proof state after:
case insert.h
ι : 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 : ι
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Theorem: Set.ncard_filter_eq_count
Proof state before:
case insert.h
ι : 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 : ι
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Tactic:
by_cases h : f a = k
Proof state after:
case pos
ι : 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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}

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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard {x | x ∈ insert a s ∧ f x = k} = Multiset.count k (Multiset.map f (insert a s).val)
Tactic:
rw [this]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map f (insert a s).val)
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map f (insert a s).val)
Tactic:
simp only [Finset.insert_val, Finset.mem_val, Multiset.mem_map, Multiset.mem_ndinsert, exists_eq_or_imp, Multiset.ndinsert_of_not_mem has]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) (a ::ₘ s.val))
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) (a ::ₘ s.val))
Tactic:
simp only [Multiset.map_cons, Multiset.mem_cons, Multiset.mem_map, Finset.mem_val,
  Multiset.nodup_cons, not_exists, not_and, ne_eq]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (f a ::ₘ Multiset.map (fun x => f x) s.val)
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (f a ::ₘ Multiset.map (fun x => f x) s.val)
Tactic:
rw [Multiset.count_cons]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0
Tactic:
by_cases h : f a = k
Proof state after:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0

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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : ¬f a = k
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0
Theorem: Set.ncard_filter_eq_count
Proof state before:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0
Tactic:
rw [if_pos h, if_pos h.symm]
Proof state after:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard (insert a {x | x ∈ s ∧ f x = k}) = Multiset.count k (Multiset.map (fun x => f x) s.val) + 1
Theorem: Set.ncard_filter_eq_count
Proof state before:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard (insert a {x | x ∈ s ∧ f x = k}) = Multiset.count k (Multiset.map (fun x => f x) s.val) + 1
Tactic:
rw [Set.ncard_insert_of_not_mem ?_ ?_]
Proof state after:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard {x | x ∈ s ∧ f x = k} + 1 = Multiset.count k (Multiset.map (fun x => f x) s.val) + 1

ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ a ∉ {x | x ∈ s ∧ f x = k}

ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ Set.Finite {x | x ∈ s ∧ f x = k}
Theorem: Set.ncard_filter_eq_count
Proof state before:
case pos
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ncard {x | x ∈ s ∧ f x = k} + 1 = Multiset.count k (Multiset.map (fun x => f x) s.val) + 1

ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ a ∉ {x | x ∈ s ∧ f x = k}

ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ Set.Finite {x | x ∈ s ∧ f x = k}
Tactic:
simp only [add_left_inj, ih]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ a ∉ {x | x ∈ s ∧ f x = k}

ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ Set.Finite {x | x ∈ s ∧ f x = k}
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ a ∉ {x | x ∈ s ∧ f x = k}
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ¬(a ∈ s ∧ f a = k)
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ ¬(a ∈ s ∧ f a = k)
Tactic:
intro ha
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
ha : a ∈ s ∧ f a = k
⊢ False
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
ha : a ∈ s ∧ f a = k
⊢ False
Tactic:
exact has ha.1
Proof state after:
no goals
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ Set.Finite {x | x ∈ s ∧ f x = k}
Tactic:
apply Set.Finite.subset s.finite_toSet
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ {x | x ∈ s ∧ f x = k} ⊆ ↑s
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
⊢ {x | x ∈ s ∧ f x = k} ⊆ ↑s
Tactic:
intro x
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
⊢ x ∈ {x | x ∈ s ∧ f x = k} → x ∈ ↑s
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
⊢ x ∈ {x | x ∈ s ∧ f x = k} → x ∈ ↑s
Tactic:
simp only [Set.mem_setOf_eq, Finset.mem_coe, and_imp]
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
⊢ x ∈ s → f x = k → x ∈ s
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
⊢ x ∈ s → f x = k → x ∈ s
Tactic:
intro hx _
Proof state after:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
hx : x ∈ s
a✝ : f x = k
⊢ x ∈ s
Theorem: Set.ncard_filter_eq_count
Proof state before:
ι : 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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : f a = k
x : ι
hx : x ∈ s
a✝ : f x = k
⊢ x ∈ s
Tactic:
exact hx
Proof state after:
no goals
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)
this : {x | x ∈ insert a s ∧ f x = k} = if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
h : ¬f a = k
⊢ ncard (if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}) =
    Multiset.count k (Multiset.map (fun x => f x) s.val) + if k = f a then 1 else 0
Tactic:
rw [if_neg h, if_neg (ne_comm.mp h), ih, add_zero]
Proof state after:
no goals
Theorem: Set.ncard_filter_eq_count
Proof state before:
case pos
ι : 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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Tactic:
simp only [Set.mem_setOf_eq, if_pos h, Set.mem_insert_iff]
Proof state after:
case pos
ι : 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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x = a ∨ x ∈ s ∧ f x = k
Theorem: Set.ncard_filter_eq_count
Proof state before:
case pos
ι : 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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x = a ∨ x ∈ s ∧ f x = k
Tactic:
aesop
Proof state after:
no goals
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
⊢ (x = a ∨ x ∈ s) ∧ f x = k ↔ x ∈ if f a = k then insert a {x | x ∈ s ∧ f x = k} else {x | x ∈ s ∧ f x = k}
Tactic:
simp only [Set.mem_setOf_eq, if_neg h, and_congr_left_iff, or_iff_right_iff_imp]
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
⊢ f x = k → x = a → x ∈ s