Mathlib.Algebra.Homology.Embedding.Boundary

Stream: mathlib4

[Sophie Morel]

In Mathlib.Algebra.Homology.Embedding.Boundary, the last two lemmas, ComplexShape.boundaryGE_embeddingUpIntGE_iff and ComplexShape.boundaryLE_embeddingUpIntLE_iff, seem to say the same thing.
I think the second one should be saying instead:

(embeddingUpIntLE p).BoundaryLE n ↔ n = 0

Pinging @Joël Riou , who authored that file.

[Joël Riou]

Thanks! This is fixed in #25673.