simp only [Finset.subtype_map, Subtype.mk.injEq, b]
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ b (Finset.subtype (fun a => a ≠ s) x) = ⟨x, hx⟩
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ Finset.filter (fun a => a ≠ s) x = x