[{"type":"thinking","thinking":"Confirmed:\n- `iteratedDeriv_sum (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) : iteratedDeriv n (∑ i ∈ I, f i) x = ∑ i ∈ I, iteratedDeriv n (f i) x` — Pi.sum form ⟹ need the funext bridge (like deriv_Gprim) ✓\n- `iteratedDeriv_const_mul (c : 𝔸) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (c * f ·) x = c * iteratedDeriv n f x` — function form `c * f ·` — Pi.mul — so my term lambda `fun w => c_j * (w−1)^j` needs bridging to `c_j * (fun w => (w−1)^j)` — defeq; rw [iteratedDeriv_const_mul ...] needs syntactic match on `iteratedDeriv i (c_j * f ·) 1` — the goal after iteratedDeriv_sum + sum_congr would have iteratedDeriv i (fun w => c_j * (w−1)^j) 1 — the lemma's LHS pattern is `iteratedDeriv n (c * f ·) x` — (c * f ·) is eta-expanded Pi.mul — is `fun w => c_j * (w−1)^j` syntactically `c * f ·`? `c * f ·` = fun x => (c*f) x = fun x => c x... hmm — `c * f` with c : ℂ (not a function!) — wait: iteratedDeriv_const_mul (c : 𝔸) {f : 𝕜 → 𝔸} : iteratedDeriv n (c * f ·) — `c * f ·`?? c is a CONSTANT in 𝔸, f is a function — c * f is the scalar-style multiplication 𝔸 → (𝕜→𝔸) → (𝕜→𝔸)? There's `Pi.instMul`? No — c * f where c : 𝔸 and f : 𝕜 → 𝔸 — this is `HMul 𝔸 (𝕜→𝔸) (𝕜→𝔸)` — the \"constant-times-function\" instance — (c * f ·) x = c * f x. This is NOT Pi.mul (which is (f * g) x = f x * g x for f g functions). It's the `HMul` for constant-times-function — exists? The elaborated form `c * f ·` suggests a special notation/instance: `Mul.const`? Hmm — in Mathlib, for c : 𝔸 and f : 𝕜 → 𝔸, `c * f` could elaborate as `fun x => c * f x` via... there IS `Pi.instMul` requiring c : ∀ i, β i — c : 𝔸 is not a function — so how does c * f typecheck? There must be an instance `HMul α (ι → α) (ι → α)`?? I'm not sure this exists generally... BUT the lemma statement compiles in Mathlib, so `c * f ·` is meaningful — probably via `Mul (𝕜 → 𝔸)`? no. Hmm — actually I bet it's: (c * f ·) where c * f · is the partial application of HMul.hMul c to f then... no.\n\nLet me think again: `theorem iteratedDeriv_const_mul {n : ℕ} {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (c * f ·) x = c * iteratedDeriv n f x`. For `c * f ·` to typecheck with c : 𝔸, f : 𝕜 → 𝔸: there must be HMul 𝔸 (𝕜 → 𝔸) ?. In Mathlib, `Mul.toConstMul`? or the instance `Pi.instMul`... Actually — I recall `instHMulConst`? hmm. There IS: `Mathlib.Algebra.Group.Pi.Lemmas`... For our purposes, what matters is whether the rewrite matches. My term: fun w => (c_j : ℂ) * (w−1)^j. The lemma's LHS: (c * f ·) which elaborates to fun x => HMul.hMul c (f x)?? — i.e. `fun x => c * f x` with the FIRST arg the constant. My lambda: fun w => c_j * (w−1)^j — with f := fun w => (w−1)^j: c * f · = fun w => c_j * (w−1)^j ✓ SAME up to how the elaborator represents it. If `c * f ·` is fun x => c * f x (via whatever instance), then it IS the lambda `fun w => c_j * (w−1)^j` syntactically-ish (up to the instance unfolding). rw matching is up to syntactic/instances — should match since both are `fun x => HMul.hMul c (f x)` with the same instance. RISK: moderate. This is exactly how the lemma is meant to be applied (the docstring says \"multiplication is in a division ring\" variant iteratedDeriv_const_mul_field has NO hypothesis — even better for ℂ!): \n\n`iteratedDeriv_const_mul_field {n : ℕ} (c : 𝕜') (f : 𝕜 → 𝕜') : iteratedDeriv n (c * f ·) x = c * iteratedDeriv n f x` — @[simp], NO ContDiff hypothesis (field version — constants are... wait why no differentiability needed? because f is iteratedDeriv-able regardless (totalized)? For fields, iteratedDeriv_const_mul_field holds unconditionally (junk-compatible). USE THIS ONE — simpler! `iteratedDeriv_const_mul_field (c : ℂ) (f : ℂ → ℂ) : iteratedDeriv n (c * f ·) x = c * iteratedDeriv n f x` — and it's @[simp] so `simp [iteratedDeriv_const_mul_field]`... \n\nSo in hpoint: rw [iteratedDeriv_const_mul_field, hdp j] — hmm the match issue remains but as a simp lemma it should fire. If the match fails, fallback: the bridge `show iteratedDeriv i ((c_j) * (fun w => (w−1)^j) ·) 1 = ...`. I'll handle at compile time.\n\nOK — now also `sum_fn` was mentioned — fine.\n\nNow, one thing I should double check: `Finset.sum_eq_single` exact name/form: `Finset.sum_eq_single (a) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) : ∑ x ∈ s, f x = f a` ✓ standard.\n\nAlso `Nat.descFactorial_self : n.descFactorial n = n !` ✓ (A_iter used: simp [Nat.descFactorial_self] ✓).\n\n`Nat.cast_ne_zero : (n : R) ≠ 0 ↔ n ≠ 0` ✓.\n\nAlright — also for hnm: I realize `Nat.cast_analyticOrderNatAt htop` — its statement: `Nat.cast_analyticOrderNatAt (hf : analyticOrderAt f z₀ ≠ ⊤) : ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀` — @[simp]. rw [← Nat.cast_analyticOrderNatAt htop] at h2 ✓.\n\nNow write the file. Let me also decide the exact statement forms:\n\nNote on ppart_mul_pow's sum_bij — direction: I want to rewrite the Icc-sum into the range-sum. Statement: `(s - 1) ^ (n + 1) * ppart n s = TaylP n s`. Proof unfolds ppart (Finset.mul_sum), giving Σ_{i ∈ Icc 1 (n+1)} (s−1)^{n+1}·(Acoeff n i/(s−1)^i); then sum_bij (i ↦ n+1−i) : Icc 1 (n+1) → range (n+1) with term equality to (iteratedDeriv j Ffun 1/j!)·(s−1)^j.\n\nFinset.sum_bij signature (from session-016 notes): Finset.sum_bij (i, hi, i_inj, i_surj, h) — i.e., sum_bij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i s) (i_surj : Set.SurjOn i s t) (h : ∀ a ∈ s, f a = g (i a)) : ∑ a ∈ s, f a = ∑ b ∈ t, g b. In ResW1_eq_sum the application was `apply Finset.sum_bij (fun i _ => n - i)` with 5 subsequent goals: mem, inj, surj, term — the inj/surj in ResW1 were given as `intro a₁ ha₁ a₂ ha₂ h` (InjOn unfolded) and `intro j hj; exact ⟨...⟩` (SurjOn unfolded: ∀ b ∈ t, ∃ a ∈ s, i a = b) ✓ copy that style.\n\nFor my bij: i ↦ n + 1 − i from Icc 1 (n+1) to range (n+1):\n- mem: i ∈ [1, n+1] ⟹ n+1−i ∈ [0, n] ✓ omega.\n- inj: n+1−a₁ = n+1−a₂ with a₁,a₂ ≤ n+1 ⟹ a₁ = a₂ ✓ omega.\n- surj: j ∈ [0, n] ⟹ i := n+1−j ∈ [1, n+1], n+1−i = j ✓ omega.\n- term: (s−1)^{n+1}·(Acoeff n i/(s−1)^i) = (iteratedDeriv (n+1−i) (Ffun n) 1/(n+1−i)!)·(s−1)^{n+1−i} — with the summand on the range side being g j = (iteratedDeriv j (Ffun n) 1 / j !)·(s−1)^j evaluated at j = n+1−i: (iteratedDeriv (n+1−i) Ffun 1/(n+1−i)!)·(s−1)^{n+1−i} ✓ and Acoeff n i = iteratedDeriv (n+1−i) Ffun 1/(n+1−i)! by def (Ffun bridge rfl).\n\nSo the term goal: (s−1)^{n+1}·(Acoeff n i/(s−1)^i) = (iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i) !)·(s−1)^{n+1−i}.\nRewrite Acoeff via show/rfl-bridge:\n```lean\n    · intro i hi\n      rw [Finset.mem_Icc] at hi\n      have hA : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i) ! := rfl\n      rw [hA]\n      have e : (s - 1) ^ (n + 1) = (s - 1) ^ i * (s - 1) ^ (n + 1 - i) := by\n        rw [← pow_add]; congr 1; omega\n      rw [e]\n      field_simp [hs1, pow_ne_zero i hs1]\n      ring\n```\nAfter rw [hA]: goal (s−1)^{n+1}·((D/(n+1−i)!)/(s−1)^i) = (D/(n+1−i)!)·(s−1)^{n+1−i} where D := iteratedDeriv (n+1−i) Ffun 1. rw [e]: ((s−1)^i·(s−1)^{n+1−i})·(D/(n+1−i)!/(s−1)^i) = ... field_simp [pow_ne_zero i hs1] — clears /(s−1)^i and the factorial? factorial cast is a ℂ numeral — field_simp treats (n+1−i)! cast as a nonzero?? It doesn't know it's nonzero — field_simp would need it as hypothesis... The factorial appears on BOTH sides identically (D/(n+1−i)!) — field_simp might multiply out the factorial division too and then need (fac ≠ 0). To avoid: pull D/(n+1−i)! as an atom: set-free approach — the equation is A · X where... Let me restructure: goal = (s−1)^{n+1}·(C/(s−1)^i) = C·(s−1)^{n+1−i} with C := D/(n+1−i)! — prove the generic:\n```lean\n      have key : ∀ C : ℂ, (s - 1) ^ (n + 1) * (C / (s - 1) ^ i) = C * (s - 1) ^ (n + 1 - i) := by\n        intro C\n        rw [e]\n        field_simp [pow_ne_zero i hs1]\n        ring\n      exact key _\n```\nfield_simp [pow_ne_zero i hs1] on ((s−1)^i·(s−1)^{n+1−i})·(C/(s−1)^i) = C·(s−1)^{n+1−i}: multiplies both sides by (s−1)^i: (s−1)^i·(s−1)^{n+1−i}·C = C·(s−1)^{n+1−i}·(s−1)^i ✓ ring. But does field_simp produce exactly that? It clears denominators and moves things — the result should be closed by ring ✓ common pattern. Alternatively:\n```lean\n        rw [e, mul_comm ((s-1)^i) ((s-1)^(n+1-i))]... \n```\nsimplest robust: \n```lean\n      have key : ∀ C : ℂ, (s - 1) ^ (n + 1) * (C / (s - 1) ^ i) = C * (s - 1) ^ (n + 1 - i) := by\n        intro C\n        have hi' : (s - 1) ^ i ≠ 0 := pow_ne_zero i hs1\n        rw [e]\n        -- ((s−1)^i * (s−1)^{n+1−i}) * (C / (s−1)^i) = C * (s−1)^{n+1−i}\n        field_simp [hi']\n        ring\n```\n✓.\n\nThen the final: after sum_bij the Icc-sum equals the range-sum; the goal was `(s−1)^{n+1} * ppart n s = TaylP n s`:\n```lean\nlemma ppart_mul_pow {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    (s - 1) ^ (n + 1) * ppart n s = TaylP n s := by\n  have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs\n  show (s - 1) ^ (n + 1) * (∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (s - 1) ^ i) =\n    ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (s - 1) ^ j\n  rw [Finset.mul_sum]\n  apply Finset.sum_bij (fun i _ => n + 1 - i)\n  ...\n```\nThe `show` unfolds ppart n s and TaylP n s by defeq ✓ (ppart n s := Σ ...; TaylP n w := Σ ...) — `show` with the unfolded form ✓ should work (delta+beta defeq).\n\nHmm — Finset.mul_sum : a * ∑ i, f i = ∑ i, a * f i ✓ (`Finset.mul_sum` — in recent Mathlib it's `Finset.mul_sum : b * ∑ i ∈ s, f i = ∑ i ∈ s, b * f i` ✓).\n\nThe bij goals with sum_bij (fun i _ => n + 1 - i): goals order per session-016 notes: (i, hi, i_inj, i_surj, h) — from ResW1_eq_sum's structure: \n```\n  apply Finset.sum_bij (fun i _ => n - i)\n  · intro i hi; ... (mem)\n  · intro a₁ ha₁ a₂ ha₂ h; ... (inj)\n  · intro j hj; exact ⟨n - j, ..., ...⟩ (surj)\n  · intro i hi; ... (term)\n```\n✓ copy.\n\nTerm goal details: after the above, goal: (s−1)^{n+1} * (Acoeff n i / (s−1)^i) = (iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i)!) * (s−1)^{n+1−i} — wait — the range-side summand evaluated at j := n+1−i: (iteratedDeriv j (Ffun n) 1 / j !) * (s−1)^j with j := n+1−i — Lean beta-reduces ✓. So goal RHS: (iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i)!) * (s−1)^{n+1−i}. And hA : Acoeff n i = iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i)! — rfl? Acoeff n i := iteratedDeriv (n+1−i) (fun w : ℂ => (w^n − (w−1)^n) * hLi w) 1 / (n+1−i)! and Ffun n := fun w : ℂ => (w^n − (w−1)^n) * hLi w — delta-unfold Ffun: SAME ✓ rfl ✓ (Acoeff's equation vs Ffun — both defs — `rfl` with default transparency unfolds both ✓ should work).\n\nAlso — the factorial in hA's RHS: `(n + 1 - i) !` — Acoeff used `Nat.factorial (n + 1 - i)` — is `(n+1−i) !` (scoped notation) the same term as `Nat.factorial (n+1−i)`? YES — the notation IS Nat.factorial ✓ rfl unaffected.\n\nBut the CAST: Acoeff n i = iteratedDeriv ... / Nat.factorial (n+1−i) — the division ℂ/ℕ → the elaborator inserts cast: / ↑(Nat.factorial (n+1−i)). In my hA statement `/ (n + 1 - i) !` — same elaboration ✓.\n\nOK. Now — one more part: Jlag_mul_pow — the field_simp step. Let me reconsider:\n```lean\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    show (s / (s - 1)) ^ n - 1 = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n\n    rw [div_pow]\n    field_simp [pow_ne_zero n h1]\n```\nAfter div_pow: (s^n/(s−1)^n) − 1 = (s^n − (s−1)^n)/(s−1)^n. field_simp [pow_ne_zero n h1]: LHS has /(s−1)^n — clears: s^n − (s−1)^n = s^n − (s−1)^n ✓ closed by field_simp itself (it proves equalities up to ring-normalization — field_simp CLOSES refl-after-normalization goals? field_simp normalizes both sides; if identical it closes via ring1/rfl internally? — field_simp is a finishing-tactic-ish: it simplifies toward clearing denominators; if both sides become syntactically equal it closes by rfl? Not guaranteed — safer to append `ring`: field_simp leaves `s^n − (s−1)^n = s^n − (s−1)^n`?? Actually field_simp followed by nothing might close it if it normalizes to rfl. Standard usage: `field_simp [...]` then `ring`. Let me write field_simp then ring — if field_simp already closed it, the ring errors \"no goals\" — hmm. Common robust pattern: `field_simp [...]`; if error \"no goals\" at ring — remove. I'll test at compile. To be safest: use `rw [div_pow]; field_simp [pow_ne_zero n h1]` and if unsolved add ring — compile will tell.\n\nActually for hk there's an even simpler route:\n```lean\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    show (s / (s - 1)) ^ n - 1 = _\n    rw [div_pow, eq_div_iff (pow_ne_zero n h1)]  -- hmm eq_div_iff : a/c = b ↔ a = b*c (c≠0)?\n    ring\n```\neq_div_iff (hc : c ≠ 0) : a / c = b ↔ a = b * c. After div_pow: s^n/(s−1)^n − 1 = (s^n−(s−1)^n)/(s−1)^n — rw [eq_div_iff (pow_ne_zero n h1)]: (s^n/(s−1)^n − 1)·(s−1)^n = s^n − (s−1)^n — hmm the LHS still has a division — rw [eq_div_iff] applies to the OUTERMOST = with / on RHS ✓: goal becomes s^n/(s−1)^n − 1 = (s^n − (s−1)^n) / (s−1)^n → transforms to... `eq_div_iff : a / c = b ↔ a = b * c` — the goal's RHS is the division — match a/c = b with a := s^n−(s−1)^n, c := (s−1)^n, b := LHS — result: s^n−(s−1)^n = (s^n/(s−1)^n − 1)·(s−1)^n — still division on RHS — ring can't handle / — need field_simp first to clear the remaining division... messy. Direct approach:\n```lean\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    have h1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs1\n    show (s / (s - 1)) ^ n - 1 = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n\n    rw [div_pow]\n    have h2 : (s - 1) ^ n ≠ 0 := pow_ne_zero n h1\n    field_simp [h2]\n```\nfield_simp [h2] on s^n/(s−1)^n − 1 = (s^n−(s−1)^n)/(s−1)^n: multiplies out: s^n − (s−1)^n = s^n − (s−1)^n — field_simp closes goals that become rfl? To be safe add `ring`?? If field_simp closes it, `ring` errors. Standard Mathlib style: `field_simp [h2]` often fully closes such goals (it ends with ring1 internally? No — field_simp is simp-based; when both sides normalize to the same thing, simp closes by rfl ✓ since simp tries rfl at the end). Actually — after clearing denominators, LHS: s^n − (s−1)^n, RHS: s^n − (s−1)^n — identical ⟹ simp closes by rfl ✓. I'll leave field_simp alone; compile will tell.\n\nHmm — s^n/(s−1)^n − 1 clearing: multiply by (s−1)^n: (s^n − 1·(s−1)^n) = s^n − (s−1)^n ✓ same ✓ closes.\n\nFull Jlag_mul_pow:\n```lean\nlemma Jlag_mul_pow {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :\n    (s - 1) ^ (n + 1) * Jlag n s = Ffun n s := by\n  have h1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs1\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    have h2 : (s - 1) ^ n ≠ 0 := pow_ne_zero n h1\n    show (s / (s - 1)) ^ n - 1 = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n\n    rw [div_pow]\n    field_simp [h2]\n  show (s - 1) ^ (n + 1) * (kFun n s * (-(deriv riemannZeta s / riemannZeta s))) =\n    (s ^ n - (s - 1) ^ n) * hLi s\n  rw [hk, hLi_eq_of_ne hs1 hs0, pow_succ]\n  have h2 : (s - 1) ^ n ≠ 0 := pow_ne_zero n h1\n  field_simp [h2, hs0]\n  ring\n```\nAfter rw: goal ((s−1)^n·(s−1))·(((s^n−(s−1)^n)/(s−1)^n)·(−(ζ' s/ζ s))) = (s^n−(s−1)^n)·((s−1)·(−(ζ' s/ζ s))). field_simp [h2, hs0]: clears /(s−1)^n and /ζ s: both sides × (s−1)^n·ζ s... then ring ✓. Let me double check: LHS: (s−1)^n·(s−1)·(s^n−(s−1)^n)·(−ζ' s)/((s−1)^n·ζ s) → cleared: (s−1)^n·(s−1)·(s^n−(s−1)^n)·(−ζ' s) ; RHS cleared: (s^n−(s−1)^n)·(s−1)·(−ζ' s)·(s−1)^n. Equal ✓ ring. ✓\n\nWait — pow_succ : a^(n+1) = a^n·a ✓ rewrites (s−1)^{n+1} → (s−1)^n·(s−1) ✓.\n\nThe `show` for the main goal: unfolds Jlag n s and Ffun n s by defeq ✓.\n\nNow Rfun_eq_sub_div_near_one:\n```lean\nlemma Rfun_eq_sub_div_near_one (n : ℕ) :\n    ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = (Ffun n s - TaylP n s) / (s - 1) ^ (n + 1) := by\n  have hne : ∀ᶠ s in 𝓝[≠] (1 : ℂ), riemannZeta s ≠ 0 := by\n    have h := riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)\n    filter_upwards [h] with w hw\n    have h2 := hw\n    simp only [ne_eq, mul_eq_zero] at h2\n    push Not at h2\n    exact h2.2\n  filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs1\n  have hs1' : s ≠ 1 := hs1\n  have h1 : (s - 1) ^ (n + 1) ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hs1')\n  have e : (s - 1) ^ (n + 1) * Rfun n s = Ffun n s - TaylP n s := by\n    have e1 := Jlag_mul_pow hs1' hs0\n    have e2 := ppart_mul_pow hs1'\n    show (s - 1) ^ (n + 1) * (Jlag n s - ppart n s) = Ffun n s - TaylP n s\n    rw [mul_sub, e1, e2]\n  exact eq_div_of_mul_eq h1 (by rw [mul_comm]; exact e)\n```\n- hne mirrors hLi_eq_near_one's first have ✓ (LiResidue lines 131-132: riemannZeta_residue_one.eventually_ne (show (1:ℂ) ≠ 0 by norm_num) — gives ∀ᶠ w in 𝓝[≠] 1, (w−1)·ζ w ≠ 0 ✓).\n- `hs1'` from hs1: hs1 : s ∈ {1}ᶜ — `have hs1' : s ≠ 1 := hs1` — defeq ✓ (LiResidue used hw1 directly as w ≠ 1 ✓).\n- The `show` in e: Rfun n s defeq Jlag n s − ppart n s (delta+Pi.sub_apply) ✓.\n- eq_div_of_mul_eq h1 : a·c = b → a = b/c — hmm signature check from LiPrincipal line 129: eq_div_of_mul_eq Complex.I_ne_zero (by rw [mul_comm]; exact h6) where goal was ∫ = X / I and h6 : I * ∫ = X — so eq_div_of_mul_eq (hc : c ≠ 0) (h : c * a = b) : a = b / c — the mul_comm usage: h6 : I * ∫ = X, and after rw [mul_comm] : ∫ * I = X — wait then eq_div_of_mul_eq takes a*c = b form: (hc) (h : a * c = b) : a = b / c. In LiPrincipal: goal ∫ = X/I, h6 : I * ∫ = X, rw [mul_comm] at...? they wrote (by rw [mul_comm]; exact h6): the anonymous goal: ?a * ?c = ?b — unify a := ∫, c := I, b := X: rw [mul_comm] : I * ∫ = X... wait mul_comm rewrites ?a*?c to ?c*?a i.e. goal becomes I * ∫ = X? no: mul_comm : a*b = b*a — rw [mul_comm] rewrites the goal's `∫ * I = X` LHS to `I * ∫ = X`?? no — rw [mul_comm] rewrites the first ?*? pattern: ∫ * I → I * ∫ giving goal I * ∫ = X, closed by exact h6 ✓. So eq_div_of_mul_eq (hc : c ≠ 0) (h : a * c = b) : a = b / c ✓.\n  My usage: goal Rfun n s = (Ffun n s − TaylP n s)/(s−1)^{n+1}: a := Rfun n s, c := (s−1)^{n+1}, b := Ffun−TaylP. Need a*c = b: Rfun n s·(s−1)^{n+1} = Ffun − TaylP — I have e : (s−1)^{n+1}·Rfun n s = ... (c·a form) — so (by rw [mul_comm]; exact e): goal Rfun n s·(s−1)^{n+1} = Ffun − TaylP — rw [mul_comm] → (s−1)^{n+1}·Rfun n s = ... ✓ exact e ✓. \n\nRfun_tendsto_one — full:\n```lean\nlemma Rfun_tendsto_one (n : ℕ) :\n    ∃ L : ℂ, Tendsto (Rfun n) (𝓝[≠] (1 : ℂ)) (𝓝 L) := by\n  have hgan : AnalyticAt ℂ (Ffun n - TaylP n) 1 :=\n    (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1)\n  have hord : ((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1 :=\n    Ffun_sub_TaylP_order n\n  by_cases htop : analyticOrderAt (Ffun n - TaylP n) 1 = ⊤\n  · refine ⟨0, ?_⟩\n    have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), (Ffun n - TaylP n) s = 0 := analyticOrderAt_eq_top.mp htop\n    have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = 0 := by\n      filter_upwards [Rfun_eq_sub_div_near_one n, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n      have hg0' : Ffun n s - TaylP n s = 0 := hg0\n      rw [hs, hg0']\n      exact zero_div _\n    exact tendsto_const_nhds.congr' hev.symm\n  · obtain ⟨h, hh, hh0, hfh⟩ := hgan.analyticOrderAt_ne_top.mp htop\n    have hnm : n + 1 ≤ analyticOrderNatAt (Ffun n - TaylP n) 1 := by\n      rw [← Nat.cast_analyticOrderNatAt htop] at hord\n      exact ENat.natCast_le_natCast.mp hord\n    have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ),\n        Rfun n s = (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s := by\n      filter_upwards [Rfun_eq_sub_div_near_one n,\n        mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1\n      have hs1' : s ≠ 1 := hs1\n      have hs1n : s - 1 ≠ 0 := sub_ne_zero.mpr hs1'\n      rw [hs]\n      have hgs : (Ffun n - TaylP n) s =\n          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := by\n        have h2 := hgf.self_of_nhds\n        rwa [smul_eq_mul] at h2\n      have hgs' : Ffun n s - TaylP n s =\n          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := hgs\n      rw [hgs']\n      have e : (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 =\n          (s - 1) ^ (n + 1) *\n            (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) := by\n        rw [← pow_add]\n        congr 1\n        omega\n      rw [e, mul_assoc, mul_div_cancel_left₀ (pow_ne_zero (n + 1) hs1n)]\n    refine ⟨(1 - 1 : ℂ) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h 1, ?_⟩\n    have hcont : ContinuousAt\n        (fun s : ℂ => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) 1 :=\n      ((continuousAt_id.sub continuousAt_const).pow _).mul hh.continuousAt\n    exact (hcont.tendsto.mono_left nhdsWithin_le_nhds).congr' hev.symm\n```\nConcerns:\n- hg0' : Ffun n s − TaylP n s = 0 from hg0 : (Ffun n − TaylP n) s = 0 — defeq (Pi.sub_apply) ✓ exact-assign.\n- hgs' from hgs — defeq again (Pi.sub_apply direction) ✓.\n- After rw [hs]: goal (Ffun n s − TaylP n s)/(s−1)^{n+1} = (s−1)^{m−(n+1)}·h s. rw [hgs'] rewrites Ffun n s − TaylP n s → (s−1)^m·h s ✓. Then rw [e]: (s−1)^m → (s−1)^{n+1}·(s−1)^{m−(n+1)}: expression becomes ((s−1)^{n+1}·(s−1)^{m−n−1})·h s/(s−1)^{n+1}; mul_assoc: (s−1)^{n+1}·((s−1)^{m−n−1}·h s)/(s−1)^{n+1}; mul_div_cancel_left₀ (pow_ne_zero ...) : (s−1)^{m−n−1}·h s ✓ goal closed by rw's trailing rfl ✓.\n\n  mul_div_cancel_left₀ signature: `mul_div_cancel_left₀ (ha : a ≠ 0) : a * b / a = b` ✓ I believe exists (GroupWithZero cancels). Name check: there's `mul_div_cancel_left₀ : a ≠ 0 → a * b / a = b` ✓ (Mathlib, Algebra/GroupWithZero/Basic or Field). Fallback: field_simp+ring.\n\n- e's omega needs hnm in context ✓ (it is — same tactic block, hnm defined before hev ✓). Wait — e's proof is inside the filter_upwards lambda; hnm is in the enclosing context ✓ visible.\n\n- The ⊤ case's Tendsto.congr' — direction: tendsto_const_nhds : Tendsto (fun _ => (0:ℂ)) (𝓝[≠] 1) (𝓝 0); hev : ∀ᶠ s, Rfun n s = 0 — as EventuallyEq: Rfun n =ᶠ (fun _ => 0)? hev's RHS is `0` — the constant zero VALUE; as an EventuallyEq between functions: Rfun n =ᶠ[𝓝[≠] 1] (fun _ => 0)?? hev : ∀ᶠ s, Rfun n s = 0 — the \"0\" is (0:ℂ) — EventuallyEq f g l := ∀ᶠ x, f x = g x — unifying g x with 0: g := fun _ => 0 ✓. tendsto_const_nhds.congr' — signature Tendsto.congr' (hl : f₁ =ᶠ[l] f₂) (h : Tendsto f₁ l l₂) : Tendsto f₂ l l₂ — I need f₂ := Rfun n, f₁ := fun _ => 0: hl : (fun _ => 0) =ᶠ Rfun n := hev.symm ✓ h := tendsto_const_nhds ✓. So `tendsto_const_nhds.congr' hev.symm` ✓ (method dot on the Tendsto term: tendsto_const_nhds.congr' — hmm the dot notation: Tendsto.congr' — first explicit arg is hl, the Tendsto comes second — dot notation on tendsto_const_nhds puts it as the first Tendsto-typed explicit arg — Tendsto.congr' (hl) (h : Tendsto ...) — the first explicit arg hl is EventuallyEq, not Tendsto — dot notation inserts at the first matching-type position ✓ (Lean 4 inserts the dot-term at the first explicit arg of matching namespace-type — Tendsto.congr' has hl : EventuallyEq (not Tendsto) then h : Tendsto — dot inserts at h ✓ works).\n\n- Similarly (hcont.tendsto.mono_left nhdsWithin_le_nhds).congr' hev.symm ✓.\n\nOne concern: `mem_nhdsWithin_of_mem_nhds h0` — h0 : ∀ᶠ s in 𝓝 1, ... — gives ∀ᶠ s in 𝓝[≠] 1, ... ✓.\n\n`hgf.self_of_nhds`: hgf : (Ffun n − TaylP n) =ᶠ[𝓝 s] fun z => (z−1)^m • h z — self_of_nhds : (Ffun n − TaylP n) s = (s−1)^m • h s ✓.\n\n`hfh.eventually_nhds` ✓.\n\nEverything checks. §5's full residue lemma assembled earlier. The main theorem assembled earlier.\n\nAlso — I realize I should double-check `analyticOrderAt_eq_top` — line 75: `lemma analyticOrderAt_eq_top : analyticOrderAt f z₀ = ⊤ ↔ ∀ᶠ z in 𝓝 z₀, f z = 0` ✓ .mp ✓.\n\nAlso `Nat.cast_analyticOrderNatAt` — it's `@[simp] lemma Nat.cast_analyticOrderNatAt (hf : analyticOrderAt f z₀ ≠ ⊤) : ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀` (line 71) ✓.\n\nAnd `ENat.natCast_le_natCast : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m` (ENat Basic 393) ✓.\n\nNow — one more check on `Ffun_sub_TaylP_order` statement form: I want `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1`. The lemma natCast_le_analyticOrderAt_iff... : (n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0 — with n := n+1 the cast (n+1 : ℕ∞) — my statement's cast: `((n + 1 : ℕ) : ℕ∞)` — the lemma's is `((?n : ℕ) : ℕ∞)` — hmm actually the lemma statement at Order.lean:333: `lemma natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero ... (hf : AnalyticAt 𝕜 f z₀) : n ≤ analyticOrderAt f z₀ ↔ ...` — with n : ℕ and an invisible cast (the ≤ on ℕ∞ forces the cast). So its LHS is `↑n ≤ analyticOrderAt f z₀`. My goal `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1` — the rewrite `rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero hgan]` — pattern ↑(n+1) matches ↑?n with ?n := n+1 ✓.\n\nThe `show` form in my theorem statement: write `(n + 1 : ℕ∞)` vs `((n + 1 : ℕ) : ℕ∞)` — to guarantee the rewrite matches, state it as `((n + 1 : ℕ) : ℕ∞) ≤ ...` — hmm, `(n + 1 : ℕ∞)` elaborates n+1 IN ℕ∞ (HAdd ℕ∞) giving Nat.cast n + 1 — NOT the Nat.cast (n+1) form — rewrite would fail to match ↑?n! So write the statement carefully with the explicit ℕ cast: `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1` — elaborates n+1 at ℕ (HAdd ℕ ✓) then casts ✓ matches the lemma ✓.\n\nAfter rw: goal ∀ i < n + 1, iteratedDeriv i (Ffun n - TaylP n) 1 = 0 — hmm — the lemma's RHS: ∀ i < n, iteratedDeriv i f z₀ = 0 with n := n+1: ∀ i < n+1, iteratedDeriv i (Ffun n − TaylP n) 1 = 0 — the function: hgan : AnalyticAt ℂ (Ffun n − TaylP n) 1 — the Pi.sub form (Ffun n − TaylP n) ✓ my goal has (Ffun n − TaylP n) ✓ match.\n\nThen `intro i hi; exact Ffun_sub_TaylP_iteratedDeriv n i (Nat.lt_succ_iff.mp hi)` — wait Ffun_sub_TaylP_iteratedDeriv's conclusion: iteratedDeriv i (Ffun n - TaylP n) 1 = 0 ✓.\n\nAnd Ffun_sub_TaylP_iteratedDeriv (n i : ℕ) (hi : i ≤ n) : iteratedDeriv i (Ffun n - TaylP n) 1 = 0:\n```lean\n  have hF : ContDiffAt ℂ i (Ffun n) 1 := (Ffun_analyticAt_one n).contDiffAt\n  have hT : ContDiffAt ℂ i (TaylP n) 1 := (TaylP_analyticAt n 1).contDiffAt\n  rw [iteratedDeriv_sub hF hT, iteratedDeriv_TaylP hi, sub_self]\n```\niteratedDeriv_sub : ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → iteratedDeriv n (f − g) x = iteratedDeriv n f x − iteratedDeriv n g x ✓ (A_iter used ✓). Hmm — A_iter used `iteratedDeriv_sub hf hg` where the function was (fun..) − (fun..) — here Ffun n − TaylP n is Pi.sub of defs ✓ matches f − g with f := Ffun n ✓.\nAnalyticAt.contDiffAt : AnalyticAt ℂ f x → ContDiffAt ℂ ↑n? — LiResidue line 199-200: `have hh : ContDiffAt ℂ n hLi 1 := hLi_analyticAt_one.contDiffAt` — n : ℕ, coerced — so .contDiffAt gives ContDiffAt ℂ n for the ℕ n directly (there's a coercion n → ℕ∞ handled by unification? — AnalyticAt.contDiffAt : ContDiffAt 𝕜 ⊤? or ∀ (n : ℕ)... — LiResidue's usage proves it works with the target type ContDiffAt ℂ n hLi 1 given ✓ — the .contDiffAt must be polymorphic/order-inferred from the expected type ✓ same here).\n\nsub_self : a − a = 0 — after the two rewrites goal: iteratedDeriv i (Ffun n) 1 − iteratedDeriv i (Ffun n) 1 = 0 — rw [sub_self] closes? sub_self rewrites a−a → 0, leaving 0 = 0 closed by rw's rfl ✓.\n\nNow assemble everything and write the file. Length estimate: ~430 lines. Let me also prepare the exact file header doc.\n\nOne more consideration — `Rfun_residue_at` statement: I should double check the sign/value of the residue once more against D-064: \"simple poles at zeros with residue mult·(1−(ρ/(ρ−1))ⁿ)\". My A-formula: (zeroMult ρ : ℂ) * (1 - (ρ/(ρ-1))^n) ✓ matches STATE.md exactly.\n\nAlso for n = 0: 1 − (ρ/(ρ−1))⁰ = 1 − 1 = 0 ✓ fine.\n\nAlso — hO's Tendsto limit expression: I need hslope's deriv (kFun n) ρ — fine as is.\n\nNow — one more potential snag: in hexp, `filter_upwards [self_mem_nhdsWithin, ...]` — self_mem_nhdsWithin : s ∈ 𝓝[S] s? — self_mem_nhdsWithin : S ∈ 𝓝[S] a? The set here: 𝓝[≠] ρ = 𝓝[{ρ}ᶜ] ρ — self_mem_nhdsWithin : {ρ}ᶜ ∈ 𝓝[{ρ}ᶜ] ρ ✓ so filter_upwards gives hsρ : s ∈ {ρ}ᶜ — as s ≠ ρ: `sub_ne_zero.mpr hsρ` — needs s ≠ ρ: s ∈ {ρ}ᶜ defeq s ∉ {ρ} defeq (s = ρ → False) = (s ≠ ρ) ✓ defeq — sub_ne_zero.mpr hsρ should typecheck ✓ (as in LiResidue usages).\n\nAlso for `hh.continuousAt.eventually_ne hh0` — ContinuousAt.eventually_ne (h : ContinuousAt f x) (h0 : f x ≠ 0) : ∀ᶠ y in 𝓝 x, f y ≠ 0 ✓ LiResidue line 82 pattern ✓.\n\nOK, also the `Rfun_residue_at` — one more look at the overall structure:\n\n```lean\nlemma Rfun_residue_at (n : ℕ) {ρ : ℂ} (hρ : ρ ≠ 1) :\n    ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ))\n      =O[𝓝[≠] ρ] (1 : ℂ → ℂ) := by\n  have hρα : AnalyticAt ℂ riemannZeta ρ := analyticAt_riemannZeta hρ\n  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ)\n  have hkd : DifferentiableAt ℂ (kFun n) ρ := kFun_differentiableAt hρ\n  have hexp : ∀ᶠ s in 𝓝[≠] ρ,\n      (-(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))\n          - kFun n s * logDeriv h s - ppart n s)\n        = ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ)) s := by\n    filter_upwards [self_mem_nhdsWithin,\n      mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n      mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n      mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas\n    have hsρ' : s - ρ ≠ 0 := sub_ne_zero.mpr hsρ\n    have hld : logDeriv riemannZeta s =\n        (analyticOrderNatAt riemannZeta ρ : ℂ) / (s - ρ) + logDeriv h s := by\n      have e1 : logDeriv riemannZeta s =\n          logDeriv (fun z => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ * h z) s := by\n        simp only [logDeriv_apply, hfhs.deriv_eq, hfhs.self_of_nhds, smul_eq_mul]\n      rw [e1, logDeriv_mul (f := fun z : ℂ => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ)\n        (g := h) s (pow_ne_zero _ hsρ') hhs (by fun_prop) hhas.differentiableAt]\n      have e2 : logDeriv (fun z : ℂ => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ) s\n          = (analyticOrderNatAt riemannZeta ρ : ℂ) / (s - ρ) := by\n        rw [show (fun z : ℂ => (z - ρ) ^ analyticOrderNatAt riemannZeta ρ)\n            = (fun x : ℂ => x ^ analyticOrderNatAt riemannZeta ρ) ∘ (fun z => z - ρ) from rfl,\n          logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n        simp\n      rw [e2]\n    have hA : (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =\n        -(analyticOrderNatAt riemannZeta ρ : ℂ) * kFun n ρ := by\n      have hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl\n      rw [hmz]\n      show (analyticOrderNatAt riemannZeta ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =\n        -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((ρ / (ρ - 1)) ^ n - 1)\n      ring\n    simp only [Pi.sub_apply, Rfun, Jlag, hA]\n    rw [← logDeriv_apply, hld]\n    field_simp [hsρ']\n    ring\n  have hslope : Tendsto (fun s => (kFun n s - kFun n ρ) / (s - ρ)) (𝓝[≠] ρ)\n      (𝓝 (deriv (kFun n) ρ)) := by\n    have h2 := hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt\n    simpa only [slope_fun_def_field] using h2\n  have hcont1 : Tendsto (fun s => kFun n s * logDeriv h s) (𝓝[≠] ρ)\n      (𝓝 (kFun n ρ * logDeriv h ρ)) := by\n    have hc : ContinuousAt (fun s => kFun n s * (deriv h s / h s)) ρ :=\n      hkd.continuousAt.mul (hh.deriv.continuousAt.div hh.continuousAt hh0)\n    simpa only [logDeriv_apply] using hc.tendsto.mono_left nhdsWithin_le_nhds\n  have hcont2 : Tendsto (ppart n) (𝓝[≠] ρ) (𝓝 (ppart n ρ)) :=\n    (ppart_continuousAt hρ).tendsto.mono_left nhdsWithin_le_nhds\n  have hT : Tendsto\n      (fun s => -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))\n        - kFun n s * logDeriv h s - ppart n s)\n      (𝓝[≠] ρ)\n      (𝓝 (-(analyticOrderNatAt riemannZeta ρ : ℂ) * deriv (kFun n) ρ\n        - kFun n ρ * logDeriv h ρ - ppart n ρ)) :=\n    ((hslope.const_mul _).sub hcont1).sub hcont2\n  exact hT.isBigO_one ℂ |>.congr' hexp EventuallyEq.rfl\n```\nConcerns:\n- hA's `show`: kFun n ρ unfolds to (ρ/(ρ−1))^n − 1 by defeq ✓.\n- simp only [Pi.sub_apply, Rfun, Jlag, hA]: rewrites RHS; goal LHS untouched ✓. Hmm wait — after this simp, RHS = kFun n s * (−(deriv ζ s/ζ s)) − ppart n s − (−(m:ℂ)*kFun n ρ)/(s−ρ). But careful — simp only [hA] rewrites the pattern `(zeroMult ρ : ℂ) * (1 - (ρ/(ρ−1))^n)` — this appears inside RHS ✓. But ALSO — does the pattern `(zeroMult ρ : ℂ)` appear elsewhere? No ✓.\n- rw [← logDeriv_apply]: rewrites deriv riemannZeta s / riemannZeta s → logDeriv riemannZeta s ✓ — BUT does `deriv h s / h s` appear? No — LHS has logDeriv h s (already logDeriv form) ✓ unique occurrence ✓.\n- rw [hld] ✓.\n- field_simp [hsρ'] + ring ✓.\n- hT.isBigO_one ℂ : (fun s => ...) =O[𝓝[≠] ρ] 1 — `.congr' hexp EventuallyEq.rfl` — IsBigO.congr' (h : f =O[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f' =O[l] g' — with f := the big lambda, f' := ((Rfun n) − ...) — hexp : ∀ᶠ s, bigexpr = target s — as EventuallyEq: (fun s => bigexpr) =ᶠ target — hmm — hexp's statement: ∀ᶠ s, (bigexpr) = (target-lambda) s — for congr' I need f =ᶠ f' i.e. (fun s => bigexpr) =ᶠ ((Rfun n) − fun s => ...) — the ∀ᶠ statement's LHS is the raw expression bigexpr (with s free) — EventuallyEq f f' l unfolds to ∀ᶠ x, f x = f' x — with f := fun s => bigexpr: f s = bigexpr ✓ beta — defeq ✓. So hexp : (fun s => bigexpr) =ᶠ[𝓝[≠] ρ] ((Rfun n) − fun s => ...) — congr' hexp EventuallyEq.rfl : target =O 1 ✓ — vendored did exactly this ✓.\n\nWait — but vendored's hexp orientation: line 246-248: `(analyticOrderNatAt f q :ℂ)*((g s − g q)/(s−q)) + g s * logDeriv h s = ((fun s => g s * logDeriv f s) − fun s => A q/(s−q)) s` — bigexpr = target s ✓ same as mine ✓ and line 280: hO.congr' hexp EventuallyEq.rfl ✓.\n\n- `(hslope.const_mul _)` — Tendsto.const_mul (c : ℂ) (h : Tendsto f l (𝓝 c'))? signature: Filter.Tendsto.const_mul (b) (h : Tendsto f l (𝓝 c)) : Tendsto (fun k => b * f k) l (𝓝 (b * c)) ✓ — (hslope.const_mul (−(m:ℂ))) — hmm I wrote hslope.const_mul _ — the _ := −(m:ℂ) inferred from the .sub combination with the target... Actually the final hT's type is as stated; ((hslope.const_mul _).sub hcont1).sub hcont2 — the _ gets unified with −(analyticOrderNatAt...) from the expected type of hT ✓ (the have's type annotation guides elaboration ✓).\n\nHmm — the lambda produced by const_mul: fun s => C * ((kFun n s − kFun n ρ)/(s−ρ)) — my hT type's first term: −(m:ℂ) * ((kFun n s − kFun n ρ)/(s−ρ)) ✓ matches (C := −(m:ℂ)) ✓.\n\n- `.sub` : Tendsto.sub (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) : Tendsto (fun x => f x − g x) l (𝓝 (a − b)) ✓ — the resulting lambda fun s => C·(slope s) − kFun n s·logDeriv h s ✓ then .sub hcont2: fun s => (C·slope − k·logDeriv) − ppart n s — my hT type: −(m:ℂ)·(...) − kFun n s·logDeriv h s − ppart n s — parses as ((−(m)·... ) − k·logDeriv) − ppart ✓ left-assoc ✓ matches.\n\nAlso for hcont1 — the simpa only [logDeriv_apply] — rewrites logDeriv h s → deriv h s/h s in the GOAL (both in the lambda and the limit value ✓) then matches hc.tendsto... ✓. But careful — logDeriv_apply : logDeriv f a = deriv f a / f a — simp only [logDeriv_apply] on goal Tendsto (fun s => kFun n s * logDeriv h s) ... — rewrites logDeriv h s → deriv h s/h s ✓ goal becomes Tendsto (fun s => kFun n s * (deriv h s/h s)) (𝓝[≠] ρ) (𝓝 (kFun n ρ * (deriv h ρ/h ρ))) — and hc.tendsto.mono_left nhdsWithin_le_nhds : Tendsto (fun s => kFun n s * (deriv h s/h s)) (𝓝[≠] ρ) (𝓝 ((fun s => kFun n s * (deriv h s/h s)) ρ)) — beta: kFun n ρ * (deriv h ρ/h ρ) ✓ matches ✓.\n\nNow §4's remaining piece — TaylP_analyticAt — wrote with Finset induction. hterm : ∀ j, AnalyticAt ℂ (fun w => (iteratedDeriv j (Ffun n) 1 / j !) * (w−1)^j) w := fun j => analyticAt_const.mul ((analyticAt_id.sub analyticAt_const).pow j) — analyticAt_const : AnalyticAt ℂ (fun _ => c) x ✓; .mul : AnalyticAt ℂ ((fun _ => c) * (fun w => (w−1)^j)) x — Pi.mul — vs (fun w => c * (w−1)^j) — defeq ✓.\n\nempty case: AnalyticAt ℂ (fun w => ∑ j ∈ (∅ : Finset ℕ), ...) w — after simp [Finset.sum_empty]: fun w => 0 — hmm — simp_rw [Finset.sum_empty] turns the lambda into fun w => 0? Finset.sum_empty : ∑ i ∈ ∅, f i = 0 ✓ simp_rw inside the lambda binder ✓ then analyticAt_const : AnalyticAt ℂ (fun _ => 0) w ✓ `simpa using analyticAt_const`? Let me write:\n```lean\n    | empty =>\n      simp only [Finset.sum_empty]\n      exact analyticAt_const\n```\nafter simp only [Finset.sum_empty]: goal AnalyticAt ℂ (fun w => 0) w — analyticAt_const : AnalyticAt ℂ (fun _ => ?c) ?x ✓ exact ✓.\n\ninsert: goal AnalyticAt ℂ (fun w => ∑ j ∈ insert a t, term j w) w — simp_rw [Finset.sum_insert hat]: fun w => term a w + ∑ j ∈ t, term j w — (hterm a).add ht : AnalyticAt ℂ ((fun w => term a w) + (fun w => ∑ j ∈ t, ...)) w — Pi.add vs lambda-with-+ — defeq ✓ exact might work; else convert. I'll write `exact (hterm a).add ht` and fix if defeq fails.\n\nHmm — the term function in TaylP_analyticAt vs the ppart_continuousAt — note in the induction, the lambda family: fun w => ∑ j ∈ t, (iteratedDeriv j (Ffun n) 1 / j !) * (w − 1)^j — and TaylP n = fun w => ∑ j ∈ range(n+1), ... — `exact this (Finset.range (n+1))` — defeq with TaylP n ✓ (delta+beta) — AnalyticAt ℂ (TaylP n) w vs AnalyticAt ℂ (fun w => ∑...) w ✓.\n\nSame pattern for ppart_continuousAt (with ppart n, Icc 1 (n+1), Acoeff n i / (w−1)^i).\n\nOK — now also double-check `analyticAt_const` — used in LiResidue line 104-105: (analyticAt_id.sub analyticAt_const) ✓ exists.\n\n`continuousAt_id` / `continuousAt_const` ✓ standard.\n\n`(continuousAt_id.sub continuousAt_const).pow _` : ContinuousAt (fun w => (w−1))^k?? — ContinuousAt.pow : ContinuousAt f x → ContinuousAt (f^n) x — (fun w => w−1)^k vs fun w => (w−1)^k — defeq Pi.pow ✓. Then .mul hh.continuousAt ✓.\n\nNow — think about the `rectangle_mem_nhds_of_mem_not_border` lemma's obtain: hmem : p ∈ Rectangle z w — Rectangle is a def (reProdIm of uIcc) — obtain ⟨h1, h2⟩ := hmem — membership in reProdIm: p ∈ s ×ℂ t ↔ p.re ∈ s ∧ p.im ∈ t — defeq ✓ obtain works (vendored did obtain ⟨h1, h2⟩ := hρR directly ✓).\n\nThe simpa [uIcc_of_le hre] using h1: h1 : p.re ∈ [[z.re, w.re]] = uIcc — with hre : z.re ≤ w.re: uIcc_of_le hre : [[z.re,w.re]] = Icc z.re w.re — simpa [uIcc_of_le hre] using h1 : z.re ≤ p.re ∧ p.re ≤ w.re (mem_Icc) ✓ vendored line 189 verbatim ✓.\n\nOK — also need `open Set` for mem_union/mem_reProdIm in the simp only? The vendored file had `open Complex Set Topology Filter Asymptotics Real`. LiPrincipal has `open Zeta23 Complex Filter Topology` — and used mem-reProdIm-style lemmas? LiPrincipal used RectangleBorder membership via mapsTo — not mem_reProdIm directly. For my helper I need: `mem_union` (Set), `mem_reProdIm` (Complex? — Complex.mem_reProdIm? it's used in vendored with open Complex — could be Complex.mem_reProdIm or Set-like. Since I open Complex, bare mem_reProdIm should resolve (Complex namespace has mem_reProdIm? reProdIm is Complex.reProdIm; mem_reProdIm : p ∈ s ×ℂ t ↔ p.re ∈ s ∧ p.im ∈ t — in Complex namespace ✓). `mem_singleton_iff` (Set/root?) — root-level Set.mem_singleton_iff — accessible bare with... it's Set.mem_singleton_iff — vendored used bare with open Set. I'll add `open Set` — wait, conflict risk: Set has `mem_union`, `mem_singleton_iff` — root aliases exist for some. To be safe: use `open Set` in my file? LiResidue/LiPrincipal didn't. Adding open Set could cause ambiguity with Complex/Filter names? Hmm — `Set.Iic` etc no clash. But there might be clashes like Set.mem_nhds... Let me just qualify: Set.mem_union? Actually `mem_union` IS Set.mem_union with open Set... — root `mem_union` doesn't exist without open. I'll write the simp only with qualified names: `simp only [RectangleBorder, Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff, not_or] at hb` — hmm mem_reProdIm: check namespace: vendored used bare `mem_reProdIm` with `open Complex Set ...` — could be Complex.mem_reProdIm OR Set.mem_reProdIm? reProdIm ×ℂ is Complex.reProdIm — the membership lemma: `Complex.mem_reProdIm : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t`? Let me check quickly.","signature":""},{"type":"text","text":"Root file needs the new import added. Let me check two remaining name namespaces, then write."},{"type":"tool_use","id":"Bash_30","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem mem_reProdIm\\|lemma mem_reProdIm\" Mathlib/Data/Complex/ | head -3; grep -rn \"uIoo_of_le\\|theorem uIcc_of_le\" Mathlib/Order/Interval/Set/UnionIcc.lean Mathlib/Order/Interval/Set/Basic.lean 2>/dev/null | head -4","description":"Check mem_reProdIm and uIcc/uIoo namespaces"},"extra_content":null}]