internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.insert_C
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h2 : ¬M.t + 1 ≠ M.t + 1
h1 : v ∈ B
⊢ v ∈ B
Tactic:
exact h1
Proof state after:
no goals
Theorem: Turanpartition.mem_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
⊢ i ∈ range (M.t + 1) → v ∈ MultiPart.P M i → v ∈ M.A
Tactic:
intro hi hv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ v ∈ M.A
Theorem: Turanpartition.mem_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ v ∈ M.A
Tactic:
rw [M.uni]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ v ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Theorem: Turanpartition.mem_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ v ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
rw [mem_biUnion]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M a
Theorem: Turanpartition.mem_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M a
Tactic:
exact ⟨i, hi, hv⟩
Proof state after:
no goals
Theorem: Turanpartition.inv_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
M : MultiPart α
hA : v ∈ M.A
⊢ ∃ i, i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
Tactic:
rw [M.uni, mem_biUnion] at hA
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
M : MultiPart α
hA : ∃ a, a ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M a
⊢ ∃ i, i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
Theorem: Turanpartition.inv_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v : α
M : MultiPart α
hA : ∃ a, a ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M a
⊢ ∃ i, i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
Tactic:
exact hA
Proof state after:
no goals
Theorem: Turanpartition.biUnion_parts
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
ext x
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
rw [mem_biUnion]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
constructor
Proof state after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A → ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ (∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a) → x ∈ M.A
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A → ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
intro hA
Proof state after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
obtain ⟨i,hi⟩:= (inv_part hA)
Proof state after:
case a.mp.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
i : ℕ
hi : i ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mp.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : x ∈ M.A
i : ℕ
hi : i ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
exact ⟨i,hi⟩
Proof state after:
no goals
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ (∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a) → x ∈ M.A
Tactic:
intro hA
Proof state after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
⊢ x ∈ M.A
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
⊢ x ∈ M.A
Tactic:
obtain ⟨i, hi, hi2⟩ := hA
Proof state after:
case a.mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
i : ℕ
hi : i ∈ range (M.t + 1)
hi2 : x ∈ MultiPart.P M i
⊢ x ∈ M.A
Theorem: Turanpartition.biUnion_parts
Proof state before:
case a.mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
i : ℕ
hi : i ∈ range (M.t + 1)
hi2 : x ∈ MultiPart.P M i
⊢ x ∈ M.A
Tactic:
exact mem_part hi hi2
Proof state after:
no goals
Theorem: Turanpartition.card_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card M.A = ∑ i in range (M.t + 1), card (MultiPart.P M i)
Tactic:
rw [biUnion_parts M]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card (Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i) = ∑ i in range (M.t + 1), card (MultiPart.P M i)
Theorem: Turanpartition.card_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card (Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i) = ∑ i in range (M.t + 1), card (MultiPart.P M i)
Tactic:
rw [card_biUnion]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ), x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (MultiPart.P M x) (MultiPart.P M y)
Theorem: Turanpartition.card_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ), x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (MultiPart.P M x) (MultiPart.P M y)
Tactic:
intro x hx y hy ne
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (MultiPart.P M x) (MultiPart.P M y)
Theorem: Turanpartition.card_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (MultiPart.P M x) (MultiPart.P M y)
Tactic:
exact M.disj x hx y hy ne
Proof state after:
no goals
Theorem: Turanpartition.turan_bal
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : TuranPartition M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
rw [turanPartition_iff_not_moveable] at hM
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬Moveable M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Theorem: Turanpartition.turan_bal
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬Moveable M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
unfold Moveable at hM
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬¬Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Theorem: Turanpartition.turan_bal
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬¬Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
rw [not_not] at hM
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Theorem: Turanpartition.turan_bal
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
rw [card_uni]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (∑ i in range (M.t + 1), card (MultiPart.P M i)) fun i => card (MultiPart.P M i)
Theorem: Turanpartition.turan_bal
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (∑ i in range (M.t + 1), card (MultiPart.P M i)) fun i => card (MultiPart.P M i)
Tactic:
exact ⟨hM, rfl⟩
Proof state after:
no goals
Theorem: Turanpartition.uniq_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
⊢ i ∈ range (M.t + 1) → j ∈ range (M.t + 1) → v ∈ MultiPart.P M i → v ∈ MultiPart.P M j → i = j
Tactic:
intro hi hj hiv hjv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
⊢ i = j
Theorem: Turanpartition.uniq_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
⊢ i = j
Tactic:
by_contra h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
h : ¬i = j
⊢ False
Theorem: Turanpartition.uniq_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
h : ¬i = j
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨v, hiv, hjv⟩ (M.disj i hi j hj h)
Proof state after:
no goals
Theorem: Turanpartition.uniq_part'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
⊢ i ∈ range (M.t + 1) → j ∈ range (M.t + 1) → i ≠ j → v ∈ MultiPart.P M i → ¬v ∈ MultiPart.P M j
Tactic:
intro hi hj hiv ne
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : i ≠ j
ne : v ∈ MultiPart.P M i
⊢ ¬v ∈ MultiPart.P M j
Theorem: Turanpartition.uniq_part'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : i ≠ j
ne : v ∈ MultiPart.P M i
⊢ ¬v ∈ MultiPart.P M j
Tactic:
contrapose hiv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : ¬¬v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Theorem: Turanpartition.uniq_part'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : ¬¬v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Tactic:
push_neg at hiv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Theorem: Turanpartition.uniq_part'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Tactic:
rw [not_ne_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ i = j
Theorem: Turanpartition.uniq_part'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ i = j
Tactic:
exact uniq_part hi hj ne hiv
Proof state after:
no goals
Theorem: Turanpartition.sub_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ M.A
Tactic:
rw [M.uni]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Theorem: Turanpartition.sub_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Theorem: Turanpartition.sub_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
Tactic:
rw [mem_biUnion]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Theorem: Turanpartition.sub_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
Tactic:
exact ⟨i, hi, hx⟩
Proof state after:
no goals
Theorem: Turanpartition.two_parts
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤ card M.A
Tactic:
rw [card_uni,← sum_erase_add (range (M.t + 1)) _ hj]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤
    ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x) + card (MultiPart.P M j)
Theorem: Turanpartition.two_parts
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) + card (MultiPart.P M j) ≤
    ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x) + card (MultiPart.P M j)
Tactic:
apply Nat.add_le_add_right
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x)
Theorem: Turanpartition.two_parts
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x)
Tactic:
rw [← sum_erase_add ((range (M.t + 1)).erase j) _ (mem_erase_of_ne_of_mem hne hi)]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) + card (MultiPart.P M i)
Theorem: Turanpartition.two_parts
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hne : i ≠ j
⊢ card (MultiPart.P M i) ≤ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) + card (MultiPart.P M i)
Tactic:
apply Nat.le_add_left
Proof state after:
no goals
Theorem: Turanpartition.sdiff_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i
Tactic:
have := sub_part hi
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
this : MultiPart.P M i ⊆ M.A
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i
Theorem: Turanpartition.sdiff_part
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
this : MultiPart.P M i ⊆ M.A
⊢ M.A = M.A \ MultiPart.P M i ∪ MultiPart.P M i
Tactic:
rwa [sdiff_union_self_eq_union, left_eq_union_iff_subset]
Proof state after:
no goals
Theorem: Turanpartition.card_part_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card M.A = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)
Tactic:
nth_rw 1 [sdiff_part hi]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card (M.A \ MultiPart.P M i ∪ MultiPart.P M i) = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)
Theorem: Turanpartition.card_part_uni
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ card (M.A \ MultiPart.P M i ∪ MultiPart.P M i) = card (M.A \ MultiPart.P M i) + card (MultiPart.P M i)
Tactic:
apply card_disjoint_union sdiff_disjoint
Proof state after:
no goals
Theorem: Turanpartition.move_p
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) →
    MultiPart.P (move M hvi hj) k =
      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)
Tactic:
intro _
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
a✝ : k ∈ range (M.t + 1)
⊢ MultiPart.P (move M hvi hj) k =
    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)
Theorem: Turanpartition.move_p
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
a✝ : k ∈ range (M.t + 1)
⊢ MultiPart.P (move M hvi hj) k =
    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)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.move_Pcard
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 (MultiPart.P (move M hvi hj) k) =
      if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (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 (MultiPart.P (move M hvi hj) k) =
    if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
    else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1
Theorem: Turanpartition.move_Pcard
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 (MultiPart.P (move M hvi hj) k) =
    if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
    else if k = i then card (MultiPart.P M i) - 1 else card (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
      (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 (MultiPart.P M k)
    else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1
Theorem: Turanpartition.move_Pcard
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
      (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 (MultiPart.P M k)
    else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1
Tactic:
split_ifs with h h_1
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 (MultiPart.P M k) = card (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_1 : k = i
⊢ card (erase (MultiPart.P M i) v) = card (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_1 : ¬k = i
⊢ card (insert v (MultiPart.P M j)) = card (MultiPart.P M j) + 1
Theorem: Turanpartition.move_Pcard
Proof state before:
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 (MultiPart.P M k) = card (MultiPart.P M k)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.move_Pcard
Proof state before:
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_1 : k = i
⊢ card (erase (MultiPart.P M i) v) = card (MultiPart.P M i) - 1
Tactic:
exact card_erase_of_mem hvi.2
Proof state after:
no goals