Theorem: Usa2002P1.usa2002_p1_generalized (Compfiles/Usa2002P1.lean)

State before:
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
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Tactic:
let b : Finset S' → { a : Finset S // s ∉ a } :=
  fun a ↦ ⟨Finset.map (Function.Embedding.subtype _) a, by simp⟩
State after:
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, ⋯⟩
⊢ Fintype.card { a // s ∉ a } = 2 ^ k

State before:
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, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card { a // s ∉ a } = 2 ^ k
Tactic:
rw [←Fintype.card_of_bijective hb]
State after:
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, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card (Finset S') = 2 ^ k

State before:
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, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card (Finset S') = 2 ^ k
Tactic:
exact h5
State after:
no goals

State before:
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
⊢ Fintype.card (Finset S') = 2 ^ k
Tactic:
rw [Fintype.card_finset, hs']
State after:
no goals

State before:
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
a : Finset S'
⊢ s ∉ Finset.map (Function.Embedding.subtype fun a => a ≠ s) a
Tactic:
simp
State after:
no goals

State before:
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, ⋯⟩
⊢ Function.Bijective b
Tactic:
constructor
State after:
case left
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, ⋯⟩
⊢ Function.Injective b

case right
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, ⋯⟩
⊢ Function.Surjective b

State before:
case left
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, ⋯⟩
⊢ Function.Injective b
Tactic:
rintro x y hxy
State after:
case left
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 y : Finset S'
hxy : b x = b y
⊢ x = y

State before:
case left
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 y : Finset S'
hxy : b x = b y
⊢ x = y
Tactic:
simp only [Subtype.mk.injEq, Finset.map_inj, b] at hxy
State after:
case left
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 y : Finset S'
hxy : x = y
⊢ x = y

State before:
case left
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 y : Finset S'
hxy : x = y
⊢ x = y
Tactic:
exact hxy
State after:
no goals

State before:
case right
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, ⋯⟩
⊢ Function.Surjective b
Tactic:
rintro ⟨x, hx⟩
State after:
case right.mk
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
⊢ ∃ a, b a = ⟨x, hx⟩

State before:
case right.mk
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
⊢ ∃ a, b a = ⟨x, hx⟩
Tactic:
use Finset.subtype _ x
State after:
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⟩

State before:
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⟩
Tactic:
simp only [Finset.subtype_map, Subtype.mk.injEq, b]
State after:
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

State before:
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
Tactic:
have h7 : ∀ a ∈ x, ¬ a = s := by
  intro a ha has
  rw [has] at ha
  contradiction
State after:
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
h7 : ∀ a ∈ x, ¬a = s
⊢ Finset.filter (fun a => a ≠ s) x = x

State before:
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
h7 : ∀ a ∈ x, ¬a = s
⊢ Finset.filter (fun a => a ≠ s) x = x
Tactic:
exact Finset.filter_eq_self.mpr h7
State after:
no goals

State before:
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
⊢ ∀ a ∈ x, ¬a = s
Tactic:
intro a ha has
State after:
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
a : S
ha : a ∈ x
has : a = s
⊢ False

State before:
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
a : S
ha : a ∈ x
has : a = s
⊢ False
Tactic:
rw [has] at ha
State after:
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
a : S
ha : s ∈ x
has : a = s
⊢ False

State before:
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
a : S
ha : s ∈ x
has : a = s
⊢ False
Tactic:
contradiction
State after:
no goals