Theorem: Turanpartition.sdiff_insert (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
⊢ A \ insert v B = erase (A \ B) v
Tactic:
ext
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ A \ insert v B ↔ a✝ ∈ erase (A \ B) v

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ A \ insert v B ↔ a✝ ∈ erase (A \ B) v
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ A \ insert v B → a✝ ∈ erase (A \ B) v

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ erase (A \ B) v → a✝ ∈ A \ insert v B

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ A \ insert v B → a✝ ∈ erase (A \ B) v
Tactic:
intro h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A \ insert v B
⊢ a✝ ∈ erase (A \ B) v

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A \ insert v B
⊢ a✝ ∈ erase (A \ B) v
Tactic:
rw [mem_erase]
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A \ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A \ B

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A \ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A \ B
Tactic:
rw [mem_sdiff] at *
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ ¬a✝ ∈ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ ¬a✝ ∈ insert v B
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B
Tactic:
rw [mem_insert] at h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ ¬(a✝ = v ∨ a✝ ∈ B)
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ ¬(a✝ = v ∨ a✝ ∈ B)
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B
Tactic:
push_neg at h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B
⊢ a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B
Tactic:
exact ⟨h.2.1, h.1, h.2.2⟩
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
⊢ a✝ ∈ erase (A \ B) v → a✝ ∈ A \ insert v B
Tactic:
intro h
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ erase (A \ B) v
⊢ a✝ ∈ A \ insert v B

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ∈ erase (A \ B) v
⊢ a✝ ∈ A \ insert v B
Tactic:
rw [mem_erase] at h
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A \ insert v B

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A \ insert v B
Tactic:
rw [mem_sdiff]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ ¬a✝ ∈ insert v B

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ ¬a✝ ∈ insert v B
Tactic:
rw [mem_insert]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ ¬(a✝ = v ∨ a✝ ∈ B)

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ ¬(a✝ = v ∨ a✝ ∈ B)
Tactic:
push_neg
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A \ B
⊢ a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B
Tactic:
rw [mem_sdiff] at h
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B
⊢ a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
a✝ : α
h : a✝ ≠ v ∧ a✝ ∈ A ∧ ¬a✝ ∈ B
⊢ a✝ ∈ A ∧ a✝ ≠ v ∧ ¬a✝ ∈ B
Tactic:
exact ⟨h.2.1, h.1, h.2.2⟩
State after:
no goals