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

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
Tactic:
rw [parts_union h, sum_union (parts_disjoint h)]
State after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) + ∑ x in largeParts h, f (P x) =
    card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)

State before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) + ∑ x in largeParts h, f (P x) =
    card (smallParts h) * f (minP t P) + card (largeParts h) * f (minP t P + 1)
Tactic:
congr
State after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = card (smallParts h) * f (minP t P)

case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = card (largeParts h) * f (minP t P + 1)

State before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = card (smallParts h) * f (minP t P)
Tactic:
rw [card_eq_sum_ones, sum_mul, one_mul]
State after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = ∑ x in smallParts h, f (minP t P)

State before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in smallParts h, f (P x) = ∑ x in smallParts h, f (minP t P)
Tactic:
apply sum_congr
State after:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ smallParts h = smallParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)

State before:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ smallParts h = smallParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
Tactic:
rfl
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
Tactic:
rw [smallParts]
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Tactic:
intro x
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Tactic:
rw [mem_filter]
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P → f (P x) = f (minP t P)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P → f (P x) = f (minP t P)
Tactic:
intro hx
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P
⊢ f (P x) = f (minP t P)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P
⊢ f (P x) = f (minP t P)
Tactic:
rw [hx.2]
State after:
no goals

State before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = card (largeParts h) * f (minP t P + 1)
Tactic:
rw [card_eq_sum_ones, sum_mul, one_mul]
State after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = ∑ x in largeParts h, f (minP t P + 1)

State before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = ∑ x in largeParts h, f (minP t P + 1)
Tactic:
apply sum_congr
State after:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ largeParts h = largeParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)

State before:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ largeParts h = largeParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Tactic:
rfl
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Tactic:
rw [largeParts]
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Tactic:
intro x
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Tactic:
rw [mem_filter]
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P + 1 → f (P x) = f (minP t P + 1)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P + 1 → f (P x) = f (minP t P + 1)
Tactic:
intro hx
State after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P + 1
⊢ f (P x) = f (minP t P + 1)

State before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P + 1
⊢ f (P x) = f (minP t P + 1)
Tactic:
rw [hx.2]
State after:
no goals