[{"type":"thinking","thinking":"Key facts:\n\n1. Line 668: `namespace intervalIntegral` — so all are `intervalIntegral.*` ✓.\n\n2. Line 911-913: `section Comp` with `variable {a b c d : ℝ} (f : ℝ → E)` — so `intervalIntegral.integral_comp_neg (f : ℝ → E) : ∫ x in a..b, f (-x) = ∫ x in -b..-a, f x` with a, b implicit. Usage: `intervalIntegral.integral_comp_neg g` — or with implicit a b unified by expected type. Since a, b are implicit and f explicit: `intervalIntegral.integral_comp_neg (fun t => ‖Jlag n _‖)` gives `∫ x in ?a..?b, f (-x) = ∫ x in -?b..-?a, f x` with ?a ?b unified from the goal. Should work with `rw` or `exact`.\n\nCareful with the integral_comp_neg rewrite: my goal after hsplit: `∫ t in (-T)..(-10), g t`. I transform to `∫ t in (-T)..(-10), g (-t)` via integral_congr (needs EqOn g (fun t => g (-t)) [[-T, -10]]). Hmm wait — direction: integral_congr (h : EqOn f g [[a,b]]) : ∫ f = ∫ g. So with f := g, g := fun t => g(-t): need EqOn g (fun t => g (-t)) [[-T,-10]] — i.e. ∀ t ∈ uIcc, g t = g(-t) ✓ from hge.\n\nThen goal becomes ∫ t in (-T)..(-10), (fun u => g (-u)) t — hmm, will `intervalIntegral.integral_congr` produce that beta-redex? The h's RHS is `fun t => g (-t)`; after rw/exact the integral's integrand is that lambda applied to the bound variable — displayed as `∫ t in -T..-10, g (-t)`. Then `intervalIntegral.integral_comp_neg (f := fun t => g t)`... hmm f is explicit. `integral_comp_neg g : ∫ x in ?a..?b, g (-x) = ∫ x in -?b..-?a, g x`. The LHS `∫ x in -T..-10, g (-x)` matches with ?a := -T, ?b := -10 ✓. So:\n\n```lean\nhave hleft : ∫ t in (-T)..(-10:ℝ), g t = ∫ t in (10:ℝ)..T, g t := by\n  have h1 : ∫ t in (-T)..(-10:ℝ), g t = ∫ t in (-T)..(-10:ℝ), g (-t) :=\n    intervalIntegral.integral_congr (fun t _ => hge t)\n  rw [h1, intervalIntegral.integral_comp_neg g]\n  -- goal: ∫ t in -(-10)..-(-T), g t = ∫ t in 10..T, g t\n  norm_num1  -- -(-10) = 10, -(-T) = T?? -(-T) needs neg_neg\n```\n\nHmm, `-(-10 : ℝ)` — neg_neg (10) simp; `-(-T)` — neg_neg T. `simp only [neg_neg]` closes both. Then rfl. So:\n\n```lean\n  rw [h1, intervalIntegral.integral_comp_neg g]\n  simp only [neg_neg]\n```\n\nAfter this the goal should be `∫ t in 10..T, g t = ∫ t in 10..T, g t` closed by rfl automatically after simp? simp only [neg_neg] closes rfl goals ✓.\n\nWait, but `rw [intervalIntegral.integral_comp_neg g]` — rewrite with an equation whose LHS has ?a ?b implicit metavars: rw unifies `∫ x in ?a..?b, g (-x)` against the goal `∫ t in -T..-10, g (-t)` ✓ instantiates ?a := -T, ?b := -10, replaces with `∫ x in -(-10)..-(-T), g x` ✓.\n\n3. Line 1421: `variable (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b)` in section Mono (1403), inside the section at 1283 with `{f g : ℝ → ℝ}` — f g are REAL-valued ✓ (my g is ℝ-valued ✓). So `intervalIntegral.integral_mono_on (hab) (hf) (hg) (h)` — argument order: hab, hf, hg, then h. Let me verify by reading lines 1421-1449.\n\nAlso from line 1421's context I should confirm the exact conclusion statement — grep showed:\n\n```\n1432:theorem integral_mono_on (h : ∀ x ∈ Icc a b, f x ≤ g x) :\n1433:    (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ:= by\n```\n\nSo full signature: `intervalIntegral.integral_mono_on (hab : a ≤ b) (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) (h : ∀ x ∈ Icc a b, f x ≤ g x)`. ✓ as I originally assumed.\n\nLet me also confirm `norm_le_insert`, `mul_le_mul`, `one_div_le_one_div_of_le`, `Complex.abs_re_le_norm`, `norm_natCast`, `Real.le_log_iff_exp_le`, `Real.exp_one_lt_d9`, `abs_of_nonneg`, `abs_of_neg`, `Finset.mul_sum`, `norm_sum_le`, `Real.le_sqrt`, `div_eq_mul_one_div`, `mul_le_mul_of_nonneg_left`, `Real.log_nonneg`, `Continuous.norm`, `ContinuousAt.comp`, `continuous_iff_continuousAt`.\n\nLet me grep these quickly in Mathlib.","signature":""},{"type":"text","text":"Section variables confirmed. Let me verify the exact signature of `integral_mono_on` and the other general lemmas."},{"type":"tool_use","id":"Bash_16","name":"Bash","input":{"command":"sed -n '1403,1449p' \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean\"","description":"Read Mono section of IntervalIntegral Basic.lean"},"extra_content":null}]