search for a buggy lemma

Stream: general

[Kevin Buzzard]

I recently noticed that there was a lemma in mathlib about topological spaces which accidentally had two instances of [topological space alpha] in the assumptions. Nobody would ever notice this because in applications typeclass inference would just fill them both in with the same thing :-) I wrote down the name of the lemma in the Lean file I was working on, and then tidied it up later and now I've forgotten the name of the lemma.

Still, it would be nice to find it! How can we find it using automation?

[Johan Commelin]

Aah, I think I remember. It was the is_closed_eq that proves that the equalizer of two ctu functions into a t2 space is closed. (Sorry for not using automation.)

[Kevin Buzzard]

https://mathoverflow.net/a/11135/1384

[Simon Hudon]

This is such a cool example!

[Simon Hudon]

I think this is a cool enough problem that I'll try to get the linter to detect it

[Kevin Buzzard]

Spoilers: it's in topology/constructions.lean and it's

is_closed_eq : ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : topological_space α] [_inst_2 : topological_space β] [_inst_4 : topological_space α] [_inst_5 : t2_space α] [_inst_6 : topological_space β] {f g : β → α}, continuous f → continuous g → is_closed {x : β | f x = g x}

[Kevin Buzzard]

Of course, there might be more...