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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ Disjoint (erase A v) (insert v B)
Tactic:
rw [disjoint_insert_right, mem_erase]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A) ∧ Disjoint (erase A v) B

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A) ∧ Disjoint (erase A v) B
Tactic:
refine ⟨?_, disjoint_of_subset_left (erase_subset v A) hd⟩
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A)
Tactic:
push_neg
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ v ≠ v → ¬v ∈ A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ v ≠ v → ¬v ∈ A
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
h : v ≠ v
⊢ ¬v ∈ A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
h : v ≠ v
⊢ ¬v ∈ A
Tactic:
contradiction
State after:
no goals