internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.Finset.subtype_union
Proof state before:
case a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
a : Subtype p
⊢ a ∈ Finset.subtype p (s1 ∪ s2) ↔ a ∈ Finset.subtype p s1 ∪ Finset.subtype p s2
Tactic:
simp
Proof state after:
no goals
Theorem: Usa2002P1.Finset.subtype_map_subtype
Proof state before:
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
⊢ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) = x
Tactic:
ext ⟨y, hy⟩
Proof state after:
case a.mk
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
y : α
hy : p y
⊢ ⟨y, hy⟩ ∈ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) ↔ ⟨y, hy⟩ ∈ x
Theorem: Usa2002P1.Finset.subtype_map_subtype
Proof state before:
case a.mk
α : Type
p : α → Prop
inst✝ : DecidablePred p
x : Finset { a // p a }
y : α
hy : p y
⊢ ⟨y, hy⟩ ∈ Finset.subtype p (Finset.map (Function.Embedding.subtype p) x) ↔ ⟨y, hy⟩ ∈ x
Tactic:
simp [hy]
Proof state after:
no goals
Theorem: Usa2002P1.lemma1
Proof state before:
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }
Tactic:
let b : {a : Finset α // s ∉ a} → {a : Finset α // s ∈ a} :=
   fun ⟨a, ha⟩ ↦ ⟨Finset.cons s a ha, Finset.mem_cons_self s a⟩
Proof state after:
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }
Theorem: Usa2002P1.lemma1
Proof state before:
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
hb : Function.Bijective b
⊢ Fintype.card { a // s ∈ a } = Fintype.card { a // s ∉ a }
Tactic:
rw [Fintype.card_of_bijective hb]
Proof state after:
no goals
Theorem: Usa2002P1.lemma1
Proof state before:
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Function.Bijective b
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Function.Injective b

case right
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Function.Surjective b
Theorem: Usa2002P1.lemma1
Proof state before:
case left
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Function.Injective b
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
Proof state after:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : b ⟨x, hx⟩ = b ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.lemma1
Proof state before:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : b ⟨x, hx⟩ = b ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
simp only [Subtype.mk.injEq, b] at hxy
Proof state after:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : Finset.cons s x ⋯ = Finset.cons s y ⋯
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.lemma1
Proof state before:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : Finset.cons s x ⋯ = Finset.cons s y ⋯
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
rw [Subtype.mk.injEq]
Proof state after:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : Finset.cons s x ⋯ = Finset.cons s y ⋯
⊢ x = y
Theorem: Usa2002P1.lemma1
Proof state before:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : (Finset.cons s x ⋯).erase s = (Finset.cons s y ⋯).erase s
⊢ x = y
Tactic:
simp [Finset.erase_eq_of_not_mem hx, Finset.erase_eq_of_not_mem hy] at hxy
Proof state after:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : x = y
⊢ x = y
Theorem: Usa2002P1.lemma1
Proof state before:
case left.mk.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∉ x
y : Finset α
hy : s ∉ y
hxy : x = y
⊢ x = y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Usa2002P1.lemma1
Proof state before:
case right
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
⊢ Function.Surjective b
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case right.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∈ x
⊢ ∃ a, b a = ⟨x, hx⟩
Theorem: Usa2002P1.lemma1
Proof state before:
case right.mk
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∈ x
⊢ ∃ a, b a = ⟨x, hx⟩
Tactic:
use ⟨x.erase s, Finset.not_mem_erase s x⟩
Proof state after:
case h
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∈ x
⊢ b ⟨x.erase s, ⋯⟩ = ⟨x, hx⟩
Theorem: Usa2002P1.lemma1
Proof state before:
case h
α : Type
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : α
b : { a // s ∉ a } → { a // s ∈ a } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.cons s a ha, ⋯⟩
x : Finset α
hx : s ∈ x
⊢ b ⟨x.erase s, ⋯⟩ = ⟨x, hx⟩
Tactic:
simp [Finset.insert_erase hx, b]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hs : Fintype.card α = n
N : ℕ
hN : N ≤ 2 ^ n
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
revert N α
Proof state after:
n : ℕ
⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = n →
      ∀ N ≤ 2 ^ n,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
n : ℕ
⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = n →
      ∀ N ≤ 2 ^ n,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
induction' n with k ih
Proof state after:
case zero

⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = 0 →
      ∀ N ≤ 2 ^ 0,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N

case succ
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
⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k + 1 →
      ∀ N ≤ 2 ^ (k + 1),
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case zero

⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = 0 →
      ∀ N ≤ 2 ^ 0,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
intro α hde hft hs N hN
Proof state after:
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 2 ^ 0
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 2 ^ 0
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
rw [Nat.pow_zero] at hN
Proof state after:
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
interval_cases N
Proof state after:
case zero.«0»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 0

case zero.«1»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case zero.«0»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 0
Tactic:
use λ _ ↦ Color.blue
Proof state after:
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ (Finset α → Finset α → Color.blue = Color.blue → Color.blue = Color.blue) ∧
    Fintype.card { a // Color.blue = Color.red } = 0
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ (Finset α → Finset α → Color.blue = Color.blue → Color.blue = Color.blue) ∧
    Fintype.card { a // Color.blue = Color.red } = 0
Tactic:
simp only [forall_true_left, forall_const, Fintype.card_eq_zero, and_self]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case zero.«1»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 1
Tactic:
use λ _ ↦ Color.red
Proof state after:
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ (Finset α → Finset α → Color.red = Color.red → Color.red = Color.red) ∧
    Fintype.card { a // Color.red = Color.red } = 1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ (Finset α → Finset α → Color.red = Color.red → Color.red = Color.red) ∧
    Fintype.card { a // Color.red = Color.red } = 1
Tactic:
simp [Fintype.card_subtype, Finset.card_univ, hs]
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ
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
⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k + 1 →
      ∀ N ≤ 2 ^ (k + 1),
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
intros S hde hft hs N hN
Proof state after:
case succ
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)
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ
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)
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
have s : S := Nonempty.some (Fintype.card_pos_iff.mp (by rw [hs]; exact Nat.succ_pos k))
Proof state after:
case succ
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
let S' := { a : S // a ≠ s }
Proof state after:
case succ
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 }
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ
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 }
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
have hs' : Fintype.card S' = k := by simp [Fintype.card_subtype_compl, hs, S']
Proof state after:
case succ
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
obtain hl | hg := le_or_gt N (2 ^ k)
Proof state after:
case succ.inl
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
hl : N ≤ 2 ^ k
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N

case succ.inr
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
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof 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)
⊢ 0 < Fintype.card S
Tactic:
rw [hs]
Proof 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)
⊢ 0 < k + 1
Theorem: Usa2002P1.usa2002_p1_generalized
Proof 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)
⊢ 0 < k + 1
Tactic:
exact Nat.succ_pos k
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof 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 }
⊢ Fintype.card S' = k
Tactic:
simp [Fintype.card_subtype_compl, hs, S']
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ.inl
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
hl : N ≤ 2 ^ k
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
obtain ⟨f', hf1', hf2'⟩ := ih hs' N hl
Proof state after:
case succ.inl.intro.intro
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
hl : N ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case succ.inl.intro.intro
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
hl : N ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
Tactic:
let f (x: Finset S) : Color :=
  if s ∈ x then Color.blue else f' (Finset.subtype _ x)
Proof state after:
case succ.inl.intro.intro
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
hl : N ≤ 2 ^ k
f' : Finset S' → Color
hf1' : ∀ (s1 s2 : Finset S'), f' s1 = f' s2 → f' (s1 ∪ s2) = f' s1
hf2' : Fintype.card { a // f' a = Color.red } = N
f : Finset S → Color := fun x => if s ∈ x then Color.blue else f' (Finset.subtype (fun a => a ≠ s) x)
⊢ ∃ f, (∀ (s1 s2 : Finset S), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N