Kollár's Theorem 100 at s = 1: the tautological instances

[Kol07, Theorem 100] (tuning of ideals) says that for m = max-ord I, an integer s ≥ 1 and an ideal sheaf J with I^s ⊆ J ⊆ W_{ms}(I), a smooth blow-up sequence is of order ≥ m for (I, m) exactly when it is of order ≥ ms for (J, ms); the library proves it as Hironaka.Sequence.tuning_iff. This file checks the two instances with s = 1: J = I gives the tautology (I, m) ↔ (I, m), and J = W_m(I) gives "order ≥ m for (I, m) iff order ≥ m for (W_m(I), m)". The hypothesis I ⊆ J ⊆ W_m(I) holds in both cases because I ⊆ W_m(I) (pow_le_W at the exponent 1), and the marks are m · 1 = m. Everything is checked as examples; nothing is exported.