Theorem: Turanpartition.large_parts' (Turan4/Turanpartition.lean)

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

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

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

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

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

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

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, _⟩
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

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

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

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
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 ∈ range (t + 1) ∧ ¬P a = minP t P → a ∈ range (t + 1) ∧ P a = minP t P + 1
Tactic:
intro h'
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

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, _⟩
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

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

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

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

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

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