internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.usa2002_p1_generalized
Proof 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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
⊢ Function.Injective b
Tactic:
rintro ⟨x, hx⟩ ⟨y,hy⟩ hxy
Proof state after:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : b ⟨x, hx⟩ = b ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : b ⟨x, hx⟩ = b ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
unfold_let b at hxy
Proof state after:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy :
  (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨x, hx⟩ =
    (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy :
  (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨x, hx⟩ =
    (fun x =>
        match x with
        | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩)
      ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
simp at hxy
Proof state after:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : Finset.subtype (fun a => ¬a = s) x = Finset.subtype (fun a => ¬a = s) y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.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
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : Finset.subtype (fun a => ¬a = s) x = Finset.subtype (fun a => ¬a = s) y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
obtain ⟨h3, _⟩ := (h2 x).mp hx
Proof state after:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : Finset.subtype (fun a => ¬a = s) x = Finset.subtype (fun a => ¬a = s) y
h3 : s ∉ x
right✝ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : Finset.subtype (fun a => ¬a = s) x = Finset.subtype (fun a => ¬a = s) y
h3 : s ∉ x
right✝ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
obtain ⟨h4, _⟩ := (h2 y).mp hy
Proof state after:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
hxy : Finset.subtype (fun a => ¬a = s) x = Finset.subtype (fun a => ¬a = s) y
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
have h3' : ∀ x1 ∈ x, x1 ≠ s := by
  intro x1 hx1 hx1n; rw [hx1n] at hx1; exact h3 hx1
Proof state after:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
have h4' : ∀ y1 ∈ y, y1 ≠ s := by
  intro y1 hy1 hy1n; rw [hy1n] at hy1; exact h4 hy1
Proof state after:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
h4' : ∀ y1 ∈ y, y1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
h3' : ∀ x1 ∈ x, x1 ≠ s
h4' : ∀ y1 ∈ y, y1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
rw [Finset.subtype_map_of_mem h3',
    Finset.subtype_map_of_mem h4'] at hxy
Proof state after:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy : x = y
h3' : ∀ x1 ∈ x, x1 ≠ s
h4' : ∀ y1 ∈ y, y1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case left.mk.mk.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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy : x = y
h3' : ∀ x1 ∈ x, x1 ≠ s
h4' : ∀ y1 ∈ y, y1 ≠ s
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Tactic:
exact SetCoe.ext hxy
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 }
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
⊢ ∀ x1 ∈ x, x1 ≠ s
Tactic:
intro x1 hx1 hx1n
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)
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)
h2 : ∀ (a : Finset S), f a = Color.red ↔ s ∉ a ∧ f' (Finset.subtype (fun a => a ≠ s) a) = Color.red
b : { a // f a = Color.red } → { a // f' a = Color.red } :=
  fun x =>
    match x with
    | ⟨a, ha⟩ => ⟨Finset.subtype (fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : f x = Color.red
y : Finset S
hy : f y = Color.red
h3 : s ∉ x
right✝¹ : f' (Finset.subtype (fun a => a ≠ s) x) = Color.red
h4 : s ∉ y
right✝ : f' (Finset.subtype (fun a => a ≠ s) y) = Color.red
hxy :
  Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) x) =
    Finset.map (Function.Embedding.subtype fun a => ¬a = s) (Finset.subtype (fun a => ¬a = s) y)
x1 : S
hx1 : x1 ∈ x
hx1n : x1 = s
⊢ False