As the main technical tool to do so, we introduce a new definition `PartialHomeomorph.lift_openEmbedding`, lifting a PartialHomeomorph under an `OpenEmbedding`. (The left or right inclusion into a disjoint union are open embeddings; this abstract allows proving lemmas only once, and avoids having to deal with subtypes.)

From the bordism theory project branch: future steps include proving that the disjoint union of `C^n` manifolds is a `C^n` manifold.

* origin/master: (88 commits)
  chore(scripts): update nolints.json (#20672)
  chore: de-simp `map_eq_zero_iff_eq_one` (#20662)
  feat(Combinatorics/SimpleGraph): add independent sets (#18608)
  chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641)
  feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366)
  feat(AlgebraicTopology): model categories (#19158)
  chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548)
  feat(Data/List/ReduceOption): add replicate theorems (#20644)
  feat: approximate subgroups (#20050)
  feat: use scoped trace nodes in linarith (#19855)
  feat: disjoint union of charted spaces (#20619)
  feat: add some term elaborators for reduction (#15192)
  feat(Topology/Category): category of delta-generated spaces (#19499)
  add a variable_alias for Quantale and AddQuantale (#19282)
  feat(Computability/DFA): implement `isRegular_iff` (#19940)
  chore: unpin and bump batteries and importgraph (#20651)
  chore: split `Mathlib/Algebra/Group/Int` (#20624)
  feat: three lemmas related to Hausdorff distance (#20585)
  chore: `initialize_simps_projections` for `Submodule` (#20582)
  feat(Order): Boolean algebra structure on idempotents (#20618)
  chore(CategoryTheory): moving/renaming Subpresheaf (#20583)
  refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630)
  feat: sets of doubling strictly less than 3/2 (#20572)
  chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452)
  feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298)
  feat: product of subalgebras (#20202)
  feat: `Submodule.restrictScalars` commutes with `pow` (#20581)
  feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580)
  chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576)
  chore: use ofNat more (#20546)
  feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363)
  feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797)
  refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590)
  feat: Make `PNat.recOn` induction eliminator (#20617)
  feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608)
  feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574)
  feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573)
  chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611)
  feat: AbsoluteValue.IsNontrivial (#20588)
  chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092)
  chore(Data/Set): split the `CoeSort` instance to its own file (#19031)
  feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612)
  feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286)
  chore: cleanup more `erw` (#20601)
  chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587)
  chore: cleanup imports in PrimePow/Divisors (#20626)
  chore: split Algebra/BigOperators/Group/List (#20625)
  chore: reduce Topology->Order imports by moving content (#20627)
  chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592)
  refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333)
  ...