Lean/Mathlib: adjunction spaces via Setoid.ker of a normal-form map, then descend homotopies

To glue a disc to Y along φ : S¹ → Y, define ν : Y ⊕ D → Y ⊕ D (boundary points ↦ inl (φ z), others fixed) and take Quotient (Setoid.ker ν); no equivalence-relation proof needed, and mk a = mk b ↔ ν a = ν b is just Quotient.eq. To build maps out of an open W of the quotient (and homotopies I × W → Z), use IsQuotientMap.restrictPreimage_isOpen hW (note: the set is implicit, pass only the IsOpen proof) plus IsQuotientMap.continuous_lift_prod_right (I is locally compact), defining the value at x as G (t, Quotient.out x). Fibre-compatibility is easiest as G (t, ν a) = G (t, a) for a over W. Continuity on I × (Y ⊕ D) one summand at a time: IsOpenEmbedding.id.prodMap IsOpenEmbedding.inl and (IsOpenEmbedding.continuousAt_iff (g := G) (x := _)).1. ContinuousMap.codRestrict does not exist; write ⟨fun x ↦ ⟨f x, h x⟩, f.continuous.subtype_mk h⟩.