Redundant TODO's in files?

Stream: mathlib4

[Dion Leijnse]

While looking through the Algebraic Geometry files in mathlib, I saw that some of them have some TODO's on top. For example, on top of Mathlib.AlgebraicGeometry.Morphisms.Affine is a TODO to prove that affine morphisms are separated. However, it looks to me that this has already been done in AlgebraicGeometry.IsSeparated.of_isAffineHom in https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Morphisms/Separated.html#AlgebraicGeometry.IsSeparated.of_isAffineHom. Is this true or am I missing something? And if so, can this TODO be removed? I found something similar in Mathlib.AlgebraicGeometry.Morphisms.Finite for showing that a finite morphism is proper.

[Christian Merten]

Yes these TODOs can be removed, please feel free to open a PR removing them.

[Dion Leijnse]

Thanks, I'll make a pull request once I have write access to the Github