# Zulip Chat Archive

## Stream: maths

### Topic: complex.ext_iff a simp lemma?

#### Kevin Buzzard (May 28 2020 at 14:05):

Should complex.ext_iff be a simp lemma? In `data.complex.basic`

I added the attribute to it, and the following happened: two proofs broke, but they were easily fixed (one became shorter), and about 20 proofs could be changed from `ext_iff.2 $ by simp`

to `by simp`

. I then tried compiling the rest of mathlib and a bunch of stuff had broken. I cannot currently contemplate fixing it, but I was just interested in hearing the community's ideas about whether this is a bad idea in general. The lemma says `z = w ↔ z.re = w.re ∧ z.im = w.im`

. In the complex number game it seems to work fine.

#### Scott Morrison (May 28 2020 at 14:06):

Doesn't sound like a good idea to me. You won't ever be able to reason about equality of complex numbers without having the argue separately about their real and imaginary parts...

#### Scott Morrison (May 28 2020 at 14:07):

When you're first setting up complex numbers in terms of pairs of real numbers, it's great and helpful. Less so once you want to seal off that implementation detail! :-)

#### Sebastien Gouezel (May 28 2020 at 14:08):

Instead, you could use `local attribute [simp] ext_iff`

just in this file.

#### Kevin Buzzard (May 28 2020 at 14:11):

I think that making it a local attribute is a great idea, because it really makes `data.complex.basic`

look a lot sexier.

#### Scott Morrison (May 28 2020 at 14:13):

There's a slight counter argument: that having _all_ the proofs in a good introductory pedagogical file consist of `by simp`

may induce superstition about the power of `simp`

. :-)

#### Scott Morrison (May 28 2020 at 14:13):

At least `by { ext; simp }`

may lead people to understand: "think about it in components; then it's easy".

#### Kevin Buzzard (May 28 2020 at 14:19):

That's an interesting counter-argument.

#### Kevin Buzzard (May 28 2020 at 14:22):

So I see that there is no module docstring either, and the doc_blame linter is actually complaining a lot, so at some point when marking is over in a few days I will probably fix this up; to be quite honest I even prefer `by {ext; simp}`

to what we currently have, but I am looking at this from a different point of view to some people, perhaps (for all I know I just put compilation time up by 20% which might be a cardinal sin)

#### Kevin Buzzard (May 28 2020 at 14:25):

https://github.com/leanprover-community/mathlib/tree/complex-tidyup ; I won't make a PR until I've added the module docstrong (and won't make a PR of this edit at all if people think that `ext_iff.2 $ by simp`

is better). In the complex number game I'll perhaps play with the idea when I'm streaming live

#### Reid Barton (May 28 2020 at 14:29):

On a somewhat related note, I wonder whether `ext`

should only locally be an `ext`

lemma.

#### Reid Barton (May 28 2020 at 14:31):

If you have two, I don't know, bundled holomorphic functions and you want to prove they're equal because they're pointwise equal, probably you do not want to split into real and imaginary components.

Last updated: May 18 2021 at 06:15 UTC