[{"type":"thinking","thinking":"Not there either. Where is `Summable.tsum_add` declared?! Let me just ask Lean: write a tiny probe file with `#check @Summable.tsum_add` and `#check @tsum_neg` etc. That's definitive. Quick foreground lean run on the Scratch file.","signature":""},{"type":"text","text":"Let me just ask Lean directly with a probe file."},{"type":"tool_use","id":"Write_109","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean","content":"import Mathlib\n\n#check @Summable.tsum_add\n#check @Summable.tsum_sub\n#check @tsum_neg\n#check @tsum_zero\n#check @tsum_congr\n#check @tsum_mul_left\n#check @Equiv.tsum_eq\n#check @Equiv.summable_iff\n#check @div_le_div_of_nonneg_right\n#check @Complex.norm_conj\n#check @starRingEnd_apply\n#check @norm_star\n#check @one_div_mul_one_div\n#check @mul_one_div\n#check @inv_le_inv₀\n#check @one_div_le_one_div_of_le\n#check @eventually_nhdsWithin_iff\n#check @iteratedDeriv_neg\n#check @Filter.EventuallyEq.of_eq\n#check @eq_zero_of_neg_eq\n#check @summable_of_hasFiniteSupport\n#check @inv_eq_of_mul_eq_one_right\n#check @Complex.add_conj\n#check @AnalyticAt.contDiffAt\n#check @contDiff_const\n#check @iteratedDerivWithin_tsum\n#check @SummableLocallyUniformlyOn_of_locally_bounded\n#check @Complex.Gammaℝ_eq_zero_iff\n#check @zpow_neg\n#check @zpow_natCast\n#check @neg_pow\n#check @mul_inv\n#check @pow_mul\n#check @sub_sq\n#check @div_pow\n#check @iteratedDeriv_const\n#check @iteratedDerivWithin_neg\n#check @inv_pow\n"},"extra_content":null}]