internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.con_sum
Proof state before:
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
⊢ b ≤ a + 1
Tactic:
obtain ⟨k, hk, hak⟩ := ain
Proof state after:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
⊢ b ≤ a + 1
Theorem: Turanpartition.con_sum
Proof state before:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
bin : ∃ a, a ∈ range (t + 1) ∧ P a = b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
⊢ b ≤ a + 1
Tactic:
obtain ⟨l, hl, hbl⟩ := bin
Proof state after:
case intro.intro.intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ b ≤ a + 1
Theorem: Turanpartition.con_sum
Proof state before:
case intro.intro.intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ b ≤ a + 1
Tactic:
rw [← hak, ← hbl]
Proof state after:
case intro.intro.intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ P l ≤ P k + 1
Theorem: Turanpartition.con_sum
Proof state before:
case intro.intro.intro.intro
t : ℕ
P : ℕ → ℕ
h : ∀ (i : ℕ), i ∈ range (t + 1) → ∀ (j : ℕ), j ∈ range (t + 1) → P i ≤ P j + 1
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
b : ℕ := max' (image (fun i => P i) (range (t + 1))) nem
hb : b = max' (image (fun i => P i) (range (t + 1))) nem
i : ℕ
hi : i ∈ range (t + 1)
ale : a ≤ P i
leb : P i ≤ b
k : ℕ
hk : k ∈ range (t + 1)
hak : P k = a
l : ℕ
hl : l ∈ range (t + 1)
hbl : P l = b
⊢ P l ≤ P k + 1
Tactic:
exact h l hl k hk
Proof state after:
no goals
Theorem: Turanpartition.large_parts'
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ largeParts h = filter (fun i => ¬P i = minP t P) (range (t + 1))
Tactic:
have := con_sum h
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ largeParts h = filter (fun i => ¬P i = minP t P) (range (t + 1))
Theorem: Turanpartition.large_parts'
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ largeParts h = filter (fun i => ¬P i = minP t P) (range (t + 1))
Tactic:
unfold largeParts
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ filter (fun i => P i = minP t P + 1) (range (t + 1)) = filter (fun i => ¬P i = minP t P) (range (t + 1))
Theorem: Turanpartition.large_parts'
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ filter (fun i => P i = minP t P + 1) (range (t + 1)) = filter (fun i => ¬P i = minP t P) (range (t + 1))
Tactic:
ext a
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) ↔ a ∈ filter (fun i => ¬P i = minP t P) (range (t + 1))
Theorem: Turanpartition.large_parts'
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) ↔ a ∈ filter (fun i => ¬P i = minP t P) (range (t + 1))
Tactic:
rw [mem_filter, mem_filter]
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1 ↔ a ∈ range (t + 1) ∧ ¬P a = minP t P
Theorem: Turanpartition.large_parts'
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1 ↔ a ∈ range (t + 1) ∧ ¬P a = minP t P
Tactic:
constructor
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1 → a ∈ range (t + 1) ∧ ¬P a = minP t P

case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ ¬P a = minP t P → a ∈ range (t + 1) ∧ P a = minP t P + 1
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1 → a ∈ range (t + 1) ∧ ¬P a = minP t P
Tactic:
intro h'
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ ¬P a = minP t P
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ ¬P a = minP t P
Tactic:
refine' ⟨h'.1, _⟩
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ ¬P a = minP t P
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ ¬P a = minP t P
Tactic:
intro h2
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
h2 : P a = minP t P
⊢ False
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ P a = minP t P + 1
h2 : P a = minP t P
⊢ False
Tactic:
rw [h2] at h'
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ minP t P = minP t P + 1
h2 : P a = minP t P
⊢ False
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ minP t P = minP t P + 1
h2 : P a = minP t P
⊢ False
Tactic:
exact succ_ne_self (minP t P) h'.2.symm
Proof state after:
no goals
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ ¬P a = minP t P → a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
intro h'
Proof state after:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
refine' ⟨h'.1, _⟩
Proof state after:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
⊢ P a = minP t P + 1
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
⊢ P a = minP t P + 1
Tactic:
specialize this a h'.1
Proof state after:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
this : P a = minP t P ∨ P a = minP t P + 1
⊢ P a = minP t P + 1
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
this : P a = minP t P ∨ P a = minP t P + 1
⊢ P a = minP t P + 1
Tactic:
cases this with
| inl h => 
  exfalso; exact h'.2 h
| inr h => exact h
Proof state after:
no goals
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr.inl
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
h : P a = minP t P
⊢ P a = minP t P + 1
Tactic:
exfalso
Proof state after:
case a.mpr.inl.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
h : P a = minP t P
⊢ False
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr.inl.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
h : P a = minP t P
⊢ False
Tactic:
exact h'.2 h
Proof state after:
no goals
Theorem: Turanpartition.large_parts'
Proof state before:
case a.mpr.inr
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
h' : a ∈ range (t + 1) ∧ ¬P a = minP t P
h : P a = minP t P + 1
⊢ P a = minP t P + 1
Tactic:
exact h
Proof state after:
no goals
Theorem: Turanpartition.parts_disjoint
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Disjoint (smallParts h) (largeParts h)
Tactic:
convert disjoint_filter_filter_neg (range (t + 1)) (range (t + 1)) fun i => P i = minP t P
Proof state after:
case h.e'_5
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ largeParts h = filter (fun a => ¬P a = minP t P) (range (t + 1))
Theorem: Turanpartition.parts_disjoint
Proof state before:
case h.e'_5
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ largeParts h = filter (fun a => ¬P a = minP t P) (range (t + 1))
Tactic:
exact large_parts' h
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ range (t + 1) = smallParts h ∪ largeParts h
Tactic:
have := con_sum h
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ range (t + 1) = smallParts h ∪ largeParts h
Theorem: Turanpartition.parts_union
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
⊢ range (t + 1) = smallParts h ∪ largeParts h
Tactic:
ext a
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔ a ∈ smallParts h ∪ largeParts h
Theorem: Turanpartition.parts_union
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔ a ∈ smallParts h ∪ largeParts h
Tactic:
unfold smallParts
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∪ largeParts h
Theorem: Turanpartition.parts_union
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∪ largeParts h
Tactic:
unfold largeParts
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∪ filter (fun i => P i = minP t P + 1) (range (t + 1))
Theorem: Turanpartition.parts_union
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∪ filter (fun i => P i = minP t P + 1) (range (t + 1))
Tactic:
rw [mem_union]
Proof state after:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
Theorem: Turanpartition.parts_union
Proof state before:
case a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ↔
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
Tactic:
constructor
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) →
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))

case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) →
    a ∈ range (t + 1)
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) →
    a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
Tactic:
intro ha
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
ha : a ∈ range (t + 1)
⊢ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
ha : a ∈ range (t + 1)
⊢ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1))
Tactic:
rw [mem_filter, mem_filter]
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
ha : a ∈ range (t + 1)
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
ha : a ∈ range (t + 1)
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
specialize this a ha
Proof state after:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
this : P a = minP t P ∨ P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp
t : ℕ
P : ℕ → ℕ
h : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
this : P a = minP t P ∨ P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
cases this with
| inl h => 
  left; exact ⟨ha,h⟩
| inr h => 
  right; exact ⟨ha, h⟩
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp.inl
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
left
Proof state after:
case a.mp.inl.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P
⊢ a ∈ range (t + 1) ∧ P a = minP t P
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp.inl.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P
⊢ a ∈ range (t + 1) ∧ P a = minP t P
Tactic:
exact ⟨ha,h⟩
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp.inr
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
right
Proof state after:
case a.mp.inr.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1
Theorem: Turanpartition.parts_union
Proof state before:
case a.mp.inr.h
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
a : ℕ
ha : a ∈ range (t + 1)
h : P a = minP t P + 1
⊢ a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
exact ⟨ha, h⟩
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ filter (fun i => P i = minP t P) (range (t + 1)) ∨ a ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) →
    a ∈ range (t + 1)
Tactic:
rw [mem_filter, mem_filter]
Proof state after:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1 → a ∈ range (t + 1)
Theorem: Turanpartition.parts_union
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
⊢ a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1 → a ∈ range (t + 1)
Tactic:
intro hr
Proof state after:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
hr : a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ a ∈ range (t + 1)
Theorem: Turanpartition.parts_union
Proof state before:
case a.mpr
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
hr : a ∈ range (t + 1) ∧ P a = minP t P ∨ a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ a ∈ range (t + 1)
Tactic:
cases hr with
| inl h => exact h.1
| inr h => exact h.1
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
case a.mpr.inl
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h : a ∈ range (t + 1) ∧ P a = minP t P
⊢ a ∈ range (t + 1)
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Turanpartition.parts_union
Proof state before:
case a.mpr.inr
t : ℕ
P : ℕ → ℕ
h✝ : Balanced t P
this : ∀ (i : ℕ), i ∈ range (t + 1) → P i = minP t P ∨ P i = minP t P + 1
a : ℕ
h : a ∈ range (t + 1) ∧ P a = minP t P + 1
⊢ a ∈ range (t + 1)
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Turanpartition.parts_card_add
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (smallParts h) + card (largeParts h) = t + 1
Tactic:
rw [← card_range (t + 1), parts_union h, card_disjoint_union (parts_disjoint h)]
Proof state after:
no goals
Theorem: Turanpartition.largeParts_card
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (largeParts h) ≤ t
Tactic:
have := Nat.add_le_add (card_pos.mpr (small_nonempty h)) (le_refl (card (largeParts h)))
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t
Theorem: Turanpartition.largeParts_card
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : succ 0 + card (largeParts h) ≤ card (smallParts h) + card (largeParts h)
⊢ card (largeParts h) ≤ t
Tactic:
rw [parts_card_add h,add_comm] at this
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : card (largeParts h) + succ 0 ≤ t + 1
⊢ card (largeParts h) ≤ t
Theorem: Turanpartition.largeParts_card
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
this : card (largeParts h) + succ 0 ≤ t + 1
⊢ card (largeParts h) ≤ t
Tactic:
apply  le_of_add_le_add_right this
Proof state after:
no goals
Theorem: Turanpartition.smallParts_card
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ card (smallParts h) = t + 1 - card (largeParts h)
Tactic:
rw [← parts_card_add h,add_tsub_cancel_right]
Proof state after:
no goals
Theorem: Turanpartition.bal_sum_f
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
Tactic:
rw [parts_union h, sum_union (parts_disjoint h)]
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) + ∑ x in largeParts h, f (P x) =
    card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) + ∑ x in largeParts h, f (P x) =
    card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
Tactic:
congr
Proof state after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = card (smallParts h) * f (minP t P)

case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = card (largeParts h) * f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = card (smallParts h) * f (minP t P)
Tactic:
rw [card_eq_sum_ones, sum_mul, one_mul]
Proof state after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = ∑ x in smallParts h, f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = ∑ x in smallParts h, f (minP t P)
Tactic:
apply sum_congr
Proof state after:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ smallParts h = smallParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)