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

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⟩
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 }

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]
State after:
no goals

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
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

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
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⟩

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
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⟩

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]
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

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
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

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
State after:
no goals

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⟩
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⟩

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⟩
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⟩

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]
State after:
no goals