internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.move_Pcard
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ card (insert v (MultiPart.P M j)) = card (MultiPart.P M j) + 1
Tactic:
apply card_insert_of_not_mem (uniq_part' hvi.1 hj.1 hj.2.symm hvi.2)
Proof state after:
no goals
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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 *
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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}
Theorem: Turanpartition.sdiff_erase
Proof 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'
Proof state after:
no goals
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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'⟩
Proof state after:
no goals
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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]
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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]
Proof 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)
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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)
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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)
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof state after:
no goals
Theorem: Turanpartition.sdiff_erase
Proof 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⟩
Proof state after:
no goals
Theorem: Turanpartition.sdiff_erase
Proof 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'
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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'
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_erase
Proof 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
Proof state after:
no goals
Theorem: Turanpartition.card_sdiff_erase
Proof 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
Proof 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
Theorem: Turanpartition.card_sdiff_erase
Proof 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]
Proof 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
Theorem: Turanpartition.card_sdiff_erase
Proof 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)
Proof state after:
no goals
Theorem: Turanpartition.card_sdiff_erase
Proof 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]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ ¬(v ∈ A ∧ ¬v ∈ B)
Theorem: Turanpartition.card_sdiff_erase
Proof 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
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
⊢ v ∈ A → v ∈ B
Theorem: Turanpartition.card_sdiff_erase
Proof 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 _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hB : B ⊆ A
hv : v ∈ B
_✝ : v ∈ A
⊢ v ∈ B
Theorem: Turanpartition.card_sdiff_erase
Proof 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
Proof state after:
no goals
Theorem: Turanpartition.sdiff_insert
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
⊢ A \ insert v B = erase (A \ B) v
Tactic:
ext
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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]
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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 *
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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⟩
Proof state after:
no goals
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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]
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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]
Proof 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)
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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
Proof 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
Theorem: Turanpartition.sdiff_insert
Proof 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⟩
Proof state after:
no goals
Theorem: Turanpartition.card_sdiff_insert
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (A \ insert v B) = card (A \ B) - 1
Tactic:
rw [sdiff_insert]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (erase (A \ B) v) = card (A \ B) - 1
Theorem: Turanpartition.card_sdiff_insert
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
B A : Finset α
hvB : ¬v ∈ B
hvA : v ∈ A
⊢ card (erase (A \ B) v) = card (A \ B) - 1
Tactic:
exact card_erase_of_mem (mem_sdiff.mpr ⟨hvA, hvB⟩)
Proof state after:
no goals
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
⊢ k ∈ range (M.t + 1) →
    card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
      if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
      else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Tactic:
intro hk
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Tactic:
rw [move_p hvi hj hk]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      ((move M hvi hj).A \
        if k ≠ i ∧ k ≠ j then MultiPart.P M k
        else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      ((move M hvi hj).A \
        if k ≠ i ∧ k ≠ j then MultiPart.P M k
        else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Tactic:
rw [move_a hvi hj]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      (M.A \
        if k ≠ i ∧ k ≠ j then MultiPart.P M k
        else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Theorem: Turanpartition.move_Pcard_sdiff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      (M.A \
        if k ≠ i ∧ k ≠ j then MultiPart.P M k
        else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
    else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Tactic:
split_ifs
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝ : k ≠ i ∧ k ≠ j
⊢ card (M.A \ MultiPart.P M k) = card (M.A \ MultiPart.P M k)

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝¹ : ¬(k ≠ i ∧ k ≠ j)
h✝ : k = i
⊢ card (M.A \ erase (MultiPart.P M i) v) = card (M.A \ MultiPart.P M i) + 1

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h✝¹ : ¬(k ≠ i ∧ k ≠ j)
h✝ : ¬k = i
⊢ card (M.A \ insert v (MultiPart.P M j)) = card (M.A \ MultiPart.P M j) - 1