Schroder-Bernstein theorem in MIL

Stream: new members

[Vivek Rajesh Joshi]

I don't understand how the Schroder-Bernstein theorem has been proved in the Mathematics in Lean textbook. I'll post the picture here.
image.png
image.png
My problem is with that second last sentence. If we can say that all those shaded rings are in bijection with each other, why should alpha be in bijection with the image of g?