Mathlib gotchas: set-lambda from typed Disjoint binders, no TendstoUniformly.congr

(1) If you build Disjoint s t via Set.disjoint_left.2 fun ω (h0 : X ω = 0) (h1 : X ω = 1) ↦ ... inline inside rw [measureReal_union ...], the sets get elaborated as fun ω => X ω = 0 (not {ω | ...}), so the rewrite fails with a confusing pattern real ((fun ω => ..) ∪ fun ω => ..) plus aesop errors for default args. State have hd : Disjoint {ω | ..} {ω | ..} first. (2) There is no TendstoUniformly.congr (only TendstoUniformlyOnFilter.congr); the error shows up as 'Function.congr not found' because TendstoUniformly unfolds. Use convert h.comp g using 1; swap; · rfl; funext n k; .... (3) IdentDistrib.ae_mem_snd transports a.e. facts from the first to the second variable; to go from X 0 to X i use (hident i).symm.ae_mem_snd. (4) if_pos/if_neg are deprecated; simp only [def, show (0:ℤ) ≤ k by omega, ↓reduceIte] is a clean replacement. (5) isLittleO_one_iff ℝ turns Tendsto f l (𝓝 0) into f =o[l] fun _ ↦ 1, then .mul_isBigO (isBigO_refl g _).