[{"type":"thinking","thinking":"Mathlib has `riemannZeta_neg_two_mul_nat_add_one : riemannZeta (-2 * (n + 1)) = 0` but I don't see deriv-nonvanishing at trivial zeros. Simplicity of trivial zeros is not readily available — defer it (note in file header). The generic theorem with `zeroMult ρ` covers it.\n\nNow write the file. Let me also double check a few remaining names:\n- `mem_of_mem_nhds` ✓ (used in vendored line 283).\n- `Set.Finite.mem_toFinset` ✓ (vendored line 380).\n- `ContinuousOn.rectangleBorder_integrable` ✓ (vendored line 129).\n- `residueTheorem_finset` ✓ (RectangleLogDeriv, namespace Zeta23.Analytic — with `open Zeta23` we get Analytic.residueTheorem_finset — need `open Zeta23.Analytic` or full path `Zeta23.Analytic.residueTheorem_finset`. LiPrincipal opens Zeta23 only and uses ResidueTheoremInRectangle (which is in Zeta23 directly?). Let me check where ResidueTheoremInRectangle lives — it's used in LiPrincipal with `open Zeta23 Complex Filter Topology`. residueTheorem_finset is in `Zeta23.Analytic` namespace — so reference as `Analytic.residueTheorem_finset` with open Zeta23, or `Zeta23.Analytic.residueTheorem_finset` fully qualified. I'll use the full path to be safe.\n- `finite_zeros_rectangle` is also in Zeta23.Analytic namespace ✓ same treatment.\n- `IsBigO.congr'` — check exact argument order from vendored usage: hO.congr' hexp EventuallyEq.rfl where hO : LHS =O 1 and hexp : ∀ᶠ s, LHS s = RHS s — so congr' (hf : f' =ᶠ f)? Hmm: if hO : f =O[l] g, then hO.congr' (hff' : f' =ᶠ[l] f)?? — but vendored's hexp has form `bigLHS = targetRHS s` i.e. ∀ᶠ s, f s = f' s i.e. f =ᶠ f'... Let me look at IsBigO.congr' actual signature: `theorem Asymptotics.IsBigO.congr' (h : f =O[l] g) (hf : f' =ᶠ[l] f) (hg : g' =ᶠ[l] g) : f' =O[l] g'`? If so, vendored's hexp : ∀ᶠ s, f s = f' s is f =ᶠ f' and passing it as hf : f' =ᶠ f would fail... unless EventuallyEq is symmetric-inferred? No. So congr' must be: (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') : f' =O[l] g'. Let me check: Mathlib `Asymptotics.IsBigO.congr' : f =O[l] g → f =ᶠ[l] f' → g =ᶠ[l] g' → f' =O[l] g'` — yes I believe that's the signature (congr' takes same-direction EventuallyEqs). Vendored: hO : bigterm =O 1; hexp : bigterm =ᶠ target; EventuallyEq.rfl : (1) =ᶠ (1) — gives target =O 1 ✓ consistent. So my hexp should be stated as `bigLHS-func =ᶠ target-func` i.e. ∀ᶠ s, bigLHS s = ((Rfun n) − residue-lambda) s ✓ as I planned.\n\n- `Tendsto.congr'` : f₁ =ᶠ[l] f₂ → Tendsto f₁ l l₂ → Tendsto f₂ l l₂ — so with hev : Rfun =ᶠ φ and hT : Tendsto φ: need φ =ᶠ Rfun i.e. hev.symm ✓ as planned.\n\n- For the \"slope\" lemma: hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt — vendored line 269: `hasDerivAt_iff_tendsto_slope.mp hga.differentiableAt.hasDerivAt` then `simpa only [slope_fun_def_field] using this` ✓ copy.\n\n- `logDeriv_apply` — vendored used `simp only [logDeriv_apply, ...]` ✓.\n\n- eventually_ne_nhds : used in LiResidue ✓ (eventually_ne_nhds : x ≠ y → ∀ᶠ z in 𝓝 x, z ≠ y).\n\n- `riemannZeta_residue_one.eventually_ne` ✓ (LiResidue line 132 pattern).\n\n- Nat.cast_analyticOrderNatAt : (hf : analyticOrderAt f z₀ ≠ ⊤) : ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀ ✓ (line 71, @[simp]).\n\n- ENat.natCast_le_natCast : (n : ℕ∞) ≤ (m : ℕ∞) ↔ n ≤ m ✓.\n\nFor hnm derivation:\nhord : ((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt g 1 — hmm, actually the goal of Ffun_sub_TaylP_order: I write it as `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1`. Then in Rfun_tendsto_one: rw [← Nat.cast_analyticOrderNatAt htop] at hord : ((n+1:ℕ):ℕ∞) ≤ ((analyticOrderNatAt g 1 : ℕ) : ℕ∞)... then ENat.natCast_le_natCast.mp hord : n+1 ≤ analyticOrderNatAt g 1 ✓. With m := analyticOrderNatAt g 1 — set BEFORE this rewrite so hord mentions m. Careful: `set m := analyticOrderNatAt g 1 with hm` — rewrites occurrences in hord only if hord is after set (local context order) — set folds all hypotheses' occurrences? `set` folds in goal and... by default only goal; use `set ... with hm` — it folds in the goal only unless including hypotheses... Actually `set x := e` introduces x and replaces e EVERYWHERE in goal and context? Documentation: \"set a := b\" introduces a local definition and replaces occurrences in the goal; to also replace in hypotheses use ... hmm, `set` does fold in all hypotheses I believe (it abstracts all occurrences). Let me just avoid set for m and use `analyticOrderNatAt g 1` explicitly, or use `obtain` first then `set`. Simpler: don't use set; write analyticOrderNatAt g 1 explicitly (it's short enough) — hfh's factorization has exponent analyticOrderNatAt g 1 automatically. OK.\n\nOne more subtlety — in the hexp identity: hfh.eventually_nhds : ∀ᶠ s in 𝓝 ρ, riemannZeta =ᶠ[𝓝 s] (fun z => (z − ρ)^analyticOrderNatAt riemannZeta ρ • h z) — wait hfh : riemannZeta =ᶠ[𝓝 ρ] fun z => (z − ρ)^analyticOrderNatAt riemannZeta ρ • h z (note: the factorization from hρα.analyticOrderAt_ne_top.mp has exponent analyticOrderNatAt RIEMANNZETA ρ — but I need exponent m := analyticOrderNatAt g... NO WAIT. In §5 (residue at ρ) the factorization is of ζ at ρ — exponent analyticOrderNatAt ζ ρ — and zeroMult ρ = analyticOrderNatAt ζ ρ defeq (zeroMult := (analyticOrderAt ζ ρ).toNat, analyticOrderNatAt ζ ρ := (analyticOrderAt ζ ρ).toNat — same ✓). So (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) by rfl ✓.\n\nIn §4's m-case the factorization is of g := Ffun − TaylP at 1 — exponent analyticOrderNatAt g 1 ✓ separate.\n\nOK also `hfh.eventually_nhds` — EventuallyEq.eventually_nhds : f =ᶠ[𝓝 x] g → ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g ✓ vendored used (line 242-243: h2 := hfh.eventually_nhds) ✓.\n\nAlso in §5 hexp, I need `hfs.self_of_nhds` and `hfs.deriv_eq` (vendored line 237-239, 254-256 ✓).\n\nOne more potential issue: in hexp, after `simp only [Pi.sub_apply, Rfun, Jlag, hA]` — Rfun and Jlag are defs; simp only with def names unfolds via equation lemmas — for `Rfun n s`: Rfun n = Jlag n − ppart n, so Rfun n s needs Pi.sub_apply AFTER unfolding Rfun: simp only [Rfun] gives (Jlag n − ppart n) s, then Pi.sub_apply gives Jlag n s − ppart n s, then simp only [Jlag] gives kFun n s * (−(deriv...)) − ppart n s. Order in the simp only list doesn't matter (fixpoint) ✓.\n\nAnd hA rewrite: A-side. Let me restructure hexp's final algebra explicitly:\n\nGoal: (−(m:ℂ)·((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s·logDeriv h s − ppart n s) = (Rfun n − fun s => ((zeroMult ρ:ℂ)·(1−(ρ/(ρ−1))^n))/(s−ρ)) s\n\nRHS unfolds: Jlag n s − ppart n s − ((zeroMult ρ:ℂ)·(1−(ρ/(ρ−1))^n))/(s−ρ)\n= kFun n s·(−(deriv ζ s/ζ s)) − ppart n s − (−(m:ℂ)·kFun n ρ)/(s−ρ)   [by hA]\n= kFun n s·(−logDeriv ζ s) − ppart n s + (m:ℂ)·kFun n ρ/(s−ρ)   [logDeriv_apply]\n= kFun n s·(−((m:ℂ)/(s−ρ) + logDeriv h s)) − ppart n s + (m:ℂ)·kFun n ρ/(s−ρ)   [hld]\n= −(m:ℂ)·kFun n s/(s−ρ) − kFun n s·logDeriv h s − ppart n s + (m:ℂ)·kFun n ρ/(s−ρ)\n= −(m:ℂ)·(kFun n s − kFun n ρ)/(s−ρ) − kFun n s·logDeriv h s − ppart n s ✓ = LHS.\n\nLean: \n```lean\n    simp only [Pi.sub_apply, Rfun, Jlag, hA, logDeriv_apply, hld]\n    field_simp [hsρ']\n    ring\n```\nHmm — logDeriv_apply rewrites `logDeriv ?f ?a` to `deriv ?f a / ?f a` — WRONG DIRECTION (I want deriv/· → logDeriv for ζ, but hld is about logDeriv ζ). After simp only [Jlag]: kFun n s * (-(deriv ζ s / ζ s)). I want to rewrite deriv ζ s/ζ s = logDeriv ζ s to apply hld. logDeriv_apply : logDeriv f a = deriv f a / f a. simp only [logDeriv_apply] rewrites logDeriv ζ s → deriv ζ s/ζ s — but at that point there's no logDeriv ζ s yet (Jlag has the deriv form). Instead: rw [← logDeriv_apply] — turns deriv ζ s/ζ s into logDeriv ζ s ✓ then rw [hld]. But careful — logDeriv h s also appears on LHS; ← logDeriv_apply would rewrite the FIRST occurrence of deriv ? / ? — which is deriv ζ s/ζ s (only occurrence on RHS; LHS has logDeriv h — not deriv form) ✓ OK.\n\nPlan:\n```lean\n    simp only [Pi.sub_apply, Rfun, Jlag, hA]\n    rw [← logDeriv_apply, hld]\n    field_simp [hsρ']\n    ring\n```\nAfter rw [hld]: RHS = kFun n s * (-((m:ℂ)/(s−ρ) + logDeriv h s)) − ppart n s − (−(m:ℂ)*kFun n ρ)/(s−ρ). LHS = −(m:ℂ)*((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s*logDeriv h s − ppart n s. field_simp [hsρ'] clears /(s−ρ) everywhere; ring closes ✓.\n\nhA : ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) = -(m : ℂ) * kFun n ρ:\n- (zeroMult ρ : ℂ) = (m : ℂ): m := analyticOrderNatAt ζ ρ (via `set m := ... with hm` — then hm : m = analyticOrderNatAt ζ ρ; zeroMult ρ defeq analyticOrderNatAt ζ ρ: `have hmz : (zeroMult ρ : ℂ) = (m : ℂ) := by rw [hm]` — hm : m = analyticOrderNatAt ζ ρ — rw [hm] turns (m:ℂ) into (analyticOrderNatAt ζ ρ : ℂ) — then goal (zeroMult ρ:ℂ) = (analyticOrderNatAt ζ ρ : ℂ) — defeq rfl; `exact rfl` might fail if casts differ... both are Nat.cast of defeq nats — rfl should work (defeq). Or `by simp [zeroMult, analyticOrderNatAt, hm]`... Let me write: have hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl — if rfl fails, `by unfold zeroMult analyticOrderNatAt; rfl` or norm_cast. Then rw [hmz].\n- kFun n ρ = (ρ/(ρ−1))^n − 1 — unfold kFun ✓.\n- goal: (m:ℂ)·(1 − (ρ/(ρ−1))^n) = −(m:ℂ)·((ρ/(ρ−1))^n − 1) — ring ✓.\n\nWait — set m := analyticOrderNatAt riemannZeta ρ — the obtain ⟨h, hh, hh0, hfh⟩ comes BEFORE set; hfh's exponent is analyticOrderNatAt riemannZeta ρ — set folds it in hfh too (set folds context? In Lean4 Mathlib, `set x := e` replaces e in the goal AND all hypotheses? — docs: \"set t := e ... assigns the value ... and replaces all occurrences of e in the goal and context\"? I believe `set` does fold hypotheses too by default in Lean 4 (it's `set ... at ...`? no — `set` introduces the definition everywhere; actually in Lean4 core, `set` only affects the goal unless you include locations... Mathlib's `set` tactic: `set a := e with h` — replaces in goal and all hypotheses? Let me recall: Lean4 `set` docstring: \"set x := e\" — \"The tactic set x := e introduces a new local definition x := e and replaces all occurrences of e by x in the goal and all hypotheses.\" I think it does replace everywhere. Either way it works — if it doesn't fold hfh, the exponent stays analyticOrderNatAt ζ ρ which is defeq to m — rewrites might need care. To minimize risk: DON'T set m; just use analyticOrderNatAt riemannZeta ρ directly. It's verbose but safe. Actually verbosity in a few places is fine.\n\nHmm, actually in §5 I use m in several places ((m:ℂ)/(s−ρ) etc. — from e2's simp output: logDeriv (x^m)... the e2 result: logDeriv (fun z => (z−ρ)^m...) — the exponent from hfh is analyticOrderNatAt ζ ρ. So the algebra naturally carries analyticOrderNatAt ζ ρ. And the A-value has zeroMult ρ. Bridge via hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl. Fine — no set, write it out.\n\nNow — the ordering of the file and the `open` requirements:\n- `open Zeta23 Complex Filter Topology` (as LiPrincipal/LiResidue).\n- `open scoped Nat` for n! notation? LiResidue needed `open scoped Nat` for factorial. My file uses j ! — include it.\n- Residue theorem: Zeta23.Analytic.residueTheorem_finset — full path or `open Zeta23.Analytic`. Wait — is there a name clash risk with open Zeta23.Analytic? Its contents: residueTheorem_finset, finite_zeros_rectangle, rectangleIntegral'_mul_logDeriv etc. No clashes with my names. But `open` also brings `Analytic.`... I'll use fully-qualified names (Zeta23.Analytic.residueTheorem_finset) — no open needed. With `open Zeta23`, can I write `Analytic.residueTheorem_finset`? Yes — namespace resolution finds Zeta23.Analytic. I'll use Analytic.residueTheorem_finset and Analytic.finite_zeros_rectangle... hmm — but only the corollary uses finite_zeros_rectangle, which I decided to skip. So only residueTheorem_finset needed. \n\nLet me also double-check `AnalyticAt.sum` existence... I'm not 100% sure. Alternative for TaylP analytic: each term analytic; finite sum: use `Finset.sum` induction:\n```lean\nlemma TaylP_analyticAt (n : ℕ) (w : ℂ) : AnalyticAt ℂ (TaylP n) w := by\n  have hterm : ∀ j : ℕ, AnalyticAt ℂ (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w :=\n    fun j => analyticAt_const.mul ((analyticAt_id.sub analyticAt_const).pow j)\n  have : ∀ t : Finset ℕ, AnalyticAt ℂ (fun w : ℂ => ∑ j ∈ t, (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w := by\n    intro t\n    induction t using Finset.induction with\n    | empty => simp; exact analyticAt_const  -- ∑ over empty = 0 function\n    | insert a t hat ht =>\n      simp_rw [Finset.sum_insert hat]\n      exact (hterm a).add ht\n  exact this _\n```\nThe empty case: (fun w => ∑ j ∈ ∅, ...) = fun w => 0 — simp [Finset.sum_empty] then analyticAt_const (0)... `analyticAt_const : AnalyticAt 𝕜 (fun _ => c) x`? There's `analyticAt_const` ✓ (used in LiResidue). The insert: sum_insert gives c_a·(w−1)^a + Σ_t — .add ✓.\n`exact this _` — defeq bridge ppart-style: TaylP n w unfolds to the sum ✓. AnalyticAt (TaylP n) w vs AnalyticAt (fun w => ∑ ...) w — TaylP is a def — exact uses defeq ✓.\n\nActually — check `AnalyticAt.sum`: grep quickly? I'll just include the induction version (reliable).\n\nFor AnalyticAt.mul: `AnalyticAt.mul (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f * g) x` ✓ used in LiResidue (line 104-105: (analyticAt_id.sub analyticAt_const).mul ...) ✓. And my term: (fun w => c * (w−1)^j) vs (fun _ => c) * (fun w => (w−1)^j) — Pi.mul defeq ✓.\n\nFor Ffun analytic: (analyticAt_id.pow n) : AnalyticAt ℂ (fun w => w)^n? analyticAt_id : AnalyticAt ℂ (fun w => w) 1? `analyticAt_id : AnalyticAt 𝕜 id x` — LiResidue line 88: (analyticAt_id.sub analyticAt_const) : AnalyticAt ℂ (fun w => w − 1) w ✓ so id vs lambda defeq works. (analyticAt_id.pow n) : AnalyticAt ℂ (id^n) — id^n vs (fun w => w^n): Pi.pow_apply defeq ✓. .sub : (fun w => w^n) − (fun w => (w−1)^n) = fun w => w^n − (w−1)^n ✓ Pi.sub defeq. .mul hLi_analyticAt_one ✓. Ffun n = fun w => (w^n − (w−1)^n) * hLi w ✓ defeq.\n\nNow the `iteratedDeriv_sum` signature: `lemma iteratedDeriv_sum (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) : iteratedDeriv n (fun x => ∑ i ∈ I, f i x) x = ∑ i ∈ I, iteratedDeriv n (f i) x`? — from IteratedDeriv/Lemmas.lean:509. The function form: probably `iteratedDeriv n (∑ i ∈ I, f i) x = ...`? Let me check its exact statement... I'll trust and adapt: apply with the sum-of-functions form; if the LHS is iteratedDeriv n (fun x => ∑ i, f i x) x, my TaylP unfolded via the funext-rw matches ✓.\n\nContDiffAt of each term: (contDiffAt_const).mul (((contDiff_id.sub contDiff_const).pow j).contDiffAt)... careful: ContDiffAt vs ContDiff: contDiff_id : ContDiff 𝕜 n id; .pow j : ContDiff (id^j)... then .contDiffAt : ContDiffAt ✓. LiResidue line 162-164: (contDiff_id.pow n).contDiffAt : ContDiffAt ℂ i (fun w => w^n) 1 — wait ContDiff at order i vs the pow n — ContDiff is for ALL orders up to ⊤? contDiff_id : ContDiff 𝕜 n id for the given n? contDiff_id : ContDiff 𝕜 n id ✓ polymorphic n. .contDiffAt instantiates ✓. So: ((contDiff_id.sub contDiff_const).pow j).contDiffAt : ContDiffAt ℂ i (fun w => (w−1))^j? hmm — ContDiffAt ℂ i (fun w => (w−1)^j) 1: the (id−const)^j vs fun w => (w−1)^j — defeq Pi ✓ (A_iter did this ✓). Then contDiffAt_const.mul : ContDiffAt ℂ i ((fun _ => c)·(fun w => (w−1)^j)) 1 ✓.\n\niteratedDeriv_const_mul (c) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (fun y => c * f y) x = c * iteratedDeriv n f x — my term: fun w => (iteratedDeriv j (Ffun n) 1 / j !) * (w − 1)^j — matches with c := that constant, f := fun w => (w−1)^j ✓.\n\nThe hderiv_pow term (from A_iter h2):\n```lean\n  have hdp : ∀ j : ℕ, iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) (1 : ℂ) =\n      (j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i) := by\n    intro j\n    have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ j) (1 : ℂ)) 1\n    rw [iteratedDeriv_pow] at e\n    simpa using e\n```\n(A_iter line 172-175 ✓ — there the cast (n.descFactorial i : ℂ) appeared via simp — in A_iter the statement had `n.descFactorial i * (0 : ℂ) ^ (n - i)` with the cast handled by simp: iteratedDeriv_pow gives (j.descFactorial i : ℂ)·x^{j−i}? iteratedDeriv_pow : iteratedDeriv i (fun x => x^n) x = (n.descFactorial i : 𝕜)·x^{n−i} ✓ cast built in. And e after congr_fun: iteratedDeriv i ((fun w => w^j) ∘ (fun w => w − 1)) 1 = ... hmm iteratedDeriv_comp_sub_const i f c : iteratedDeriv i (f ∘ (· − c)) = fun x => iteratedDeriv i f (x − c)? From A_iter usage: congr_fun ... 1 then rw iteratedDeriv_pow at e then simpa using e proves `iteratedDeriv i (fun w => (w−1)^n) 1 = n.descFactorial i * (0:ℂ)^{n−i}` ✓ copy.)\n\nThen the single-term evaluation:\n```lean\n  -- Σ_j c_j * (descFactorial j i * 0^{j−i}) = c_i * i!\n  rw [Finset.sum_eq_single i]\n  · -- term i\n    rw [Nat.descFactorial_self, Nat.sub_self... ] \n```\nterm i: (iteratedDeriv i (Ffun n) 1 / i !) * ((i.descFactorial i : ℂ) * (0:ℂ)^(i−i)):\nNat.descFactorial_self : n.descFactorial n = n ! ✓ (used in A_iter line 184: simp [Nat.descFactorial_self]). i−i = 0, 0⁰ = 1. So term = c_i·((i !:ℂ)·1) = iteratedDeriv i Ffun 1/i!·i! = iteratedDeriv i Ffun 1. field_simp or: (a/b)·b = a with b = (i!:ℂ) ≠ 0: `div_mul_cancel₀` — name check: `div_mul_cancel₀ (h : b ≠ 0) : a / b * b = a`? In recent Mathlib: `div_mul_cancel₀ : b ≠ 0 → a / b * b = a` ✓ (field version). The cast (i ! : ℂ) ≠ 0: Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero i) ✓.\n\nWait — the multiplication order: c_i * ((i!:ℂ) * 1) = c_i * i! — need (c_i) * (i!) = iteratedDeriv i Ffun 1: c_i = D/i! so D/i! * i! = D ✓ div_mul_cancel₀. But the term is c_j * (descFactorial...) — after rewrites: (D/i!) * ((i!:ℂ) * 1) — reassociate: ring_nf? Let me do: rw [Nat.descFactorial_self]; simp; then field_simp [Nat.factorial_ne_zero]... Let me write:\n```lean\n  · have hfi : ((i ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero i)\n    rw [Nat.descFactorial_self]\n    simp only [Nat.sub_self, pow_zero, mul_one]  -- hmm Nat.sub_self is for ℕ: i − i = 0 ✓; (0:ℂ)^0 = 1 pow_zero ✓\n    -- goal: iteratedDeriv i (Ffun n) 1 / i ! * (i ! : ℂ) = iteratedDeriv i (Ffun n) 1\n    exact div_mul_cancel₀ _ hfi  -- signature check: div_mul_cancel₀ (a) (h : b ≠ 0) : a / b * b = a\n```\nHmm div_mul_cancel₀ argument order: `div_mul_cancel₀ (a : G₀) (h : b ≠ 0) : a / b * b = a`? or (h) first? There's `div_mul_cancel₀ : a / b * b = a` with b ≠ 0 as hypothesis — modern Mathlib: `theorem div_mul_cancel₀ (a : G₀) {b : G₀} (h : b ≠ 0) : a / b * b = a`. b implicit ✓. If unsure: `field_simp [hfi]` then nothing... Actually safest: `rw [div_mul_cancel_left₀?]...` ugh. Alternative: mul_comm then mul_div_cancel... Let me just use: have : (iteratedDeriv i (Ffun n) 1 / (i ! : ℂ)) * (i ! : ℂ) = iteratedDeriv i (Ffun n) 1 := by field_simp [hfi]. field_simp with hfi : (i!:ℂ) ≠ 0 closes a/b·b = a ✓ (field_simp proves equalities of field expressions; a/b*b — it normalizes to a·b = a·b ✓). \n\nCast subtlety: `i !` in Acoeff is `Nat.factorial (n+1−i)` cast to ℂ via the division... In TaylP def I wrote `(iteratedDeriv j (Ffun n) 1 / j !)` — j ! : ℂ? The expression `iteratedDeriv j (Ffun n) 1 / j !` — iteratedDeriv gives ℂ; j ! must be ℂ — elaborates (j ! : ℂ) via Nat.cast (OfNat? no — j ! is Nat.factorial j : ℕ, then cast). In LiResidue: lcoeff k := iteratedDeriv (k+1) hLi 1 / (k+1)! — the (k+1)! elaborated as... with open scoped Nat, (k+1)! is factorial; the division ℂ/ℕ? There must be a cast — Lean inserts Nat.cast since (k+1)! : ℕ and division needs ℂ: via `Nat.cast`? HPDiv ℂ ℕ ℂ? There's a homogeneous... In LiResidue it compiled — so `(k + 1)!` in that position elaborates fine (probably ↑(k+1)! via the / instance for ℂ ℕ — there's `instHDiv ℂ ℕ`? via `Div ℂ` from... hmm, ℂ/ℕ: `instHDiv` from `NormedDivisionRing`? Actually there's `Div ℂ` only for ℂ/ℂ; the elaborator unifies ? and inserts a coercion: `(k+1)!` can elaborate AT type ℂ: Nat.factorial (k+1) : ℕ, coe to ℂ via the expected type from HDiv ℂ ? ℂ — ? gets ℕ with a lift... In Lean4/Mathlib, `x / n` with x : ℂ, n : ℕ works via `instHDiv ℂ ℕ ℂ` (from `DivInvMonoid`? there's a general `HDiv α ℕ α`? I don't think so... but LiResidue compiled with exactly this pattern — lcoeff def line 147: `iteratedDeriv (k + 1) hLi 1 / (k + 1)!` ✓ compiles. And Acoeff: `/ Nat.factorial (n + 1 - i)` — I wrote Nat.factorial explicitly there. For TaylP I'll mirror Acoeff: write `(iteratedDeriv j (Ffun n) 1 / (j ! : ℂ))` hmm or Nat.factorial j explicitly cast: `iteratedDeriv j (Ffun n) 1 / (Nat.factorial j : ℂ)`. To be safe mirror lcoeff's style: `/ j !` with open scoped Nat ✓ proven to compile.\n\nThen in hfi: the factorial in the denominator — after sum_eq_single the goal will have whatever form. I'll adapt at compile time.\n\nsum_eq_single: `Finset.sum_eq_single (i) (h₀ : ∀ j ∈ s, j ≠ i → f j = 0) (h₁ : i ∉ s → f i = 0) : ∑ j ∈ s, f j = f i` ✓ standard.\n\nThe h₀ case (j ∈ range(n+1), j ≠ i): term = c_j * (j.descFactorial i * 0^{j−i}) = 0:\nby_cases j < i: descFactorial = 0: Nat.descFactorial_eq_zero_iff_lt? — hmm exact name: `Nat.descFactorial_eq_zero_iff_lt : n.descFactorial i = 0 ↔ n < i`? In A_iter they didn't need it. I believe `Nat.descFactorial_eq_zero_iff_lt` exists... let me think — there's `Nat.descFactorial_eq_zero_iff_lt : ∀ {n i : ℕ}, n.descFactorial i = 0 ↔ n < i` ✓ I'm fairly confident. Then ((j.descFactorial i : ℕ) : ℂ) = 0 by cast, mul_zero etc.\nelse i < j (since ≠): 0^{j−i} with j−i > 0: zero_pow (by omega : j − i ≠ 0): (0:ℂ)^(j−i) = 0; mul_zero.\n\nStructure:\n```lean\n  · intro j hj hji\n    rw [Finset.mem_range] at hj\n    by_cases hlt : j < i\n    · have : (j.descFactorial i : ℂ) = 0 := by\n        have := Nat.descFactorial_eq_zero_iff_lt.mpr hlt\n        simp [this]  -- cast of 0\n      rw [this]; simp\n    · have hgt : i < j := by omega\n      have : (0 : ℂ) ^ (j - i) = 0 := zero_pow (by omega)\n      rw [this]; simp\n```\nThen `simp` closes c_j * (0 * ...) = 0 etc. — mul_zero/zero_mul chains — `simp` should. Or `ring`-ish — no, has hypothesis rewrites; use simp [this] forms.\n\nLet me restructure: prove a standalone term-identity lemma:\n```lean\nlemma iteratedDeriv_sub_one_pow (i j : ℕ) :\n    iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) (1 : ℂ) =\n      (j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i) := ...\n```\nthen in the TaylP computation, transform the sum via sum_congr into c_j * (...) and finish. \n\nActually — simplification opportunity: instead of sum_eq_single gymnastics, note:\n\nΣ_{j=0}^{n} c_j·(j.descFactorial i)·0^{j−i}: for j < i descFactorial kills; j > i the 0^{j−i} kills; only j = i survives (needs i ≤ n ✓). This is exactly sum_eq_single. Fine as planned.\n\nNow — potential issue with `iteratedDeriv_TaylP`'s statement: the iteratedDeriv i (TaylP n) 1 — TaylP n is the def; the rw [show lambda = sum-of-lambdas] trick: goal `iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1`. unfold TaylP: `iteratedDeriv i (fun w => ∑ j ∈ range(n+1), c_j*(w−1)^j) 1 = ...`. Hmm — `unfold TaylP` — does iteratedDeriv i (TaylP n) 1 unfold to iteratedDeriv i (fun w => ...) 1? TaylP n is a def : ℂ → ℂ? I defined TaylP (n : ℕ) (w : ℂ) : ℂ := Σ ... — so TaylP n is a lambda — unfold works or `show iteratedDeriv i (fun w : ℂ => ∑ ...) 1 = _` (defeq ✓). Then iteratedDeriv_sum needs the function in the form `fun x => ∑ i ∈ I, f i x` ✓ matches the lambda directly — no funext-rw needed! (iteratedDeriv_sum's LHS is iteratedDeriv n (fun x => ∑ i ∈ I, f i x) x presumably — check at compile; if it's the Pi.sum form, do the funext rw.)\n\nOK — one more: `Ffun_sub_TaylP_iteratedDeriv`'s final step: after rw [iteratedDeriv_sub hF hT, iteratedDeriv_TaylP hi]: goal `iteratedDeriv i (Ffun n) 1 − iteratedDeriv i (Ffun n) 1 = 0` — `simp`/`sub_self` — but wait: iteratedDeriv_sub hF hT : iteratedDeriv i (Ffun n − TaylP n) 1 = iteratedDeriv i (Ffun n) 1 − iteratedDeriv i (TaylP n) 1 — the (f − g) form: iteratedDeriv_sub's statement: iteratedDeriv n (f − g) x = iteratedDeriv n f x − iteratedDeriv n g x? From A_iter: `iteratedDeriv_sub hf hg` used after rewriting the lambda into (fun..) − (fun..) Pi form. So my goal's function Ffun n − TaylP n is ALREADY Pi.sub of the two defs ✓ direct match, no funext bridge needed. Then rw [iteratedDeriv_TaylP hi] rewrites iteratedDeriv i (TaylP n) 1 → iteratedDeriv i (Ffun n) 1; then sub_self: `rw [iteratedDeriv_TaylP hi, sub_self]` — wait sub_self : a − a = 0 ✓ but the goal is `... = 0`: `rw [iteratedDeriv_TaylP hi]; exact sub_self _` hmm sub_self is the equality itself: `sub_self : a - a = 0` — `exact sub_self _` ✓ or simp.\n\nOrder of definitions in the file — iteratedDeriv_TaylP needs nothing else; Ffun_sub_TaylP_iteratedDeriv needs it; Ffun_sub_TaylP_order needs those; Rfun_eq_sub_div needs Jlag_mul_pow + ppart_mul_pow; Rfun_tendsto_one needs order + eq_div; Rfun_bounded needs tendsto; Rfun_residue_at needs zeta_order_ne_top + ppart_continuousAt + kFun_differentiableAt; rectInt'_Jlag needs everything + rectangle_mem_nhds_of_mem_not_border.\n\nAlso: LiPrincipal's ppart/Acoeff are in namespace NguyenRH1 ✓ same namespace, direct reference ✓. ResW1 from LiResidue ✓. LiPrincipal imports LiResidue; LiSides imports LiPrincipal ✓ transitively gets LiResidue.\n\nImport line: `import NguyenRH1.LiPrincipal` + `import Zeta23.Analytic.RectangleLogDeriv` (for residueTheorem_finset) + Mathlib (LiPrincipal already imports Mathlib — transitively available; explicit import Mathlib is harmless and customary).\n\nNow, does the package's root file need updating to include LiSides? NguyenRH1.lean (the root) probably imports the submodules — check research/lean/NguyenRH1/NguyenRH1.lean. If it lists imports, add LiSides there — that's a NEW addition (allowed — not editing proofs). Let me check.\n\nAlso — `riemannZeta_residue_one` — LiResidue used it ✓ available via Mathlib import ✓.\n\n`hasDerivAt_zpow` was LiPrincipal's — not needed here.\n\nLet me also double check `zeroMult` is in scope: it's Zeta23.zeroMult? In Statement.lean — namespace? LiSkeleton used `zeroMult ρ` with open Zeta23 ✓ (line 47). ✓\n\n`logDeriv_pow` signature: logDeriv (f^m) x = m * logDeriv f x? — vendored used logDeriv_pow in e2 ✓.\n\n`logDeriv_comp` signature: logDeriv_comp (hf : DifferentiableAt ℂ f (g x)?) (hg : DifferentiableAt ℂ g x) : logDeriv (f ∘ g) x = logDeriv g x · deriv...? vendored: logDeriv_comp (by fun_prop) (by fun_prop) — copy ✓.\n\nOne risk: `simp` after `rw [..., logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]` in e2 — the goal after those rewrites: logDeriv-of-composition gives (logDeriv (fun x => x^m)) ((s−ρ)) · deriv (fun z => z−ρ) s?? Actually logDeriv_comp : logDeriv (f ∘ g) x = (logDeriv f (g x)) * deriv g x? — logDeriv f = f'/f so logDeriv (f∘g) = (f∘g)'/(f∘g) = (f'(g x)·g'(x))/(f (g x)) = logDeriv f (g x) · g'(x)... yes = logDeriv f (g x) * deriv g x. With f = x^m: logDeriv f y = m·y^{m−1}/y^m... hmm logDeriv_pow : logDeriv (fun x => x^m) x = m/x? or m·x^{m−1}/x^m? vendored got to (m:ℂ)/(s−q) via `simp` after — so logDeriv_pow must give m·x^{m-1}/x^m-ish and simp simplifies to m/x with x ≠ 0 in context? But s − ρ ≠ 0 needs to be available to simp... In the vendored e2 (line 259-264): the simp at the end (line 264) closed e2 : logDeriv ((s−q)^ord) s = (ord:ℂ)/(s−q). The simp call was bare `simp` — with hsq : s − q ≠ 0 in context? simp uses hypotheses? No — bare simp doesn't use hsq. Hmm — maybe logDeriv_pow : logDeriv (fun x => x ^ n) x = n / x directly? If logDeriv_pow states logDeriv (x^n) = n·logDeriv x = n·(1/x) = n/x: deriv x = 1, so logDeriv x = 1/x — simp [logDeriv_apply, deriv_id''] ... The vendored pattern compiled — I'll copy it verbatim and adjust if it fails.\n\nLet me look at vendored e2 once more:\n```lean\nhave e2 : logDeriv (fun s : ℂ => (s - q) ^ analyticOrderNatAt f q) s\n    = (analyticOrderNatAt f q : ℂ) / (s - q) := by\n  rw [show (fun s : ℂ => (s - q) ^ analyticOrderNatAt f q)\n      = (fun x : ℂ => x ^ analyticOrderNatAt f q) ∘ (fun s => s - q) from rfl,\n    logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n  simp\n```\nSo after the rewrites, goal is something simp closes. logDeriv_pow : logDeriv (fun x => x^n) = fun x => n * x^(n-1) / x^n? or (n : 𝕜)/x? If it were n/x, the remaining after logDeriv_comp: (n/(s−q))·deriv (fun s => s−q) s — deriv = 1 — simp [deriv_sub_const, deriv_id''] closes ✓. That's consistent with logDeriv_pow : logDeriv (fun x => x ^ n) x = ↑n / x. OK copy.\n\nfun_prop discharges: DifferentiableAt ℂ (fun x => x^m) (s−ρ) ✓ and DifferentiableAt ℂ (fun s => s−ρ) s ✓.\n\nNow — one more design question: the near-at-1 boundedness — actually WAIT. I realize there might be an issue with the `near` hypothesis at 1 in residueTheorem_finset: it's `(f - fun s => A p / (s - p)) =O[𝓝[≠] p] (1 : ℂ → ℂ)` — with A 1 = 0: fun s => 0/(s−1) = fun s => 0 — f − 0 = f. The simpa [hAdef] approach: goal after `rcases ... rfl`: ((Rfun n) − fun s => A 1 / (s - 1)) =O[𝓝[≠] 1] 1. simpa [hAdef] using Rfun_bounded_near_one n: simp normalizes the goal: A 1 → (if 1 = 1 then 0 else ...) → 0 (if_pos rfl — via simp [hAdef]: unfold A — hAdef : A = fun p => if p = 1 then 0 else ... — simp [hAdef] rewrites A to the lambda, then if_pos... `simp` handles if-then-else with rfl condition ✓), 0/(s−1) → 0 (zero_div ✓ simp), then (fun s => 0) : Pi.sub (Rfun n) (fun s => 0) → Rfun n − 0 → sub_zero... For functions: Rfun n − (fun s => 0) = Rfun n via sub_zero (Pi instSubNeg... sub_zero : a − 0 = a ✓ simp). And (fun s => (0:ℂ)) = 0? Pi.zero defeq ✓ simp [Pi.zero_apply] handles. So simpa [hAdef] should work. If hAdef is a `set ... with` equation — set A := ... with hAdef — hAdef : A = fun p => ... ✓ simp [hAdef] rewrites ✓.\n\nHmm — actually with `set A := fun p => ... with hAdef`, the residueTheorem_finset application `key := residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A hS fHolo near` — the `near` proof is where the case analysis happens. Fine.\n\nBUT: residueTheorem_finset's conclusion: RectangleIntegral' (Rfun n) z w = ∑ p ∈ insert 1 Sz, A p. With set A, the sum displays as A p — then hsum rewrite ✓.\n\nAlso — `(f := Rfun n)` — the near obligations' functions: ((Rfun n) − fun s => A p / (s − p)) ✓ matches Rfun_residue_at's statement form: ((Rfun n) - fun s => ((zeroMult ρ:ℂ)·...)/(s−ρ)) =O[𝓝[≠] ρ] 1 — with ρ := p and the A p — need A p = the formula: by simp [hAdef, hp1] (if_neg hp1: p ≠ 1 ✓). So:\n```lean\n    · have hp1 : p ≠ 1 := hSz_ne_one p hp\n      have hAp : A p = (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) := by simp [hAdef, hp1]\n      rw [hAp]\n      exact Rfun_residue_at n hp1\n```\n✓ (rw [hAp] on the goal rewrites A p → formula ✓).\n\nif_neg with hp1: simp [hAdef, hp1] — the if condition is p = 1; hp1 : p ≠ 1 — simp uses hp1 to close if_neg ✓.\n\nNow the final assembly order in rectInt'_Jlag:\n```lean\ntheorem rectInt'_Jlag (n : ℕ) {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)\n    (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ))\n    (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0)\n    (Sz : Finset ℂ) (hSz : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0) :\n    RectangleIntegral' (Jlag n) z w =\n      ResW1 n + ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n  classical\n  have hzA1 : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num\n  have h1notSz : (1 : ℂ) ∉ Sz := fun h => hzA1 ((hSz 1).mp h).2\n  have hSz_ne_one : ∀ ρ ∈ Sz, ρ ≠ 1 := fun ρ hρ h => h1notSz (h ▸ hρ)\n  have hSz_zeta : ∀ ρ ∈ Sz, riemannZeta ρ = 0 := by\n    intro ρ hρ\n    have hρ1 := hSz_ne_one ρ hρ\n    have h2 := ((hSz ρ).mp hρ).2\n    rw [zetaA_apply hρ1, mul_eq_zero] at h2\n    rcases h2 with h | h\n    · exact absurd (sub_ne_zero.mpr hρ1) (by exact fun hh => h (sub_eq_zero.mpr hh))...\n```\nhmm: h : ρ − 1 = 0 ⟹ contradiction with hρ1 : ρ ≠ 1: sub_eq_zero.mp h : ρ = 1 ✓ `exact absurd (sub_eq_zero.mp h) hρ1`. \n```\n    rcases h2 with h | h\n    · exact absurd (sub_eq_zero.mp h) hρ1\n    · exact h\n```\n✓.\n\nContinue:\n```lean\n  have hSzint : ∀ ρ ∈ Sz, Rectangle z w ∈ 𝓝 ρ := by\n    intro ρ hρ\n    exact rectangle_mem_nhds_of_mem_not_border hre him ((hSz ρ).mp hρ).1\n      (fun hb => hborder ρ hb (hSz_zeta ρ hρ))\n  set A : ℂ → ℂ := fun p => if p = 1 then 0 else (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) with hAdef\n  have fHolo : HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert (1 : ℂ) Sz)) := by\n    intro s hs\n    have hsc : s ∉ (↑(insert (1 : ℂ) Sz) : Set ℂ) := hs.2\n    have hs1 : s ≠ 1 := fun h => hsc (Finset.mem_coe.mpr (h ▸ Finset.mem_insert_self 1 Sz))\n    have hsSz : s ∉ Sz := fun h => hsc (Finset.mem_coe.mpr (Finset.mem_insert_of_mem h))\n    have hs0 : riemannZeta s ≠ 0 := by\n      intro h0\n      exact hsSz ((hSz s).mpr ⟨hs.1, by rw [zetaA_apply hs1, h0, mul_zero]⟩)\n    exact (Rfun_differentiableAt hs1 hs0).differentiableWithinAt\n  have key := Analytic.residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A\n    (by intro p hp; rw [Finset.mem_insert] at hp; rcases hp with rfl | hp; exacts [h1, hSzint p hp])\n    fHolo\n    (by\n      intro p hp\n      rw [Finset.mem_insert] at hp\n      rcases hp with rfl | hp\n      · simpa [hAdef] using Rfun_bounded_near_one n\n      · have hp1 : p ≠ 1 := hSz_ne_one p hp\n        have hAp : A p = (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) := by simp [hAdef, hp1]\n        rw [hAp]\n        exact Rfun_residue_at n hp1)\n  have hsum : ∑ p ∈ insert 1 Sz, A p =\n      ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n    rw [Finset.sum_insert h1notSz]\n    have hA1 : A 1 = 0 := by simp [hAdef]\n    rw [hA1, zero_add]\n    apply Finset.sum_congr rfl\n    intro ρ hρ\n    have hρ1 := hSz_ne_one ρ hρ\n    simp [hAdef, hρ1]\n  rw [hsum] at key\n  have hRint : RectangleBorderIntegrable (Rfun n) z w := by\n    apply ContinuousOn.rectangleBorder_integrable\n    apply fHolo.continuousOn.mono\n    intro s hs\n    have hsR : s ∈ Rectangle z w := rectangleBorder_subset_rectangle z w hs\n    refine ⟨hsR, fun hsc => ?_⟩\n    rw [Finset.mem_coe, Finset.mem_insert] at hsc\n    rcases hsc with h | h\n    · exact not_mem_rectangleBorder_of_rectangle_mem_nhds h1 (h ▸ hs)\n    · exact hborder s hs (hSz_zeta s h)\n  have hPint : RectangleBorderIntegrable (ppart n) z w := by\n    apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n    intro s hs\n    exact (ppart_differentiableAt hs.2).differentiableWithinAt\n  have heq : Jlag n = Rfun n + ppart n := (sub_add_cancel _ _).symm\n  rw [heq, RectangleIntegral'_add _ _ _ _ hRint hPint, key, rectInt'_ppart hre him h1, add_comm]\n```\nHmm wait — heq : Jlag n = Rfun n + ppart n: sub_add_cancel (a b) : a − b + b = a — (sub_add_cancel (Jlag n) (ppart n)) : Jlag n − ppart n + ppart n = Jlag n. Rfun n + ppart n =?= Jlag n − ppart n + ppart n defeq (delta Rfun) — the TERM (sub_add_cancel _ _).symm : Jlag n = Jlag n − ppart n + ppart n — assigning to heq : Jlag n = Rfun n + ppart n requires defeq of Rfun n + ppart n and Jlag n − ppart n + ppart n ✓ delta-unfold Rfun — should typecheck ✓ (Pi.add_apply: (Rfun n + ppart n) — as functions, Rfun n + ppart n vs (Jlag n − ppart n) + ppart n — the TERMS: Rfun n delta-unfolds to Jlag n − ppart n ✓).\n\nThen rw [heq]: goal RectangleIntegral' (Jlag n) z w = ... becomes RectangleIntegral' (Rfun n + ppart n) z w = ... ✓.\nrw [RectangleIntegral'_add _ _ _ _ hRint hPint]: its statement: RectangleIntegral'_add (f g : ℂ → ℂ) (z w) (hf) (hg) : RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w — the explicit underscores: f g z w inferred from hRint/hPint ✓ (they determine f = Rfun n etc.). Rewrite ✓.\nrw [key]: RectangleIntegral' (Rfun n) z w → Σ formula ✓.\nrw [rectInt'_ppart hre him h1]: RectangleIntegral' (ppart n) z w → ResW1 n ✓.\nFinal: Σ + ResW1 n = ResW1 n + Σ → rw [add_comm] — DANGER: add_comm rewrites the FIRST a + b it finds — the LHS Σ + ResW1 n → ResW1 n + Σ — but there are additions inside the sum formula?? The sum formula (1 − (ρ/(ρ−1))^n) has no +. The exponent (n+1) etc. — not in this goal. The goal: ∑ ρ ∈ Sz, formula + ResW1 n = ResW1 n + ∑ ρ ∈ Sz, formula. rw [add_comm] rewrites the first `_ + _` — top-level LHS sum+ResW1 — actually rw rewrites the first MATCHING subterm in the goal — the goal's first add: (Σ ...) + (ResW1 n) ✓ becomes ResW1 n + Σ — then goal: ResW1 n + Σ = ResW1 n + Σ — rfl closed automatically by rw ✓. Safer: `rw [add_comm (∑ ...) (ResW1 n)]` with explicit args — the explicit sum term is long; use `ac_rfl`? or `ring`! Final step: `ring` closes a + b = b + a over the commutative ring ℂ ✓ (the sums are opaque terms — ring treats as atoms ✓). Use `ring`.\n\nAlso — one more check on `Finset.sum_insert h1notSz`: insert 1 Sz with 1 ∉ Sz ✓ gives A 1 + Σ_{p ∈ Sz} A p ✓.\n\nAnd hA1 : A 1 = 0 by simp [hAdef] — if 1 = 1 → if_pos ✓.\n\nNow — Rfun_residue_at's exact statement. Also — POTENTIAL ISSUE: `zeroMult` — it's `Zeta23.zeroMult` — with open Zeta23 ✓ accessible as zeroMult ✓ (LiSkeleton confirms).\n\nAlso `logDeriv` — open? logDeriv is root-namespace (Mathlib.Analysis.Calculus.LogDeriv) ✓ vendored uses bare logDeriv ✓.\n\n`𝓝[≠]` notation — needs `open Topology`? It's `nhdsWithin` sieve notation from Filter — LiResidue used 𝓝[≠] with `open ... Filter Topology` ✓ have both.\n\n`Finset.Icc`/`range` ✓.\n\nLet me also double check `analyticAt_riemannZeta` : (hs : s ≠ 1) → AnalyticAt ℂ riemannZeta s ✓ used in LiResidue ✓.\n\n`riemannZeta_residue_one` : Tendsto (fun w => (w−1)·ζ w) (𝓝[≠] 1) (𝓝 1) ✓ LiResidue.\n\nOK — also potential elaboration pitfall: `(by intro p hp; ... exacts [h1, hSzint p hp])` — after rcases hp with rfl | hp: first goal p := 1 — wait rcases with rfl on hp : p = 1 ∨ p ∈ Sz — `rcases hp with rfl | hp` — first branch substitutes p = 1? hp : p = 1 — rfl pattern substitutes p := 1 (or 1 := p) ✓ goal Rectangle z w ∈ 𝓝 1 — exact h1 — but wait if the substitution goes the other way (1 := p — can't, 1 is not a local var) ✓ p := 1 ✓.\n\nNow, let me also think about whether `HolomorphicOn` needs unpacking: HolomorphicOn f s = DifferentiableOn ℂ f s — residueTheorem_finset's fHolo : HolomorphicOn f (Rectangle z w \\ ↑S) — my fHolo proof: `intro s hs; exact (...).differentiableWithinAt` — DifferentiableOn intro pattern ✓ (HolomorphicOn is reducible-def? `HolomorphicOn f s : Prop := DifferentiableOn ℂ f s` — intro s hs works if it's a def unfolding to ∀ — Pi intro on the goal HolomorphicOn f S after intro s hs — need the goal to be `∀ s ∈ ..., DifferentiableWithinAt ...` — HolomorphicOn is defined as DifferentiableOn ℂ f s := ∀ x ∈ s, DifferentiableWithinAt... — the `intro s hs` on goal `HolomorphicOn f S`: Lean unfolds the def to introduce ✓ works (vendored/LiPrincipal did exactly this: `intro s hs` then DifferentiableWithinAt ✓).\n\n`ContinuousOn.rectangleBorder_integrable` — vendored line 129: ContinuousOn.rectangleBorder_integrable (hf₂holo.continuousOn.mono hbS) — applied as a term. My usage: `apply ContinuousOn.rectangleBorder_integrable; apply fHolo.continuousOn.mono; intro s hs; ...` — mono's argument: border ⊆ Rectangle ∖ S — `intro s hs` with hs : s ∈ RectangleBorder z w, goal s ∈ Rectangle z w \\ ↑(insert 1 Sz) ✓ my proof provides the pair ⟨hsR, notin⟩ — I wrote `refine ⟨hsR, fun hsc => ?_⟩` — the second component: s ∉ ↑(insert 1 Sz) — as fun hsc => proof-of-False ✓. But — Set complement membership: s ∈ X \\ Y := s ∈ X ∧ s ∉ Y ✓ anonymous constructor ✓. The goal after `apply ... .mono`: RectangleBorder z w ⊆ Rectangle z w \\ ↑(insert 1 Sz) — intro s hs ✓.\n\nfHolo.continuousOn : ContinuousOn (Rfun n) (Rectangle z w \\ ↑(insert 1 Sz)) — HolomorphicOn.continuousOn ✓ exists (vendored used hf₂holo.continuousOn ✓).\n\nAlso `Set.Finite.mem_toFinset` — only in the (skipped) corollary. Skip.\n\nOne more: `mem_of_mem_nhds` ✓ vendored line 283.\n\nNow — hmm, ONE MORE THING. `Rfun_tendsto_one`'s ⊤-case:\n```lean\n    have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), g s = 0 := analyticOrderAt_eq_top.mp htop\n```\nanalyticOrderAt_eq_top : analyticOrderAt f z₀ = ⊤ ↔ ∀ᶠ z in 𝓝 z₀, f z = 0 ✓ (line 75). With g := Ffun n − TaylP n — h0 : ∀ᶠ s, (Ffun n − TaylP n) s = 0 — Pi.sub_apply: (Ffun n − TaylP n) s = Ffun n s − TaylP n s — the eventual-eq chain:\n```lean\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      rw [hs]\n      -- hg0 : (Ffun n − TaylP n) s = 0; goal: (Ffun n s − TaylP n s)/(s−1)^{n+1} = 0\n      have hg0' : Ffun n s - TaylP n s = 0 := by\n        have := hg0  -- (Ffun n − TaylP n) s = 0\n        rw [Pi.sub_apply] at this; exact this  -- hmm (f − g) s = f s − g s via Pi.sub_apply ✓\n      rw [hg0']; simp  -- 0 / _ = 0: zero_div ✓ simp\n```\nWait — `set g := Ffun n - TaylP n with hg` earlier: then analyticOrderAt g 1 — h0 : ∀ᶠ s, g s = 0 — g s is the set-local-def application; g s = (Ffun n − TaylP n) s defeq ✓ rw [hg] at... With `set`, g is a local def and hg : g = Ffun n − TaylP n. hg0 : g s = 0 — I need Ffun n s − TaylP n s = 0: `rw [hg] at hg0` gives (Ffun n − TaylP n) s = 0 then Pi.sub_apply... or hg0 : g s = 0 and the hs-rewritten goal: (Ffun n s − TaylP n s)/(s−1)^{n+1} = 0 — hmm Rfun_eq_sub_div_near_one gives Rfun n s = (Ffun n s − TaylP n s)/(s−1)^{n+1} — the numerator in lambda form. From hg0 (g s = 0, g delta= Ffun n − TaylP n): g s = (Ffun n − TaylP n) s = Ffun n s − TaylP n s by defeq: `have hg0' : Ffun n s - TaylP n s = 0 := hg0` — defeq through delta+Pi.sub_apply — `exact hg0` should typecheck by defeq ✓. If not: `by rw [hg, Pi.sub_apply] at hg0; exact hg0`.\n\nThen `rw [hs, hg0']`; goal 0/(s−1)^{n+1} = 0: `exact zero_div _` ✓.\n\nActually hold on — `set g := ...` would also fold occurrences... Ffun_sub_TaylP_order n : ((n+1:ℕ):ℕ∞) ≤ analyticOrderAt (Ffun n − TaylP n) 1 — after set g, hord := Ffun_sub_TaylP_order n : ... ≤ analyticOrderAt (Ffun n − TaylP n) 1 — with set active, is it displayed/folded to g? `set` folds the goal and context at time of invocation; hord is obtained AFTER via `have hord := Ffun_sub_TaylP_order n` — its type mentions Ffun n − TaylP n which is defeq to g — subsequent rewrites on analyticOrderAt g 1 vs analyticOrderAt (Ffun n − TaylP n) 1 — MISMATCH risk: htop : analyticOrderAt g 1 = ⊤ (from by_cases on the goal... wait by_cases htop : analyticOrderAt g 1 = ⊤ — I'd write it explicitly) vs hord's analyticOrderAt (Ffun n − TaylP n) 1. To avoid all this: DON'T use set; write Ffun n − TaylP n everywhere. Verbose but zero risk. Same for m — avoid set.\n\nHmm, wait — but hfh from hgan.analyticOrderAt_ne_top.mp : (Ffun n − TaylP n) =ᶠ[𝓝 1] fun z => (z − 1)^analyticOrderNatAt (Ffun n − TaylP n) 1 • h z ✓ explicit. Fine.\n\nLet me also reconsider `Nat.cast_analyticOrderNatAt htop` — signature: Nat.cast_analyticOrderNatAt (hf : analyticOrderAt f z₀ ≠ ⊤) : ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀ ✓ — rewrite hord : ((n+1:ℕ):ℕ∞) ≤ analyticOrderAt (Ffun n − TaylP n) 1 via ← this: rw [← Nat.cast_analyticOrderNatAt htop] at hord — turns analyticOrderAt ... 1 into ↑(analyticOrderNatAt ...) ✓ then ENat.natCast_le_natCast.mp hord : n + 1 ≤ analyticOrderNatAt (Ffun n − TaylP n) 1 ✓ (the cast ((n+1:ℕ):ℕ∞) vs (analyticOrderNatAt ... : ℕ∞) — natCast_le_natCast : (↑n ≤ ↑m) ↔ n ≤ m ✓ matches).\n\nIn the hev for the m-case: \n```lean\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 ≠ 0 := sub_ne_zero.mpr (Set.mem_compl_singleton_iff.mp? ...)\n```\nhs1 : s ∈ {1}ᶜ? self_mem_nhdsWithin : s ∈ 𝓝[≠] 1 — wait self_mem_nhdsWithin : s ∈ 𝓝[≠] 1 — no: self_mem_nhdsWithin is a FILTER statement: {s | s ≠ 1} ∈ 𝓝[≠] 1 — filter_upwards [self_mem_nhdsWithin] with s hs1 — hs1 : s ≠ 1 ✓ (𝓝[≠] 1 = 𝓝[{1}ᶜ] 1; self_mem_nhdsWithin : s ∈ 𝓝[S] x — hmm self_mem_nhdsWithin : S ∈ 𝓝[S] x ✓ so hs1 : s ∈ {1}ᶜ — defeq s ≠ 1; `by simpa using hs1` or Set.mem_compl_iff... LiResidue line 133-139 used: filter_upwards [..., eventually_mem_nhdsWithin] with w hw hw1 then used hw1 : w ≠ 1 — wait eventually_mem_nhdsWithin : {y | y ∈ S} ∈ 𝓝[S] x — for S = {1}ᶜ: hw1 : w ∈ {1}ᶜ — used as w ≠ 1? In hLi_eq_near_one: `filter_upwards [hne, eventually_mem_nhdsWithin] with w hw hw1` then hw1 used where? hLi_eq_of_ne hw1 hz — hw1 : w ≠ 1 — so w ∈ {1}ᶜ coerces/defeqs to w ≠ 1 ✓ (Set.mem_compl_singleton_iff defeq). OK: hs1 : s ≠ 1 usable directly-ish; wrap with `by simpa using hs1` if needed.\n\nLet me write `have hs1n : s ≠ 1 := by simpa using hs1` — wait self_mem_nhdsWithin gives s ∈ {y | y ≠ 1}? 𝓝[≠] 1 = 𝓝[Set.compl {1}]... the set is {1}ᶜ — membership s ∈ {1}ᶜ unfolds to s ∉ {1} to s = 1 → False — `simpa using hs1` gives s ≠ 1 ✓ (mem_compl_iff, mem_singleton_iff simp). Actually since LiResidue passed hw1 directly to hLi_eq_of_ne (w ≠ 1), the defeq works — exact would accept. I'll use hs1 directly where s ≠ 1 is needed, with simpa-fallback.\n\nContinuing hev:\n```lean\n      have hs1' : s - 1 ≠ 0 := sub_ne_zero.mpr hs1\n      rw [hs]  -- goal: (Ffun n s − TaylP n s)/(s−1)^{n+1} = (s−1)^{m−(n+1)} * h s\n      have hgs : (Ffun n - TaylP n) s = (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      -- hgf : (Ffun n − TaylP n) =ᶠ[𝓝 s] fun z => (z−1)^m • h z\n      -- the goal's LHS numerator: Ffun n s − TaylP n s — defeq (Ffun n − TaylP n) s\n      rw [show Ffun n s - TaylP n s = (Ffun n - TaylP n) s from rfl, hgs]\n      have e : (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 =\n          (s - 1) ^ (n + 1) * (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) := by\n        rw [← pow_add]; congr 1; omega  -- needs hnm : n + 1 ≤ analyticOrderNatAt ...\n      rw [e]\n      field_simp [hs1', pow_ne_zero (n+1) hs1']\n      ring\n```\nhnm : n + 1 ≤ analyticOrderNatAt (Ffun n − TaylP n) 1 — proved before hev. The omega inside e needs hnm in context ✓.\n\nfield_simp then ring: (X^{n+1}·X^k)·h s / X^{n+1} = X^k·h s — field_simp [pow_ne_zero (n+1) hs1'] — goal becomes X^{n+1}·X^k·h s = X^k·h s·X^{n+1}? — ring closes ✓. Hmm field_simp on `A / B = C` multiplies out: A = C·B ✓ then ring. Or more directly: `rw [mul_div_cancel_left₀?]`... mul_div_cancel_left₀ : a ≠ 0 → a·b/a = b? The form: (X^{n+1}·(X^k·h s))/X^{n+1} = X^k·h s — mul_div_cancel_left₀ (pow_ne_zero (n+1) hs1') : a·b/a = b — matches with a := X^{n+1}, b := X^k·h s — but the numerator is X^{n+1}·h s·... association — after rw [e], numerator: (s−1)^{n+1}·(s−1)^k * h s — that's ((s−1)^{n+1}·(s−1)^k)·h s vs a·b form needs (s−1)^{n+1}·((s−1)^k·h s) — reassociate: mul_assoc. Let me do:\n```lean\n      rw [e, mul_assoc, mul_div_cancel_left₀ (pow_ne_zero (n + 1) hs1')]\n```\nmul_div_cancel_left₀ : a ≠ 0 → (a * b) / a = b ✓ (name: mul_div_cancel_left₀ exists in Mathlib ✓ I believe — GroupWithZero). After e: ((s−1)^{n+1}·(s−1)^k)·h s/(s−1)^{n+1}; mul_assoc → (s−1)^{n+1}·((s−1)^k·h s)/(s−1)^{n+1}; mul_div_cancel_left₀ → (s−1)^k·h s ✓ = goal RHS ✓ rfl auto.\n\nWait — the numerator after hgs rewrite: ((s−1)^m·h s)/(s−1)^{n+1} where m := analyticOrderNatAt... — e rewrites (s−1)^m → (s−1)^{n+1}·(s−1)^{m−(n+1)} ✓. Then the expression: ((s−1)^{n+1}·(s−1)^{m−(n+1)}·... hmm (s−1)^m * h s with e rewritten inside: rw [e] rewrites (s−1)^m to the product: ((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} — then mul_div_cancel_left₀ (h : (s−1)^{n+1} ≠ 0) : (s−1)^{n+1}·X/(s−1)^{n+1} = X ✓. Signature mul_div_cancel_left₀ : a ≠ 0 → a * b / a = b ✓ I'm fairly confident (there's also mul_div_cancel_left). Try; fallback field_simp+ring.\n\nThen the final Tendsto:\n```lean\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    have hT := hcont.tendsto.mono_left nhdsWithin_le_nhds\n    exact hT.congr' hev.symm\n```\nhcont.tendsto : Tendsto φ (𝓝 1) (𝓝 (φ 1)) — φ 1 = (1−1)^k·h 1 ✓ matches the refine witness ✓ (ContinuousAt.tendsto : Tendsto f (𝓝 x) (𝓝 (f x)) ✓).\nmono_left nhdsWithin_le_nhds : 𝓝[≠] 1 ≤ 𝓝 1 ✓.\nhT.congr' hev.symm : Tendsto.congr' (φ =ᶠ Rfun) (Tendsto φ) : Tendsto Rfun ✓.\n\nTendsto congr' signature: `Filter.Tendsto.congr' : f₁ =ᶠ[l] f₂ → Tendsto f₁ l l₂ → Tendsto f₂ l l₂` — hev.symm : φ =ᶠ Rfun (hev : Rfun =ᶠ φ) ✓ hT.congr' hev.symm ✓.\n\nThe ⊤-case similarly: tendsto_const_nhds.congr' hev0.symm where hev0 : Rfun =ᶠ (fun _ => 0) ✓.\n\nNOW — the §5 `near` at ρ also needs: the `near` function equality — the algebra: I planned simp only [Pi.sub_apply, Rfun, Jlag, hA]; rw [← logDeriv_apply, hld]; field_simp; ring.\n\nWait — one problem: hld rewrites logDeriv riemannZeta s — after ← logDeriv_apply, the term deriv riemannZeta s / riemannZeta s becomes logDeriv riemannZeta s ✓ then hld : logDeriv riemannZeta s = (m:ℂ)/(s−ρ) + logDeriv h s ✓ rw.\n\nBut — does `← logDeriv_apply` also hit `logDeriv h s` on the LHS?? ← logDeriv_apply rewrites deriv ?f ?a / ?f ?a → logDeriv — LHS has logDeriv h s (no deriv quotient) ✓ only RHS has deriv ζ/ζ ✓. But wait — rw [← logDeriv_apply]: logDeriv_apply : logDeriv f a = deriv f a / f a; ← direction: find deriv ?f ?a / ?f ?a in goal, replace with logDeriv ?f ?a. Occurrence: deriv riemannZeta s / riemannZeta s ✓ unique ✓.\n\nAlternatively avoid: state hld in deriv-form: deriv ζ s/ζ s = m/(s−ρ) + deriv h s/h s... whatever, current plan fine.\n\nAlso the hexp statement's LHS function must EXACTLY match the hO lambda for congr'. I'll state hexp as:\n∀ᶠ s in 𝓝[≠] ρ, (fun s => -(m:ℂ)*((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s * logDeriv h s − ppart n s) s = ((Rfun n) − fun s => A-formula/(s−ρ)) s\n— with beta-redexes... filter_upwards produces pointwise equalities with the lambdas applied — messy. Cleaner (vendored style): hexp : (fun s => bigterm) =ᶠ[𝓝[≠] ρ] ((Rfun n) − fun s => ...) — vendored stated hexp as ∀ᶠ s, big = target s and passed to congr' which expects EventuallyEq — ∀ᶠ s, f s = g s IS f =ᶠ g definitionally ✓. So state hexp as ∀ᶠ s in 𝓝[≠] ρ, bigterm = ((Rfun n) − fun s => ...) s — where bigterm written WITHOUT a lambda wrapper (just the expression in s) ✓ vendored did exactly this (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`) ✓ copy that style. Then hO must be about `fun s => bigterm` ✓.\n\nSo:\n```lean\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```\nand\n```lean\n  have hO : (fun s => -((analyticOrderNatAt riemannZeta ρ : ℂ)) * ((kFun n s - kFun n ρ) / (s - ρ))\n      - kFun n s * logDeriv h s - ppart n s) =O[𝓝[≠] ρ] (1 : ℂ → ℂ) := ...\n  exact hO.congr' hexp EventuallyEq.rfl\n```\ncongr' (hf : f =O g) : (hff' : f =ᶠ f') → (hgg' : g =ᶠ g') → f' =O g' — hexp : (fun s => big) =ᶠ target ✓ matches f = big-lambda, f' = target ✓.\n\nThe Tendsto for hO:\n```lean\n  have hT : Tendsto (fun s => -(m:ℂ)*((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s * logDeriv h s − ppart n s)\n      (𝓝[≠] ρ) (𝓝 (-(m:ℂ)*deriv (kFun n) ρ − kFun n ρ * logDeriv h ρ − ppart n ρ)) := by\n    have h1T := (hslope.const_mul (-(m:ℂ)))  -- hmm const_mul : Tendsto f l (𝓝 c) → Tendsto (fun x => a * f x) l (𝓝 (a * c))\n    exact ((hslope.const_mul _).sub hcont1).sub hcont2\n```\nTendsto.const_mul (c) (h : Tendsto f l (𝓝 c')) : Tendsto (fun x => c * f x) l (𝓝 (c * c')) ✓. The lambda forms: hslope : Tendsto (fun s => (kFun n s − kFun n ρ)/(s−ρ)) ... ; const_mul gives fun s => C·((kFun n s − kFun n ρ)/(s−ρ)) ✓; .sub hcont1 : fun s => C·(...) − kFun n s·logDeriv h s — the Pi-style sub of the two lambdas: (fun s => ...) − ... vs fun s => ... − ... — Tendsto.sub's conclusion: Tendsto (fun x => f x − g x)? `Filter.Tendsto.sub : Tendsto f l (𝓝 a) → Tendsto g l (𝓝 b) → Tendsto (fun x => f x − g x) l (𝓝 (a − b))` ✓ (Mathlib's Tendsto.sub has the pointwise lambda form? In Mathlib: Filter.Tendsto.sub (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) : Tendsto (fun x => f x − g x) l (𝓝 (a - b)) ✓ yes pointwise). ✓ then hO := hT.isBigO_one ℂ ✓.\n\nhslope: Tendsto (fun s => (kFun n s − kFun n ρ)/(s−ρ)) (𝓝[≠] ρ) (𝓝 (deriv (kFun n) ρ)) — from hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt : Tendsto (slope (kFun n) ρ) (𝓝[≠] ρ) (𝓝 (deriv (kFun n) ρ)) — slope f a x = (f x − f a)/(x − a) — slope_fun_def_field : slope f a = fun x => (f x − f a)/(x − a)? vendored: simpa only [slope_fun_def_field] using this ✓ copy.\n\nhcont1: Tendsto (fun s => kFun n s * logDeriv h s) (𝓝[≠] ρ) (𝓝 (kFun n ρ * logDeriv h ρ)):\nContinuousAt (fun s => kFun n s * logDeriv h s) ρ := hkd.continuousAt.mul (hh.deriv.continuousAt.div hh.continuousAt hh0) — logDeriv h s = deriv h s/h s ✓ (logDeriv_apply — the lambda with logDeriv vs deriv/div — ContinuousAt (fun s => kFun n s * logDeriv h s): logDeriv h s is defeq deriv h s/h s (logDeriv_apply is a lemma — defeq? logDeriv f x := deriv f x / f x by definition ✓ defeq — the term (hh.deriv.continuousAt.div hh.continuousAt hh0) : ContinuousAt (fun s => deriv h s / h s) ρ... .div gives (fun s => deriv h s) / (fun s => h s) Pi-div — defeq to fun s => deriv h s/h s ✓; then logDeriv h s defeq deriv h s/h s ✓ (logDeriv is a def: logDeriv f = fun x => deriv f x / f x — defeq ✓). exact-with-defeq should accept; else `show` + rw [logDeriv_apply]. To be safe:\n```lean\n  have hcont1 : Tendsto (fun s => kFun n s * logDeriv h s) (𝓝[≠] ρ) (𝓝 (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```\nsimpa only [logDeriv_apply] rewrites logDeriv h s → deriv h s/h s in the GOAL, turning it into the hc form ✓ safer.\n\nhcont2: Tendsto (ppart n) (𝓝[≠] ρ) (𝓝 (ppart n ρ)) := (ppart_continuousAt hρ).tendsto.mono_left nhdsWithin_le_nhds ✓.\n\nhh.deriv : AnalyticAt ℂ (deriv h) ρ — AnalyticAt.deriv ✓ (LiResidue used ha.deriv ✓). .continuousAt ✓.\n\nAlso hkd : DifferentiableAt ℂ (kFun n) ρ — kFun_differentiableAt hρ ✓.\n\nNow hexp's proof (the algebra):\n```lean\n  have hexp : ∀ᶠ s in 𝓝[≠] ρ, big = target := 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    ...\n```\nhfh.eventually_nhds : ∀ᶠ s in 𝓝 ρ, riemannZeta =ᶠ[𝓝 s] fun z => (z−ρ)^m • h z — wait hfh : riemannZeta =ᶠ[𝓝 ρ] (fun z => (z − ρ) ^ analyticOrderNatAt riemannZeta ρ • h z); hfh.eventually_nhds : ∀ᶠ s in 𝓝 ρ, riemannZeta =ᶠ[𝓝 s] (fun z => ...) ✓ (EventuallyEq.eventually_nhds : f =ᶠ[𝓝 x] g → ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g ✓).\n\nmem_nhdsWithin_of_mem_nhds : S ∈ 𝓝 x → S ∈ 𝓝[≠]... — signature: mem_nhdsWithin_of_mem_nhds (h : s ∈ 𝓝 x) : s ∈ 𝓝[t] x? hmm — vendored line 249-251: mem_nhdsWithin_of_mem_nhds h2 etc. where h2 : ∀ᶠ s in 𝓝 q, ... — so mem_nhdsWithin_of_mem_nhds takes an EVENTUAL statement in 𝓝 and gives it in 𝓝[≠]? Vendored: filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds h2, ...] with h2 : ∀ᶠ s in 𝓝 q, f =ᶠ[𝓝 s] ... — so mem_nhdsWithin_of_mem_nhds : (∀ᶠ s in 𝓝 x, p s) → (∀ᶠ s in 𝓝[t] x, p s)?? Hmm — actually 𝓝[≠] x ≤ 𝓝 x so any 𝓝-eventual is 𝓝[≠]-eventual: the lemma is probably `mem_nhdsWithin_of_mem_nhds : s ∈ 𝓝 x → s ∈ 𝓝[t] x` (set version) — but vendored applies it to ∀ᶠ- statements which ARE set memberships: (∀ᶠ s in l, p s) := {s | p s} ∈ l ✓ so mem_nhdsWithin_of_mem_nhds h2 : {s | ...} ∈ 𝓝[≠] q — i.e. ∀ᶠ s in 𝓝[≠] q, ... ✓ works for both readings ✓ copy.\n\nhh.continuousAt.eventually_ne hh0 : ∀ᶠ s in 𝓝 ρ, h s ≠ 0 ✓ (ContinuousAt.eventually_ne : ContinuousAt f x → f x ≠ 0 → ∀ᶠ y in 𝓝 x, f y ≠ 0 ✓ used in LiResidue line 82 ✓).\n\nhh.eventually_analyticAt : ∀ᶠ s in 𝓝 ρ, AnalyticAt ℂ h s ✓ (AnalyticAt.eventually_analyticAt — vendored line 245 ✓).\n\nThen inside:\n```lean\n    have hsρ' : s - ρ ≠ 0 := sub_ne_zero.mpr hsρ  -- hsρ : s ≠ ρ\n    have hld : logDeriv riemannZeta s = ((analyticOrderNatAt riemannZeta ρ : ℂ)) / (s - ρ) + logDeriv h s := by\n      have e1 : logDeriv riemannZeta s = 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 ρ) (g := h) s\n        (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```\nHmm — e1: the vendored line 254-256: `have e1 : logDeriv f s = logDeriv (fun s => (s - q) ^ analyticOrderNatAt f q * h s) s := by simp only [logDeriv_apply, hfs.deriv_eq, hfs.self_of_nhds, smul_eq_mul]` — note the mul form (not •) in e1's RHS — the simp converts • to * via smul_eq_mul ✓ copy.\n\nlogDeriv_mul after e1: logDeriv ((z−ρ)^m * h) s = logDeriv (z−ρ)^m s + logDeriv h s — vendored: logDeriv_mul (f := ...) (g := h) s (pow_ne_zero _ hsq) hhs (by fun_prop) hhas.differentiableAt — gives logDeriv (f*g) s = logDeriv f s + logDeriv g s ✓ — the function in e1 is `fun z => (z−ρ)^m * h z` — logDeriv_mul's f*g is Pi.mul — defeq ✓ (vendored passed same shape ✓).\n\nThen rw [e2] — after logDeriv_mul, goal: logDeriv (fun z => (z−ρ)^m) s + logDeriv h s = m/(s−ρ) + logDeriv h s — rw [e2] ✓ then closed by rfl? After rw the two sides become identical — rw closes by rfl ✓.\n\nWait — actually there's a subtlety: after `rw [e1, logDeriv_mul ...]`, the goal is `logDeriv (fun z => (z−ρ)^m) s + logDeriv h s = m/(s−ρ) + logDeriv h s` — then `rw [e2]` makes both sides equal ✓ auto-closed.\n\nBUT e2's proof: the trailing `simp` — what remains: logDeriv (x^m) applied at (s−ρ) times deriv (s−ρ): (m:ℂ)·(s−ρ)^{m−1}/(s−ρ)^m·1 or (m:ℂ)/((s−ρ))·1 — the vendored `simp` handled it — with what hypotheses? hsq : s − q ≠ 0 was in their context — bare simp doesn't use it... unless logDeriv_pow gives directly n/x form and deriv (s−q) = 1 via simp [deriv_sub_const, deriv_id''] — then n/(s−q)·1 = n/(s−q) ✓ mul_one by simp. So logDeriv_pow must be: logDeriv (fun x => x^n) x = (n:𝕜)/x? Hmm but that's false at x = 0 for n ≥ 1 (logDeriv (x^1) 0 = deriv(x) 0/0 = 1/0 = 0; 1/0 = 0 ✓ junk-consistent!). OK fine — copy and see.\n\nAlso fun_prop discharge for logDeriv_comp: DifferentiableAt ℂ (fun x => x^m) (s−ρ) ✓ fun_prop; DifferentiableAt ℂ (fun z => z−ρ) s ✓ fun_prop. And logDeriv_mul's (by fun_prop) : DifferentiableAt ℂ (fun z => (z−ρ)^m) s ✓.\n\nThen the final algebra block:\n```lean\n    have hA : (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =\n        -((analyticOrderNatAt riemannZeta ρ : ℂ)) * kFun n ρ := by\n      have hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl\n      rw [hmz]\n      simp only [kFun]\n      ring\n    simp only [Pi.sub_apply, Rfun, Jlag, hA]\n    rw [← logDeriv_apply, hld]\n    field_simp [hsρ']\n    ring\n```\nHmm — hmz rfl: zeroMult ρ := (analyticOrderAt riemannZeta ρ).toNat; analyticOrderNatAt riemannZeta ρ := (analyticOrderAt riemannZeta ρ).toNat — SAME ✓ rfl should work (the casts (Nat.cast) of defeq terms ✓).\n\nsimp only [Pi.sub_apply, Rfun, Jlag, hA]: goal LHS is the big expression (in s), RHS: ((Rfun n) − fun s => A-val/(s−ρ)) s. Pi.sub_apply: RHS → Rfun n s − (fun s => ...) s — also beta: (fun s => A/(s−ρ)) s — simp only [Pi.sub_apply] handles beta too? Pi.sub_apply : (f − g) x = f x − g x ✓ applies to ((Rfun n) − (fun s => ...)) s giving Rfun n s − (fun s => ...) s; the remaining beta (fun s => A/(s−ρ)) s — simp only beta-reduces automatically ✓ (simp does beta). Then Rfun unfolds via simp only [Rfun]: Rfun n s → (Jlag n − ppart n) s — hmm simp only [Rfun] rewrites Rfun → fun n => Jlag n − ppart n — then beta + Pi.sub_apply again — simp only list applies repeatedly to fixpoint ✓ include Pi.sub_apply in the same call ✓. Jlag similarly: Jlag n s → kFun n s * (−(deriv ζ s/ζ s)) ✓ (Jlag's equation). hA rewrites the A-value ✓.\n\nResult goal: −m·((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s·logDeriv h s − ppart n s\n= kFun n s * (−(deriv ζ s/ζ s)) − ppart n s − (−m·kFun n ρ)/(s−ρ)\n\nrw [← logDeriv_apply]: deriv ζ s/ζ s → logDeriv ζ s — WAIT: ← logDeriv_apply finds pattern deriv ?f ?a / ?f ?a — in the goal: deriv riemannZeta s / riemannZeta s ✓ → logDeriv riemannZeta s. Then rw [hld]: → (m:ℂ)/(s−ρ) + logDeriv h s.\n\nGoal: −m·((k s − k ρ)/(s−ρ)) − k s·logDeriv h s − ppart n s = k s·(−(m/(s−ρ) + logDeriv h s)) − ppart n s − (−m·k ρ)/(s−ρ).\nfield_simp [hsρ']: clears denominators (s−ρ) — multiplies through: LHS·(s−ρ): −m·(k s − k ρ) − k s·logDeriv h s·(s−ρ) − ppart n s·(s−ρ); RHS·(s−ρ): k s·(−(m + logDeriv h s·(s−ρ))) − ppart n s·(s−ρ) + m·k ρ — ring ✓.\n\nBut careful — field_simp might need the ppart/kFun/logDeriv terms as atoms ✓ they are opaque to field_simp ✓ fine. Also field_simp could choke if it can't find denominators — there's only /(s−ρ) ✓.\n\nOne concern: after simp only [...], is the goal's LHS exactly the hexp LHS? The hexp statement's LHS is the raw expression (not a lambda) — inside filter_upwards the goal is `rawLHS = ((Rfun n) − ...) s` ✓ simp only [Pi.sub_apply, ...] might also try to simplify LHS — Pi.sub_apply doesn't apply (no Pi apps on LHS) ✓ Rfun/Jlag don't appear on LHS ✓ hA's LHS-pattern (zeroMult ρ:ℂ)*(1−...) doesn't appear on LHS ✓.\n\nPotential issue: `simp only [Rfun]` — for a def with equation lemma: Rfun (n : ℕ) : ℂ → ℂ := Jlag n − ppart n — equation: Rfun n = Jlag n − ppart n ✓ simp only [Rfun] uses it ✓. Jlag (n) (s) : ℂ := kFun n s * (...) — equation Jlag n s = kFun n s * (...) ✓.\n\nAlso in hA — simp only [kFun]: kFun n ρ → (ρ/(ρ−1))^n − 1 ✓ then goal (m:ℂ)*(1−(ρ/(ρ−1))^n) = −(m:ℂ)*((ρ/(ρ−1))^n−1) — ring ✓.\n\nNOW — also need `ppart_continuousAt` — mirror tail_continuousAt but Icc 1 (n+1):\nActually tail_continuousAt's proof body works verbatim with Icc 1 — just change the set. Write it fresh (can't import the private proof — tail_continuousAt is a lemma in LiPrincipal with Icc 2 — I need Icc 1; write ppart_continuousAt).\n\nAlso note — Rfun_residue_at needs ρ ≠ 1 ONLY (no zero hypothesis) ✓ as analyzed (m could be 0).\n\nHmm — wait, one more subtle thing in §5: hfh's factorization has exponent analyticOrderNatAt riemannZeta ρ — fine. But hold on: AnalyticAt.analyticOrderAt_ne_top.mp gives the factorization with analyticOrderNatAt — I obtain via hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ) ✓.\n\nAnd in §4's Rfun_tendsto_one m-case — hnm : n + 1 ≤ analyticOrderNatAt (Ffun n − TaylP n) 1 via:\n```lean\n    have hnm : n + 1 ≤ analyticOrderNatAt (Ffun n - TaylP n) 1 := by\n      have h2 := Ffun_sub_TaylP_order n\n      rw [← Nat.cast_analyticOrderNatAt htop] at h2\n      exact ENat.natCast_le_natCast.mp h2\n```\nCareful: h2 : ((n+1:ℕ):ℕ∞) ≤ analyticOrderAt (Ffun n − TaylP n) 1 — wait, how exactly did I state Ffun_sub_TaylP_order? `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1`. rw [← Nat.cast_analyticOrderNatAt htop] at h2: h2 : ((n+1:ℕ):ℕ∞) ≤ ((analyticOrderNatAt (Ffun n − TaylP n) 1 : ℕ) : ℕ∞) — the rewrite replaces `analyticOrderAt (Ffun n − TaylP n) 1` with `↑(analyticOrderNatAt (Ffun n − TaylP n) 1)` ✓. Then ENat.natCast_le_natCast.mp h2 : n + 1 ≤ analyticOrderNatAt (Ffun n − TaylP n) 1 ✓. (natCast_le_natCast : (↑n ≤ ↑m) ↔ (n ≤ m) ✓ — the casts must be syntactically Nat.cast — ((n+1:ℕ):ℕ∞) is Nat.cast (n+1) ✓.)\n\nNow — the TOP-level structure also needs hgan := (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1) — used for htop-case's analyticOrderAt_eq_top.mp (no — that's for any f), the ne_top.mp (needs AnalyticAt ✓), and natCast_le... in Ffun_sub_TaylP_order (needs AnalyticAt (Ffun n − TaylP n) 1 ✓).\n\nAlso in Ffun_sub_TaylP_order: the lemma natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf : AnalyticAt 𝕜 f z₀) : ↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, ... — the f must match: goal `((n+1:ℕ):ℕ∞) ≤ analyticOrderAt (Ffun n − TaylP n) 1` — rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero hgan] — the lemma LHS `↑?n ≤ analyticOrderAt ?f ?z₀` — unify ?n := n+1, f := Ffun n − TaylP n ✓ — becomes ∀ i < n+1, iteratedDeriv i (Ffun n − TaylP n) 1 = 0 ✓ intro i hi; exact Ffun_sub_TaylP_iteratedDeriv n i (Nat.lt_succ_iff.mp hi)? — wait hi : i < n+1 — the lemma's RHS after rw: ∀ i < (n+1), ... — hmm the bound is `i < n+1` where the cast was (n+1 : ℕ) — so hi : i < n + 1 ✓ Nat.lt_succ_iff.mp hi : i ≤ n ✓.\n\nAlright — also `Nat.lt_succ_iff` ✓ exists.\n\nEdge: does `Ffun_sub_TaylP_iteratedDeriv` need i ≤ n or i < n+1 — same thing ✓.\n\nLet me now also write the iteratedDeriv_TaylP fully:\n\n```lean\nlemma iteratedDeriv_TaylP {n i : ℕ} (hi : i ≤ n) :\n    iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1 := by\n  have hterm : ∀ j ∈ Finset.range (n + 1),\n      ContDiffAt ℂ i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 :=\n    fun j _ => contDiffAt_const.mul (((contDiff_id.sub contDiff_const).pow j).contDiffAt)\n  have hdp : ∀ j : ℕ, iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) (1 : ℂ) =\n      (j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i) := by\n    intro j\n    have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ j) (1 : ℂ)) 1\n    rw [iteratedDeriv_pow] at e\n    simpa using e\n  show iteratedDeriv i (fun w : ℂ => ∑ j ∈ Finset.range (n + 1),\n      (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 = _\n  rw [iteratedDeriv_sum hterm]\n  -- pointwise: iteratedDeriv i (c_j·(w−1)^j) 1 = c_j * descFac_j\n  have hpoint : ∀ j ∈ Finset.range (n + 1),\n      iteratedDeriv i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 =\n        (iteratedDeriv j (Ffun n) 1 / j !) * ((j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i)) := by\n    intro j hj\n    rw [iteratedDeriv_const_mul _ (((contDiff_id.sub contDiff_const).pow j).contDiffAt), hdp j]\n  rw [Finset.sum_congr rfl hpoint]\n  rw [Finset.sum_eq_single i]\n  · -- j = i term\n    have hfi : ((i ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero i)\n    rw [Nat.descFactorial_self]\n    simp only [Nat.sub_self, pow_zero, mul_one]\n    field_simp [hfi]  -- hmm goal: D/i! * i! = D — wait the (i ! : ℂ) cast placement\n  · -- j ≠ i terms vanish\n    intro j hj hji\n    rw [Finset.mem_range] at hj\n    by_cases hlt : j < i\n    · have h0 : (j.descFactorial i : ℂ) = 0 := by\n        have h := Nat.descFactorial_eq_zero_iff_lt.mpr hlt\n        exact_mod_cast h  -- or simp [h]\n      rw [h0]; simp\n    · have h0 : (0 : ℂ) ^ (j - i) = 0 := zero_pow (by omega)\n      rw [h0]; simp\n  · -- i ∈ range(n+1)\n    intro hi'\n    rw [Finset.mem_range] at hi'\n    omega\n```\nIssues:\n- `show iteratedDeriv i (fun w => ∑ ...) 1 = _` — the TaylP n def unfolds — `show` with defeq ✓.\n- iteratedDeriv_sum hterm: signature (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) : iteratedDeriv n (fun x => ∑ i ∈ I, f i x) x = ∑ i ∈ I, iteratedDeriv n (f i) x — my lambda matches fun w => ∑ j ∈ range, (term j) w ✓. But wait — is the LHS form `iteratedDeriv n (∑ i ∈ I, f i) x` (Pi sum)? Line 509 IteratedDeriv/Lemmas.lean: `lemma iteratedDeriv_sum (hf : ∀ i ∈ I, ContDiffAt 𝕜 n (f i) x) :` — unknown body form. If it's the Pi.sum form (∑ i ∈ I, f i as function sum), I need the funext bridge like Gprim. I'll include the bridge preemptively? The `show` I wrote targets the lambda-sum form. If iteratedDeriv_sum wants Pi.sum — mismatch → error → then add the rw [show lambda = ∑ f j from funext...]. I'll write with the bridge to be safe:\n\n```lean\n  rw [show (fun w : ℂ => ∑ j ∈ Finset.range (n + 1),\n      (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) =\n    ∑ j ∈ Finset.range (n + 1),\n      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) from by\n    funext w; simp [Finset.sum_apply]]\n```\nhmm but if iteratedDeriv_sum's LHS is the lambda form, this rw makes the goal Pi.sum form and then iteratedDeriv_sum fails to match... CONFLICT. Let me actually CHECK iteratedDeriv_sum's statement before writing. I'll grep it when writing. Same for deriv_sum in LiPrincipal — deriv_Gprim used `rw [deriv_sum (fun i hi => ?_)]` after the funext-to-Pi.sum bridge (line 195-201) — so deriv_sum wants Pi form: `deriv (∑ i ∈ s, f i) x = ∑ i ∈ s, deriv (f i) x`? deriv_Gprim bridged the lambda to Pi-sum THEN applied deriv_sum — so deriv_sum's LHS is `deriv (∑ i ∈ s, f i) x`?? Hmm wait, deriv_Gprim line 195: rw [show (lambda-sum) = ∑ i, (lambda i)] then `rw [deriv_sum ...]` — so deriv_sum's LHS must be deriv (fun x => ∑ i ∈ s, f i x)? No — if they first converted TO the Pi-sum form ∑ i ∈ s, (fun w => ...) and then deriv_sum matched, deriv_sum's LHS is `deriv (∑ i ∈ s, f i) x` (Pi.sum). Hmm — actually wait: in deriv_Gprim the bridge converts the raw lambda to `∑ i ∈ Finset.Icc 2 (n + 1), (fun w : ℂ => ...)` — Finset.sum of functions — then deriv_sum rewrites. Hmm, but actually maybe deriv_sum's statement is `deriv (fun x => ∑ i ∈ s, f i x) x = ∑ i ∈ s, deriv (f i) x`? If so, the bridge to Pi-sum form would MISMATCH (the goal would be deriv (∑ i, f i) x with a Pi.sum — but fun x => ∑ i, f i x is DEFEQ to ∑ i, f i — rw needs SYNTACTIC match up to reducible defeq — Finset.sum_apply is simp-normal... the bridge they used suggests deriv_sum wants the Pi form). Conclusion: check iteratedDeriv_sum's actual statement when compiling; likely same convention as deriv_sum (Pi form). I'll include the Pi bridge (matching deriv_Gprim's proven pattern).\n\n- `iteratedDeriv_const_mul _ (...)`: signature iteratedDeriv_const_mul {n} {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (fun y => c * f y) x = c * iteratedDeriv n f x — hmm actually let me double-check: line 368: theorem iteratedDeriv_const_mul {n : ℕ} {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (fun x => c * f x) x = c * iteratedDeriv n f x — I think that's the shape (𝔸 a normed algebra — c : 𝔸 — for 𝔸 = ℂ ✓). ✓ usage: iteratedDeriv_const_mul (c_j) (ContDiffAt-of-(w−1)^j) : iteratedDeriv i (fun w => c_j * (w−1)^j) 1 = c_j * iteratedDeriv i (fun w => (w−1)^j) 1 ✓.\n\n- The cast in hfi: the denominator `j !` in TaylP — how does it elaborate? In lcoeff (LiResidue:147): `iteratedDeriv (k + 1) hLi 1 / (k + 1)!` — (k+1)! with open scoped Nat is Nat.factorial (k+1) : ℕ, and the / with ℂ LHS: HDiv ℂ ℕ ? — hmm there IS `instHDiv ℂ ℕ ℂ`? I don't think so... Actually maybe (k+1)! elaborates directly AT ℂ: `Nat.factorial` has type ℕ → ℕ only. `(k + 1)!` — the `!` postfix with open scoped Nat: `n !` := Nat.factorial n. For it to be ℂ, Lean would need factorial defined at ℂ — no. So there must be a coercion: Lean inserts ↑ when unifying ℕ with ℂ in HDiv — HDiv ℂ ?m ℂ with ?m := ℕ: is there an instance HDiv ℂ ℕ ℂ? There's `instHDiv` via `Div ℂ` only for ℂ/ℂ... BUT Lean 4 Mathlib has the `binarith` elaboration: a / b with a : ℂ, b : ℕ — unification fails, then Lean tries coercion: b lifted via Nat.cast — HDiv ℂ ℂ ℂ ✓. This is standard (x / n works in Mathlib with n : ℕ via the `Nat.cast` insertion in binop elaboration). Since lcoeff compiled, `/ (k+1)!` works ✓. So in TaylP, `/ j !` similarly = / ↑(j!) — hfi : ((Nat.factorial j : ℕ) : ℂ)... I'll write the denominator in TaylP as `iteratedDeriv j (Ffun n) 1 / (j ! : ℂ)` — hmm (j ! : ℂ) ascribes the factorial expr AT ℂ — but Nat.factorial j : ℕ can't be ascribed ℂ... `(j ! : ℂ)` — elaborates j ! with expected type ℂ: Nat.factorial j : ℕ ≠ ℂ — coercion inserted: ↑(j!) ✓ works (this is the standard `(n : ℂ)` style). OK — use `/ (j ! : ℂ)`? Hmm wait — but in lcoeff it's `/ (k + 1)!` with NO ascription and it compiled — meaning the binop elaborator handled it. To minimize variance from proven code, mirror lcoeff exactly: `/ j !` with open scoped Nat ✓. Then hfi about ↑(i !): after descFactorial_self rewrite, the term is `(iteratedDeriv i (Ffun n) 1 / i !) * ((i ! : ℂ) * 1)` — hmm the descFactorial's cast: hdp gives (j.descFactorial i : ℂ) — with explicit ascription in MY hdp statement ✓ I control it: (j.descFactorial i : ℂ) ✓. After rw [Nat.descFactorial_self]: (↑(i!) : ℂ)... Nat.descFactorial_self : i.descFactorial i = i ! — rewriting inside the cast ✓. Then simp only [Nat.sub_self, pow_zero, mul_one]: (0:ℂ)^(i−i) → (0:ℂ)^0 → 1, ·*1 → ·. Term: (iteratedDeriv i (Ffun n) 1 / i !) * (i ! : ℂ) — hmm the i ! in the denominator — same elaboration ascription: / i ! = / ↑(i!) ✓ and the second factor (↑(i!)): field_simp with hfi : (↑(i!) : ℂ) ≠ 0 — closes D/↑(i!) * ↑(i!) = D? field_simp proves it (clears to D·↑(i!) = D·↑(i!)) ✓. Alternatively exact div_mul_cancel₀ ... Let me use `field_simp [hfi]`; if that leaves junk, `exact div_mul_cancel₀ _ hfi` — div_mul_cancel₀ (a) (h : b ≠ 0) : a / b * b = a — a := iteratedDeriv i (Ffun n) 1, b := ↑(i!) — the goal D / ↑(i!) * ↑(i!) = D — exact div_mul_cancel₀ _ hfi ✓ (b implicit inferred from h? h : ↑(i!) ≠ 0 — b := ↑(i!) ✓). Use this directly — cleaner than field_simp. Hmm — is it div_mul_cancel₀ or div_mul_cancel_of_invertible... In current Mathlib: `div_mul_cancel₀ (a : G₀) (h : b ≠ 0) : a / b * b = a`? I recall `div_mul_cancel₀` indeed exists (GroupWithZero). Fallback options at compile time.\n\nAlso the two `rw [h0]; simp` closers: after rw [h0]: term = c_j * (0 * (0:ℂ)^{j−i}) or c_j * (descFac * 0): simp closes via zero_mul/mul_zero ✓ goal is `... = 0` ✓ simp [h0] would also work — write `simp [h0]`.\n\nWait — the term in the sum after hpoint rewrite: the sum is Σ j ∈ range(n+1), (c_j) * ((j.descFactorial i : ℂ) * (0:ℂ)^(j−i)) — sum_eq_single i's side-goals: ∀ j ∈ range, j ≠ i → term j = 0 ✓ as written.\n\nAlso — hmm, `Finset.sum_congr rfl hpoint` rewrites the sum's summand — but rw [Finset.sum_congr rfl hpoint]?? Finset.sum_congr is a congruence lemma producing an equality — rw with it: rw [Finset.sum_congr rfl hpoint] — hmm, that tries to rewrite with the equation Σ f = Σ g — as a rewrite rule it replaces the sum — should work: the equation's LHS pattern is the original sum ✓. Actually cleaner: `rw [Finset.sum_congr rfl hpoint]` — hmm, rw with a term of type (s = t) rewrites s → t ✓ fine.\n\nAlternatively `trans` — skip, rw is fine.\n\nNow — one more thing to double-check: `iteratedDeriv_comp_sub_const` exact signature — from LiResidue A_iter line 173: `congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1` — so iteratedDeriv_comp_sub_const (i : ℕ) (f : ℂ → ℂ) (c : ℂ) : iteratedDeriv i (f ∘ (· − c)) = fun x => iteratedDeriv i f (x − c)? and congr_fun ... 1 : iteratedDeriv i (f ∘ (·−1)) 1 = iteratedDeriv i f (1−1) — then the goal's `iteratedDeriv i (fun w => (w−1)^j) 1` — is `fun w => (w−1)^j` syntactically `(fun w => w^j) ∘ (fun w => w−1)`? A_iter's simpa handled this defeq ✓ copy the pattern (simpa using e).\n\nBut note — in A_iter, the goal had `(n.descFactorial i : ℂ)` cast: statement `n.descFactorial i * (0 : ℂ) ^ (n - i)` — with (n.descFactorial i : ℂ)? A_iter's statement: `iteratedDeriv i (fun w : ℂ => (w - 1) ^ n) 1 = n.descFactorial i * (0 : ℂ) ^ (n - i)` — the n.descFactorial i : ℕ cast to ℂ by the multiplication with ℂ — binop coercion ✓. My hdp: `(j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i)` — explicit ✓.\n\niteratedDeriv_pow : iteratedDeriv i (fun w => w^n) x = (n.descFactorial i : ℂ)·x^(n−i)? — its statement: iteratedDeriv_pow {n i : ℕ} : iteratedDeriv i (fun x => x^n) x = n.descFactorial i * x^(n−i) ✓ roughly. e after congr_fun: iteratedDeriv i ((fun w => w^j) ∘ (fun w => w−1)) 1 = iteratedDeriv i (fun w => w^j) (1−1)?? hmm — actually iteratedDeriv_comp_sub_const i f (1:ℂ) : probably iteratedDeriv k (fun x => f (x − c)) x = iteratedDeriv k f (x − c) — as a FUNCTION equality (congr_fun applied ✓). So e : iteratedDeriv i (fun w => (w−1)^j)... wait f := fun w => w^j — f ∘ (·−1) = fun w => (w−1)^j ✓ defeq — e : iteratedDeriv i (f ∘ (·−1)) 1 = iteratedDeriv i f (1 − 1) — rw [iteratedDeriv_pow] at e: e : iteratedDeriv i (f ∘ (·−1)) 1 = j.descFactorial i * (1−1)^{j−i} — simpa using e: simp turns 1−1 → 0 and the LHS comp-form → the lambda form, goal's cast handled ✓ copy A_iter's simpa.\n\nOK. Also `Nat.descFactorial_eq_zero_iff_lt` — verify name at compile; alternative `Nat.descFactorial_eq_zero_iff_lt` — I'm fairly sure ✓ (used commonly). If missing: prove j.descFactorial i = 0 from j < i by... there's `Nat.descFactorial_of_lt`? hmm: `Nat.descFactorial_eq_zero_iff_lt : n.descFactorial i = 0 ↔ n < i` ✓ I'll trust it.\n\nNow — file header + the main theorem. Also update the package root import. Let me check the root file.","signature":""},{"type":"text","text":"All names verified. Now let me check the package root file, then write `LiSides.lean`."},{"type":"tool_use","id":"Read_28","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1.lean"},"extra_content":null},{"type":"tool_use","id":"Bash_29","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && sed -n '505,515p' Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean && sed -n '364,380p' Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean","description":"Check iteratedDeriv_sum and const_mul exact statements"},"extra_content":null}]