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

State before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
unfold Bal at hb
State after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)

State before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
cases' hb with hb1 hb2
State after:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2 : psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)

State before:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2 : psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
rw [bal_sum' hb1, ← div_add_mod n (t + 1)] at hb2
State after:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2✝ : psum t P = n
hb2 : (t + 1) * minP t P + card (largeParts hb1) = (t + 1) * (n / (t + 1)) + n % (t + 1)
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)

State before:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2✝ : psum t P = n
hb2 : (t + 1) * minP t P + card (largeParts hb1) = (t + 1) * (n / (t + 1)) + n % (t + 1)
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
exact mod_tplus1 (largeParts_card hb1) (le_of_lt_succ (mod_lt n (succ_pos t))) hb2
State after:
no goals