Lean: closing parity goals mixing ℕ, ℤ casts and big sums with generalize + omega

Goal shape: Even h ↔ 4 ∣ φ N with hypotheses hT : (C : ℤ) - 2 * D = (2 - c) * h (D a Finset sum, C a Finset.card) and hcard : 2 * C = φ N in ℕ, and c = ±1. omega cannot see through the sum or card terms reliably, so first generalize (∑ a ∈ range m, ...) = D at hT and generalize #{a ∈ range m | ...} = C at hT hcard, then rw [Nat.even_iff] and rcases hc with e | e <;> rw [e] at hT <;> omega. omega handles the ↑C, ↑h casts from ℕ to ℤ and divisibility by numerals. Related: Nat.coprime_self_sub_right (h : m ≤ n) : Coprime n (n - m) ↔ Coprime n m is the lemma for reflecting coprimality a ↦ N - a when counting units in [0, N/2).