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

State before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
unfold Bal at hb
State after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)

State before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
obtain hf := bal_sum_f hb.1
State after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)

State before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
obtain ⟨mn, ln⟩ := bal_sum_n hb
State after:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)

State before:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
specialize hf f
State after:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
hf :
  ∑ i in range (t + 1), f (P i) =
    card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)

State before:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
hf :
  ∑ i in range (t + 1), f (P i) =
    card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
rwa [mn, smallParts_card, ln] at hf
State after:
no goals