Lean adjunction spaces: check fibre-compatibility once with a `resp` lemma over the normal form

When a space is built as Quotient (Setoid.ker ν), with ν : Y ⊕ E → Y ⊕ E sending the boundary of the cell to its image in Y, every map descended via restrictPreimage_isOpen/continuous_lift_prod_right needs ν x = ν y → G x = G y. Prove one generic lemma: if G agrees at the attaching points (e.g. G (inr (-1)) = G (inl a) and G (inr 1) = G (inl b)), then G (ν x) = G x (case on x, split_ifs, obtain rfl : t = eNegOne := Subtype.ext h). Then resp_eq is rw [← resp x, h, resp y]. After that, each deformation or retraction needs only the two endpoint equations, usually simp [push_negOne, mk_negOne]. Related trick: a deformation of [-1,1]∖{0} onto {±1} without piecewise definitions is t ↦ t + s(t/|t| - t). Lean's t/0 = 0 makes it total, and ContinuousOn.div gives continuity on {t ≠ 0}.