Theorem: Turanpartition.card_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
⊢ card (A \ erase B v) = card (A \ B) + 1
Tactic:
have hv2 : v ∉ A \ B := by rw [mem_sdiff]; push_neg; intro _; exact hv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ erase B v) = card (A \ B) + 1

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ erase B v) = card (A \ B) + 1
Tactic:
rw [sdiff_erase hB hv]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ B ∪ {v}) = card (A \ B) + 1

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
hv2 : ¬v ∈ A \ B
⊢ card (A \ B ∪ {v}) = card (A \ B) + 1
Tactic:
exact card_disjoint_union (disjoint_singleton_right.mpr hv2)
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ ¬v ∈ A \ B
Tactic:
rw [mem_sdiff]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ ¬(v ∈ A ∧ ¬v ∈ B)

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ v ∈ A → v ∈ B
Tactic:
intro _
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
_✝ : v ∈ A
⊢ v ∈ B

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
_✝ : v ∈ A
⊢ v ∈ B
Tactic:
exact hv
State after:
no goals