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

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (smallParts h)
Tactic:
rw [smallParts]
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
have nem : ((range (t + 1)).image fun i => P i).Nonempty :=
  (Nonempty.image_iff _).mpr nonempty_range_succ
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
set a : ℕ := min' ((range (t + 1)).image fun i => P i) nem with ha
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
have ain := min'_mem ((range (t + 1)).image fun i => P i) nem
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
rw [← ha, mem_image] at ain
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
obtain ⟨k, hk1, hk2⟩ := ain
State after:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))

State before:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
use k
State after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ filter (fun i => P i = minP t P) (range (t + 1))

State before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ filter (fun i => P i = minP t P) (range (t + 1))
Tactic:
rw [mem_filter]
State after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ range (t + 1) ∧ P k = minP t P

State before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ range (t + 1) ∧ P k = minP t P
Tactic:
refine' ⟨hk1, _⟩
State after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ P k = minP t P

State before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ P k = minP t P
Tactic:
rw [ha] at hk2
State after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = min' (image (fun i => P i) (range (t + 1))) nem
⊢ P k = minP t P

State before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
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
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = min' (image (fun i => P i) (range (t + 1))) nem
⊢ P k = minP t P
Tactic:
exact hk2
State after:
no goals