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

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ range (t + 1) = smallParts h ∪ largeParts h
Tactic:
have := con_sum h
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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