Theorem: Set.ncard_filter_eq_count (Jordan/ConjClassCount.lean)

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
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)

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
State after:
no goals

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
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}

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]
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}

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
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}

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]
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)

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]
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))

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]
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)

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]
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

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
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

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]
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

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 ?_ ?_]
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}

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]
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}

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]
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)

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
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

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
State after:
no goals

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
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

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
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

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]
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

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 _
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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
State after:
no goals

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]
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

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
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

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
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

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
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

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]
State after:
no goals