nightly#38 adaptations for nightly-2025-08-18

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-08-18 nightly#38 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kim Morrison]

LGTM, although I don't see how the proof in Mathlib/LinearAlgebra/Quotient/Basic.lean was ever working before adding that line...?

Does anyone else want to review this?

[Robin Arnez]

Context:

   | succ k ih =>
     simp only [Module.End.iterate_succ]
     rw [mapQ_comp, ih]
+    exact p.le_comap_pow_of_le_comap h k

Previously

ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) ⋯), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

so the ih in the rw actually elaborated to ih (evaluate optParam), thus inserting what now needs to be specified explicitly.