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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ A \ erase B v = A \ B ∪ {v}
Tactic:
ext a
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ erase B v ↔ a ∈ A \ B ∪ {v}

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ erase B v ↔ a ∈ A \ B ∪ {v}
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ erase B v → a ∈ A \ B ∪ {v}

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ B ∪ {v} → a ∈ A \ erase B v

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ erase B v → a ∈ A \ B ∪ {v}
Tactic:
intro h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ erase B v
⊢ a ∈ A \ B ∪ {v}

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ erase B v
⊢ a ∈ A \ B ∪ {v}
Tactic:
rw [mem_union, mem_sdiff] at *
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ erase B v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ erase B v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
Tactic:
rw [mem_erase] at h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬(a ≠ v ∧ a ∈ B)
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}

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

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
Tactic:
by_cases h' : a = v
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : a = v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : a = v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
Tactic:
right
State after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : a = v
⊢ a ∈ {v}

State before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : a = v
⊢ a ∈ {v}
Tactic:
exact mem_singleton.mpr h'
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
Tactic:
left
State after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B

State before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ (a ≠ v → ¬a ∈ B)
h' : ¬a = v
⊢ a ∈ A ∧ ¬a ∈ B
Tactic:
exact ⟨h.1, h.2 h'⟩
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
⊢ a ∈ A \ B ∪ {v} → a ∈ A \ erase B v
Tactic:
intro h
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A \ erase B v

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A \ erase B v
Tactic:
rw [mem_sdiff]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A ∧ ¬a ∈ erase B v

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A ∧ ¬a ∈ erase B v
Tactic:
rw [mem_erase]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A ∧ ¬(a ≠ v ∧ a ∈ B)

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A \ B ∪ {v}
⊢ a ∈ A ∧ ¬(a ≠ v ∧ a ∈ B)
Tactic:
rw [mem_union, mem_sdiff] at h
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
⊢ a ∈ A ∧ ¬(a ≠ v ∧ a ∈ B)

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
⊢ a ∈ A ∧ ¬(a ≠ v ∧ a ∈ B)
Tactic:
push_neg
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
⊢ a ∈ A ∧ (a ≠ v → ¬a ∈ B)

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ B ∨ a ∈ {v}
⊢ a ∈ A ∧ (a ≠ v → ¬a ∈ B)
Tactic:
cases h with
| inl h =>  exact ⟨h.1, fun _ => h.2⟩;
| inr h => 
  by_contra h'; push_neg at h' 
  have ha := hB hv
  have := mem_singleton.mp h; rw [← this] at ha 
  exact (h' ha).1 this
State after:
no goals

State before:
case a.mpr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ A ∧ ¬a ∈ B
⊢ a ∈ A ∧ (a ≠ v → ¬a ∈ B)
Tactic:
exact ⟨h.1, fun _ => h.2⟩
State after:
no goals

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
⊢ a ∈ A ∧ (a ≠ v → ¬a ∈ B)
Tactic:
by_contra h'
State after:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : ¬(a ∈ A ∧ (a ≠ v → ¬a ∈ B))
⊢ False

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : ¬(a ∈ A ∧ (a ≠ v → ¬a ∈ B))
⊢ False
Tactic:
push_neg at h'
State after:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
⊢ False

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
⊢ False
Tactic:
have ha := hB hv
State after:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : v ∈ A
⊢ False

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : v ∈ A
⊢ False
Tactic:
have := mem_singleton.mp h
State after:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : v ∈ A
this : a = v
⊢ False

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : v ∈ A
this : a = v
⊢ False
Tactic:
rw [← this] at ha
State after:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : a ∈ A
this : a = v
⊢ False

State before:
case a.mpr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
a : α
h : a ∈ {v}
h' : a ∈ A → a ≠ v ∧ a ∈ B
ha : a ∈ A
this : a = v
⊢ False
Tactic:
exact (h' ha).1 this
State after:
no goals