F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
⊢ count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
letI := Classical.decEq α
case refine'_1
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup ∅ f) = Finset.sup ∅ fun a => count b (f a)

case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)) →
        count b (Finset.sup (insert a s) f) = Finset.sup (insert a s) fun a => count b (f a)
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
refine' s.induction _ _
no goals
case refine'_1
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (Finset.sup ∅ f) = Finset.sup ∅ fun a => count b (f a)
exact count_zero _
case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ count b (Finset.sup (insert i s) f) = Finset.sup (insert i s) fun a => count b (f a)
case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)) →
        count b (Finset.sup (insert a s) f) = Finset.sup (insert a s) fun a => count b (f a)
intro i s _ ih
case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ max (count b (f i)) (Finset.sup s fun a => count b (f a)) = count b (f i) ⊔ Finset.sup s fun a => count b (f a)
case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ count b (Finset.sup (insert i s) f) = Finset.sup (insert i s) fun a => count b (f a)
rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]
no goals
case refine'_2
F : Type ?u.410886
α : Type u_2
β : Type u_1
γ : Type ?u.410895
ι : Type ?u.410898
κ : Type ?u.410901
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
i : α
s : Finset α
a✝ : ¬i ∈ s
ih : count b (Finset.sup s f) = Finset.sup s fun a => count b (f a)
⊢ max (count b (f i)) (Finset.sup s fun a => count b (f a)) = count b (f i) ⊔ Finset.sup s fun a => count b (f a)
rfl