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

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
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))

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
State after:
no goals