I've made some stylistic comments, I will have a proper look tomorrow.

Second round.

I agree that you should split the theorem in two version (you can still have a iff version if you want). For the t2_space → .. direction t2_space should obviously be an instance.

Third round, I think we are getting close

Some more suggestions.

I am always happy to see new people contribute to the analysis part of mathlib.

Congratulations for your first PR! 🎉

I don't have a lot to add about the "technicalities of Lean" side, your code looks really good, so I added suggestions on how to use the existing API more efficiently. You don't have to adopt all of them, but I think this is a great way to get familiar with Mathlib so I wanted to at least explain how to make your life easier.

Basically, the key mathematical point that can make your life easier is that spaces satisfying with_seminorms are topological groups, and we have a ton of general facts about topological groups in mathlib. Most interesting for you is the fact that a topological group is T2 if and only if {0} is closed, and you can probably see why this makes things much easier!

Note: Unfortunately, we don't have the lemma saying that with_seminorms imply topological_add_group yet, but you should add it. I used the following in my suggestions:

lemma with_seminorms.topological_add_group (hp : with_seminorms p) : topological_add_group E :=
begin
  rw hp.with_seminorms_eq,
  exact add_group_filter_basis.is_topological_add_group _
end

I think this looks very good, but now we might want to change everything from t1 to t2.