# Zulip Chat Archive

## Stream: maths

### Topic: linear_isometry_complex

#### François Sunatori (Mar 14 2021 at 20:12):

Hi,

I've been working on proving the following lemma since last week:

```
import analysis.complex.basic
open complex
local notation `|` x `|` := complex.abs x
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z)) :=
begin
sorry
end
```

I proved another helper lemma:

```
lemma linear_isometry_complex' (z : ℂ) (h : ℂ →ₗᵢ[ℝ] ℂ) :
h 0 = 0 → h 1 = 1 → ((h z = z) ∨ (h z = conj z)) :=
begin
...
end
```

I would now like to use the helper lemma `linear_isometry_complex'`

in my proof of `linear_isometry_complex`

and am uncertain how to go at this.

Since `linear_isometry_complex`

has a `∃ a : ℂ, |a| = 1`

, I wanted to use:

```
use exp ^ I * θ
```

and I need to define a function, say `h`

that will fit the hypotheses of `linear_isometry_complex'`

:

`h 0 = 0`

and `h 1 = 1`

for `h 0 = 0`

I can use `linear_isometry.map_zero`

, but I get stuck with the definition of `h`

because I would need to take in `θ`

as an argument.

I'm wondering if I'm going in a good direction here or if there is a way to define this `h`

function without using `exp ^ I * θ`

.

#### Heather Macbeth (Mar 14 2021 at 20:20):

How about defining `a := f 1`

and then letting `h`

be `a⁻¹ • f`

, (i.e., `λ z, a⁻¹ * f z`

, but the first definition will make it automatically a linear map)?

#### François Sunatori (Mar 14 2021 at 20:30):

ok nice thanks, then there is no need to define a `θ`

. I'll try it out!

#### Heather Macbeth (Mar 14 2021 at 20:42):

By the way, `conj a`

might work more nicely than `a⁻¹`

, I'm not sure, you could try it both ways!

#### Kevin Buzzard (Mar 14 2021 at 20:49):

The advantage of `conj a`

is that you don't need to get division involved, which is in general a good idea (you can use `ring`

to do your algebra, for example, if division is not involved).

#### François Sunatori (Mar 14 2021 at 20:54):

thanks for the tips :)

#### François Sunatori (Mar 14 2021 at 20:55):

btw for the definition of `h`

I'm guessing I need to do something like:

```
h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a⁻¹ * f z
, map_add' := by simp
, map_smul' := sorry
},
```

otherwise I'll just get a `h`

with type `ℂ → ℂ`

#### Kevin Buzzard (Mar 14 2021 at 20:59):

If your f is already linear then just `bub`

it with `conj a`

like Heather said and hopefully you won't need to fill in those sorries

#### Kevin Buzzard (Mar 14 2021 at 21:00):

Bubbing should send a linear map to a linear map

#### Heather Macbeth (Mar 14 2021 at 21:01):

@Kevin Buzzard I guess François is saying that he can't do this because `f`

lives in `ℂ →ₗᵢ[ℝ] ℂ`

which is only a real vector space, not complex? My bad.

#### François Sunatori (Mar 14 2021 at 21:10):

Sorry if I'm not understanding completely.. I'm still new to Lean. @Kevin Buzzard What does bubbing mean (does it mean that Lean will just understand the type of `h`

from using `conj`

)? and I'm still unsure about the meaning of the notation `ℂ →ₗᵢ[ℝ] ℂ`

.. I know it is some sort of linear map but not sure what the `ᵢ`

stands for, nor the `[ℝ]`

.

#### Heather Macbeth (Mar 14 2021 at 21:16):

Indeed, one limitation of Lean's tools is that it can be hard to discover where a notation is defined. `ℂ →ₗᵢ[ℝ] ℂ`

is notation for docs#linear_isometry, here an `ℝ`

-linear map from `ℂ`

to `ℂ`

which also preserves lengths.

#### Heather Macbeth (Mar 14 2021 at 21:17):

So, in your constructor, you'll have

```
h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a⁻¹ * f z,
map_add' := by simp,
map_smul' := sorry,
norm_map' := sorry },
```

#### François Sunatori (Mar 14 2021 at 21:22):

ok right, that's what I observed (Lean was asking me to provide something for `norm_map'`

as well and I imagine this case isn't one where bubbing will work? (since for me just setting `h := λ z, a⁻¹ * f z`

directly gives `ℂ → ℂ`

instead of `ℂ →ₗᵢ[ℝ] ℂ`

)

#### Heather Macbeth (Mar 14 2021 at 21:25):

Right ... the property `norm_map'`

is not preserved under scalar multiplication/`\bub`

/`•`

!

#### Kevin Buzzard (Mar 14 2021 at 22:45):

@François Sunatori sorry to mislead you! Bub is `\bub`

, the dot. But as you have pointed out you might not be able to use it (I was reading on my phone and couldn't even see the little l and i because of a font issue). Yes why not just make it a function, and then beef it up to a linear isometry manually, the way you originally said. By the way if you write `def foo : ℂ →ₗᵢ[ℝ] ℂ := {! !}`

and then click on the light bulb and then click on the bottom-but-one option (something about fields of a structure) then it will print out all the fields of the structure which you need to fill in.

#### François Sunatori (Mar 15 2021 at 01:24):

@Kevin Buzzard Thanks for the clarification about the bub (I was searching for that word in the codebase but didn't find anything related to what we were talking about haha, but I just tried typing `\bub`

now and indeed it gives the `•`

)! and also thanks for the trick involving `{! !}`

. I didn't know I could do that.

#### François Sunatori (Mar 21 2021 at 21:59):

I've gotten further in the proof of `linear_isometry_complex`

but not as quickly as I did with `linear_isometry_complex'`

```
import analysis.complex.basic
open complex
local notation `|` x `|` := complex.abs x
lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 → ((f z = a * z) ∨ (f z = a * conj z)) :=
begin
have h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, (f 1)⁻¹ * f z,
map_add' := by {
intros x y,
rw linear_isometry.map_add,
rw mul_add,
},
map_smul' := by {
intros m x,
rw linear_isometry.map_smul,
rw algebra.mul_smul_comm,
},
norm_map' := by {
intros x,
simp,
rw ← complex.abs_inv,
rw ← complex.abs_mul,
sorry
},
},
use f 1,
intros f1,
{
have H0 : h 0 = 0 := linear_isometry.map_zero h,
have H1 : h 1 = 1 := by {
-- TODO from use to_fun definition: λ z, (f 1)⁻¹ * f z?
sorry,
},
-- TODO from use to_fun definition: λ z, (f 1)⁻¹ * f z?
exact (linear_isometry_complex' z h H0 H1),
sorry
},
end
```

I'm left with 3 `sorry`

s. I'm trying to tackle the proof of `have H1 : h 1 = 1`

.

I'm not sure how to apply `λ z, (f 1)⁻¹ * f z`

that I defined in `h.to_fun`

.

Once I write a proof for a field in an instance of a Lean `record`

, can I invoke `h.to_fun`

and use it with `exact`

or `rw`

for example?

Thanks :)

#### Kevin Buzzard (Mar 21 2021 at 22:35):

You're proving the wrong thing:

```
lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 → ((f z = a * z) ∨ (f z = a * conj z)) :=
begin
use 0,
intro h,
simp at h,
cases h,
end
```

This says "there exists a complex number a such that if |a|=1 then something is true" so you can prove it by supplying any complex number whose norm isn't 1.

#### François Sunatori (Mar 21 2021 at 22:38):

Oh ok... so in that case it needs to be:

```
lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((f z = a * z) ∨ (f z = a * conj z))
```

?

(replace the → with ∧)

#### François Sunatori (Mar 21 2021 at 22:46):

but I would still like an answer to the following question:

I'm not sure how to apply λ z, (f 1)⁻¹ * f z that I defined in h.to_fun.

Once I write a proof for a field in an instance of a Lean record, can I invoke h.to_fun and use it with exact or rw for example?

#### Heather Macbeth (Mar 21 2021 at 22:48):

Instead of `have`

, use `let`

; `have`

forgets the definition, `let`

remembers it.

#### Heather Macbeth (Mar 21 2021 at 22:48):

Thus,

```
let h : ℂ →ₗᵢ[ℝ] ℂ :=
```

#### Heather Macbeth (Mar 21 2021 at 22:48):

Then, when the time comes to remember how `h`

was defined, you can do something like `rw h`

or `simp only [h]`

or `unfold h`

.

#### Kevin Buzzard (Mar 21 2021 at 22:52):

I think you're going the wrong way with the first `sorry`

. You have to use that |f(x)|=|x|. How about

```
norm_map' := by {
intros x,
simp,
change ∥f 1∥⁻¹ * ∥f x∥ = ∥x∥,
rw linear_isometry.norm_map,
rw linear_isometry.norm_map,
simp,
},
```

#### Kevin Buzzard (Mar 21 2021 at 22:55):

For the others, I think Heather's advice on let v have should see you through.

While I'm here I should point out that in early 2018 I was running around on the Lean chat going "me and a bunch of undergraduates have defined schemes!" and there were essentially no other number theorists or algebraic geometers here at the time, so the definition just sat there for a while with the computer scientists looking bemusedly at it, and then Johan Commelin showed up, took one look at the definition and said "you know that ->, don't you think it should be an \and?"

#### François Sunatori (Mar 21 2021 at 23:00):

Thanks @Kevin Buzzard for the trick to change to `∥-∥`

.. I actually wasn't too sure how far I would be able to get with route I had taken. And thanks for the story ! I guess I'll remember to watch out for that one in the future!

#### François Sunatori (Mar 21 2021 at 23:01):

Thank you @Heather Macbeth `let`

is exactly what I need! I guess I should have tried `let`

in the first place.. I think I wrongly assumed that it was a synonym for `have`

and maybe the parts of mathlib I was looking at weren't using `let`

so much.

#### Kevin Buzzard (Mar 21 2021 at 23:20):

`have`

is for proofs, `let`

is for data.

#### François Sunatori (Mar 22 2021 at 00:25):

Heather Macbeth said:

Then, when the time comes to remember how

`h`

was defined, you can do something like`rw h`

or`simp only [h]`

or`unfold h`

.

In the proof for

```
let H1 : h 1 = 1
```

When I try to use `rw h`

or `unfold h`

I get

```
rewrite tactic failed, lemma is not an equality nor a iff
```

but using `simp only [h]`

gives me

**A**: `⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _} 1 = 1`

and I would like to apply `λ (z : ℂ), a⁻¹ * ⇑f z`

to `1`

so I tried using `simp`

(which simplified the expression and applied `λ (z : ℂ), a⁻¹ * ⇑f z`

when I used it `norm_map'`

) but it gives me `simplify tactic failed to simplify`

.

How would I go at getting `λ (z : ℂ), a⁻¹ * ⇑f z`

out of **A**?

#### Heather Macbeth (Mar 22 2021 at 01:19):

@François Sunatori Does it work to do `simp`

rather than `simp only`

?

#### François Sunatori (Mar 22 2021 at 01:20):

no...

```
let H1 : h 1 = 1 := by {
simp,
}
```

gives

```
simplify tactic failed to simplify
```

#### Heather Macbeth (Mar 22 2021 at 01:21):

Sorry, I should have been more precise. I meant you to keep the `h`

-- `simp [h]`

rather than `simp only [h]`

.

#### François Sunatori (Mar 22 2021 at 01:23):

oh ok, yes it works but it gives me the same result as `simp only [h]`

```
⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _} 1 = 1
```

#### François Sunatori (Mar 22 2021 at 01:25):

I would still need some way to get `λ (z : ℂ), a⁻¹ * ⇑f z`

out somehow... when I worked on the proof for `norm_map'`

in the definition of `h`

, I was able to use `simp`

to get `λ (z : ℂ), a⁻¹ * ⇑f z`

out and apply it to an argument, but not in this case...

#### Heather Macbeth (Mar 22 2021 at 01:28):

Ah, I see! OK, here's a line that seems to do it:

```
change (f 1)⁻¹ * f 1 = 1,
```

Basically this is the `come_on_lean`

tactic that people joke about ...

#### Heather Macbeth (Mar 22 2021 at 01:29):

That is, we're instructing Lean to check that the following statement is definitionally equal to our goal.

#### François Sunatori (Mar 22 2021 at 01:29):

oh lol I haven't heard about that one yet!

#### François Sunatori (Mar 22 2021 at 01:29):

could it be because in the case of `norm_map'`

I was dealing with

```
⇑{to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}
```

while this time I'm dealing with

```
⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _}
```

where `to_fun`

is a level deeper?

#### Heather Macbeth (Mar 22 2021 at 01:30):

Seems plausible!

#### François Sunatori (Mar 22 2021 at 01:31):

Thanks a lot! I really couldn't wrap my head around why it worked for `norm_map'`

but not in this case (I still don't know why but at least I have a workaround now!)

#### Heather Macbeth (Mar 22 2021 at 01:32):

There are not many uses of `change`

in mathlib, because usually each definition (in the library proper rather than a definition hidden inside a proof like yours is) is immediately followed by a lemma which unfolds that definition, whose proof is `rfl`

. Often this "definition-unfolding" lemma is even a simp-lemma.

#### François Sunatori (Mar 22 2021 at 01:35):

Oh I see. Would it make sense to have that extra lemma or is it so specific that it doesn't really make sense to define it outside of this proof?

#### Heather Macbeth (Mar 22 2021 at 01:38):

I'd say, not at this stage. That sort of "infrastructure" can be figured out after everything else is working.

#### Heather Macbeth (Mar 22 2021 at 01:41):

By the way, here's an example of the kind of thing I was describing: see how the imaginary part function docs#complex.im_clm, as a continuous linear map, is immediately followed by a simp-lemma docs#complex.im_clm_apply explaining what it does as a function.

#### Scott Morrison (Mar 22 2021 at 01:44):

(I tend to write my `@[simp]`

lemmas as soon as they're needed --- every time I try `simp`

and it doesn't solve the goal, I stop to think if a lemma is missing. Life is so much easier once they're in place.)

#### François Sunatori (Mar 22 2021 at 01:47):

Oh yes I remember seeing a few of those `rfl`

lemmas often just after a definition.. Thanks, now I understand why they're there!

#### François Sunatori (Mar 22 2021 at 02:08):

Interestingly when I try the next step to go from `(f 1)⁻¹ * f 1 = 1`

to `1 = 1`

,

```
let H1 : h 1 = 1 := by {
change (f 1)⁻¹ * f 1 = 1,
rw mul_left_inv (f 1),
...
}
```

I get

```
failed to synthesize type class instance for
z : ℂ,
f : ℂ →ₗᵢ[ℝ] ℂ,
a : ℂ := ⇑f 1,
h : ℂ →ₗᵢ[ℝ] ℂ :=
{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _},
H0 : ⇑h 0 = 0 := h.map_zero
⊢ group ℂ
```

but when I look in `analysis.normed_space.linear_isometry`

I see an `instance : group (E ≃ₗᵢ[R] E)`

with `mul_left_inv`

defined..

Is there something I'm missing to make Lean aware that `f`

has access to `mul_left_inv`

?

#### François Sunatori (Mar 22 2021 at 02:09):

I also tried adding `import analysis.normed_space.linear_isometry`

but it didn't change anything

#### Heather Macbeth (Mar 22 2021 at 02:13):

Careful, `ℂ ≃ₗᵢ[ℝ] ℂ`

is a group but `ℂ`

itself is not a group!

#### Heather Macbeth (Mar 22 2021 at 02:13):

Because 0 is not invertible.

#### François Sunatori (Mar 22 2021 at 02:14):

oh right! oups

#### Heather Macbeth (Mar 22 2021 at 02:19):

Instead of the lemma docs#mul_left_inv (for groups only), you want to use the lemma docs#inv_mul_cancel.

#### François Sunatori (Mar 22 2021 at 02:22):

Ok nice and then I need to supply a proof that `a ≠ 0`

#### François Sunatori (Mar 23 2021 at 00:06):

I'm now running into an awkward situation..

I have

```
⇑f z = a * z ∨ ⇑f z = a * ⇑conj z
```

and would like to get to

```
a⁻¹ * ⇑f z = a⁻¹ * (a * z) ∨ a⁻¹ * ⇑f z = a⁻¹ * (a * ⇑conj z)
```

When I use `rw ← mul_right_inj' H3`

where (`H3 : a⁻¹ ≠ 0`

), I'm able to get

```
a⁻¹ * ⇑f z = 1 * z ∨ ⇑f z = a * ⇑conj z
```

and then I try to use `rw ← mul_right_inj' H3 @(f z) @(a * conj z)`

to act on the other equality

but I get the error

```
function expected at
mul_right_inj' H3
term has type
a⁻¹ * ?m_1 = a⁻¹ * ?m_2 ↔ ?m_1 = ?m_2
```

#### François Sunatori (Mar 23 2021 at 00:08):

I was trying to use the `@`

to pass the parameters to implicit arguments `{b c}`

#### Scott Morrison (Mar 23 2021 at 00:14):

The `@`

has to go on the `mul_right_inj'`

#### Scott Morrison (Mar 23 2021 at 00:15):

You can also use `conv`

in this situation to "zoom in" on the subexpression you want to rewrite. The proof is sometimes easier to follow this way.

#### François Sunatori (Mar 23 2021 at 00:21):

Thanks for the tips @Scott Morrison , how would I use `conv`

? Would I use it with `rw`

or on its own?

#### Scott Morrison (Mar 23 2021 at 00:21):

Something like `conv at h { congr, skip, rw p }`

.

#### Scott Morrison (Mar 23 2021 at 00:22):

This says: "look at h, split into subexpressions, skip over the first one, rewrite using `p`

in the second one".

#### François Sunatori (Mar 23 2021 at 00:26):

nice, I just tried it.. yup it's much easier to follow like this! Thanks for the new tool!

#### François Sunatori (Mar 24 2021 at 00:45):

I'm trying to use

```
apply (mul_left_cancel 2 (h z).re z.re) H_left
```

and am getting the error:

```
invalid pre-numeral, universe level must be > 0
```

when I did my first pass on the proof, I wrote this lemma

```
lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry
```

and applied it like this

```
apply (mul_left_cancel 2 (h z).re z.re) H_left
```

so that I could move on.

But now I'm cleaning up the proof and would like to know what the error `invalid pre-numeral, universe level must be > 0`

means and how I can solve it.

Thanks!

#### Yakov Pechersky (Mar 24 2021 at 01:09):

Can you share the full lemma statement and attempted proof?

#### François Sunatori (Mar 24 2021 at 01:13):

it's for this lemma in particular (it's rather long and I'm working on making it shorter but here's the part I'm having an issue with):

```
import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry
open complex
local notation `|` x `|` := complex.abs x
lemma linear_isometry_complex' (z : ℂ) (h : ℂ →ₗᵢ[ℝ] ℂ) :
h 0 = 0 → h 1 = 1 → ((h z = z) ∨ (h z = conj z))
begin
...
have Hre : (h z).re = z.re := by {
rw ext_iff at H,
iterate 2 { rw add_re at H },
iterate 2 { rw add_im at H },
iterate 2 { rw conj_re at H },
iterate 2 { rw conj_im at H },
iterate 2 { rw add_neg_self at H },
iterate 2 { rw add_self_eq at H },
cases H,
rw eq_comm at H_left,
ring at H_left,
apply (reals_mul_left_cancel 2 (h z).re z.re) H_left, <-------
},
...
end
```

#### Yakov Pechersky (Mar 24 2021 at 01:20):

what's `H`

here? just the statement

#### François Sunatori (Mar 24 2021 at 01:24):

oh sorry, yes it's

```
H : z + ⇑conj z = ⇑h z + ⇑conj (⇑h z)
```

#### Yakov Pechersky (Mar 24 2021 at 01:34):

This works for me, so something is different than what you shared:

```
import data.buffer.parser.basic
import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry
open complex
lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry
example (z : ℂ) (h : ℂ →ₗ[ℝ] ℂ) (h0 : h 0 = 0) (h1 : h 1 = 1) (H : z + z.conj = h z + (h z).conj) :
(h z).re = z.re :=
begin
rw ext_iff at H,
iterate 2 { rw add_re at H },
iterate 2 { rw add_im at H },
iterate 2 { rw conj_re at H },
iterate 2 { rw conj_im at H },
iterate 2 { rw add_neg_self at H },
rw ←two_mul at H,
rw ←two_mul at H,
cases H,
rw eq_comm at H_left,
ring_nf at H_left,
apply (reals_mul_left_cancel 2 (h z).re z.re) H_left,
end
```

#### François Sunatori (Mar 24 2021 at 01:44):

yes it works but I would like to get rid of

```
lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry
```

and use

```
apply (mul_left_cancel 2 (h z).re z.re) H_left
```

instead

#### Eric Rodriguez (Mar 24 2021 at 02:03):

The reason you're getting the cryptic pre-numeral error is because `mul_left_cancel`

has the arguments implicit so you're feeding it numbers when it expects something completely different; you'll see the same error if you change your lemma to use `{a b c : ℝ}`

. You could just `linarith [H_left]`

to get around it if you don't like using that lemma, or maybe people that know a lot more than me know how to give Lean more hints so that it would understand, say, `apply mul_left_cancel H_left`

.

#### François Sunatori (Mar 24 2021 at 02:09):

Oh great, thanks @Eric Rodriguez ! I'll stick to `linarith [H_left]`

. I haven't used much automation in my proofs yet. Does the `[H_left]`

mean: try `linarith`

lemmas with `H_left`

as a parameter?

#### Eric Rodriguez (Mar 24 2021 at 02:10):

as far as I understand! I'm still learning so I'm sure the wiser ones will know far better :b

#### François Sunatori (Mar 27 2021 at 17:39):

I'm working on readying this lemma for a PR. I'm wondering:

- in which file it should be or should it be in its own file (e.g.
`analysis/complex/isometry.lean`

)? - I have another lemma that I used in the proof of
`linear_isometry_complex`

for now it's called`linear_isometry_complex'`

. How should I name it? - I'll try to go through the documentation style (https://leanprover-community.github.io/contribute/doc.html) and rename some variables and if it will be in its own file I guess I'll need to add a file header.
- anything else I should know about the process?

thanks!

#### Johan Commelin (Mar 27 2021 at 17:40):

François Sunatori said:

- I have another lemma that I used in the proof of
`linear_isometry_complex`

for now it's called`linear_isometry_complex'`

. How should I name it?

That depends a lot on the statement

#### Johan Commelin (Mar 27 2021 at 17:40):

If it is reusable, it should be moved to the file where it belongs, and follow the naming convention

#### Johan Commelin (Mar 27 2021 at 17:40):

If it's really a one-off helper lemma, we typically append `_aux`

or something like that.

#### François Sunatori (Mar 27 2021 at 17:43):

I think it's more of a one-off helper lemma in this case so I'll add `_aux`

#### François Sunatori (Mar 27 2021 at 17:47):

How about the `linear_isometry_complex`

lemma itself? in which file would it make most sense to add it?

#### Johan Commelin (Mar 27 2021 at 17:51):

your suggestion sounded good

#### François Sunatori (Mar 27 2021 at 17:53):

ok, thanks :)

#### François Sunatori (Mar 28 2021 at 01:01):

I think I would be ready to open a PR for this addition. This is a first for me and I look forward to getting some feedback. I would like to have write access for a non-master branch. My GitHub username is `frankymacster`

. Thanks!

#### Kevin Buzzard (Mar 28 2021 at 08:34):

@maintainers

#### Scott Morrison (Mar 28 2021 at 09:24):

@François Sunatori, invitation sent! (Sorry, everyone must be enjoying their weekend, usually we're fast on these. :-)

#### François Sunatori (Mar 28 2021 at 14:20):

Thanks! No worries, I expected that since I asked on a Saturday night ;)

#### François Sunatori (Mar 29 2021 at 03:53):

Hi, I'm trying to use `conv`

on the following expression

```
(∀ (z : ℂ), a⁻¹ * ⇑f z = z) ∨ ∀ (z : ℂ), a⁻¹ * ⇑f z = ⇑conj z
```

by doing:

```
conv {
congr,
intro z <--------
},
```

but `intro z`

gives the error

```
unknown identifier 'z'
```

How come I can't use `intro`

in `conv`

? Is there some other way to deal with a situation like

```
(∀ (z : ℂ), a⁻¹ * ⇑f z = z) ∨ ∀ (z : ℂ), a⁻¹ * ⇑f z = ⇑conj z
```

to affect change to `a⁻¹ * ⇑f z = z`

for example?

Thanks!

#### Bryan Gin-ge Chen (Mar 29 2021 at 03:55):

Use `funext`

to rewrite under binders in `conv`

. See the docs.

#### François Sunatori (Mar 29 2021 at 04:03):

Thanks! I tried replacing `intro z`

with `funext`

```
conv {
congr,
funext
},
```

but the goal didn't change... the goal is

```
∀ (z : ℂ), ⇑f z = a * z
```

before and after `funext`

#### Bryan Gin-ge Chen (Mar 29 2021 at 04:09):

Ah, I guess `funext`

only works on lambdas. Maybe you can try to get inside using `find`

?

#### Alex J. Best (Mar 29 2021 at 04:12):

`conv in ..`

should work?

e.g.

```
import tactic
lemma a (a b : ℕ) : (∀ (c : ℕ), a * b = c) ∨ ∀ (c : ℕ), a = b * c :=
begin
conv in (_ = _) {
}
end
```

PS it'll be easier to help if you can make a #mwe like I did here for people to try their suggestions

#### François Sunatori (Mar 29 2021 at 04:16):

great, both `find (f _ = _)`

and `conv in (_ = _)`

worked! (I think I'll opt for `conv in (_ = _)`

since it gave less lines). Thanks to you both :)

#### Heather Macbeth (Mar 29 2021 at 04:17):

Alex J. Best said:

PS it'll be easier to help if you can make a #mwe like I did here for people to try their suggestions

One nice thing about a #mwe is that anyone can open it instantly in the web editor (using the tool in the top right corner of the code snippet) to play with it.

#### François Sunatori (Mar 29 2021 at 04:21):

Oh I didn't know that it opened the web editor! ok I'll try to do that next time, I guess it will make communicating things easier!

#### François Sunatori (Mar 31 2021 at 01:56):

I'm trying to generalize the expression `(f z).re = z.re`

to `∀ (z : ℂ), (f z).re = z.re`

like so:

```
import analysis.complex.basic
open complex
lemma add_self_eq (a : ℝ) : a + a = a * 2 := by ring
lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) : ∀ (z : ℂ), (f z).re = z.re := by {
conv at h₃ {
find (_ = _) {
rw ext_iff,
rw add_re, rw add_re,
rw add_im, rw add_im,
rw conj_re, rw conj_re,
rw conj_im, rw conj_im,
rw add_neg_self, rw add_neg_self,
rw add_self_eq, rw add_self_eq,
congr,
skip,
-- refl,
-- trivial,
},
},
sorry,
}
```

I tried to use `refl`

and `trivial`

inside `conv at h3`

(and thought that it would work since I saw it used in https://leanprover-community.github.io/extras/conv.html) but am getting this error:

```
type mismatch at application
conv.istep 19 6 19 6 refl
term
refl
has type
∀ (a : ?m_1), ?m_2 a a : Prop
but is expected to have type
conv ?m_1 : Type
```

am I missing something here? or should I be trying a different tactic?

Thanks!

#### Yakov Pechersky (Mar 31 2021 at 02:16):

One way to generalize it is just to say:

```
lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re :=
begin
simpa [ext_iff, add_re, add_im, conj_re, conj_im, ←two_mul,
(show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm
end
```

#### François Sunatori (Mar 31 2021 at 02:23):

oh nice, however an extra detail is that `(∀ z : ℂ) : (f z).re = z.re`

is a hypothesis in the lemma I'm working on. Will this work in that case?

#### Yakov Pechersky (Mar 31 2021 at 02:25):

I'm not sure what you mean. All I did was move the `∀ (z : ℂ)`

to the left of the `colon`

in ` lemma name args *here* : statement := proof`

#### Yakov Pechersky (Mar 31 2021 at 02:25):

And you'll be able to use it. Take a look:

#### Yakov Pechersky (Mar 31 2021 at 02:26):

```
import analysis.complex.basic
open complex
lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re :=
begin
simpa [ext_iff, add_re, add_im, conj_re, conj_im, ←two_mul,
(show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm
end
#check hf_re
/-
hf_re :
∀ (f : ℂ →ₗᵢ[ℝ] ℂ),
(∀ (z : ℂ), z + ⇑conj z = ⇑f z + ⇑conj (⇑f z)) → ∀ (z : ℂ), (⇑f z).re = z.re
-/
```

#### Yakov Pechersky (Mar 31 2021 at 02:26):

As you can see, I placed the `z`

to the left of the colon, and the lemma, as Lean sees it, still has the universal quantifier.

#### François Sunatori (Mar 31 2021 at 02:30):

ok thanks :) I'll see how I can use it in my lemma!

#### Greg Price (Mar 31 2021 at 02:57):

François Sunatori said:

I tried to use

`refl`

and`trivial`

inside`conv at h3`

(and thought that it would work since I saw it used in https://leanprover-community.github.io/extras/conv.html)

I think the docs may be unclear about this. That page says (modulo formatting):

Once arrived at the relevant target, we can use rw as in normal mode. Note that Lean tries to solves the current goal if it became x = x (in the strict syntactical sense, definitional equality is not enough: one needs to conclude by refl or trivial in this case).

It sounds like it's saying you can use `refl`

or `trivial`

inside the `conv`

block, but I think what it actually means is just that in that case you need to say `refl`

or `trivial`

after the `conv`

is over.

#### Greg Price (Mar 31 2021 at 03:02):

Putting the `z : ℂ`

before the colon is a good way to write the proof, but perhaps it's informative to see another way you could more directly do what you were trying to do above:

```
lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) : ∀ (z : ℂ), (f z).re = z.re := by {
intro z,
have h₄, from h₃ z,
/-
f : ℂ →ₗᵢ[ℝ] ℂ,
h₃ : ∀ (z : ℂ), z + ⇑conj z = ⇑f z + ⇑conj (⇑f z),
z : ℂ,
h₄ : z + ⇑conj z = ⇑f z + ⇑conj (⇑f z)
⊢ (⇑f z).re = z.re
-/
sorry,
}
```

#### François Sunatori (Mar 31 2021 at 03:21):

oh right, I haven't thought of doing that! thanks for the trick :)

#### François Sunatori (Mar 31 2021 at 03:24):

Greg Price said:

Putting the

`z : ℂ`

before the colon is a good way to write the proof

Is there a preferred style for mathlib in terms of having

`z : ℂ`

before the colon vs`∀ (z : ℂ)`

after the colon

?

#### Heather Macbeth (Mar 31 2021 at 03:26):

Yes, the former! It avoids one `intros`

step.

#### Heather Macbeth (Mar 31 2021 at 03:27):

And I might guess (not sure, though) that it's less sensitive to ordering of hypotheses in things like `library_search`

.

#### François Sunatori (Mar 31 2021 at 03:34):

thanks! I'll work on cleaning up my code to follow that more and maybe also split some parts out as smaller lemmas (I get the feeling my proofs were too long when I compare with other ones in mathlib)

#### François Sunatori (Mar 31 2021 at 03:36):

Is there some rule of thumb or a style preference on when a code block should stay in a `have`

inside a proof vs when it should be moved out?

#### Yury G. Kudryashov (Mar 31 2021 at 03:37):

#mwe? What are the two options (it's OK to use `foo`

instead of a real example)?

#### François Sunatori (Mar 31 2021 at 03:49):

actually I was asking more as a general question if there's a general way or heuristic to determine when a proof should be split into smaller lemmas (for one I'm guessing if it can be reused elsewhere it's a good idea to move it out as its own lemma, but would there be other reasons?), but here's how I had it:

the "main" lemma to prove

```
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))
```

an auxiliary lemma that I'm using in the proof of the one above

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) :
f 0 = 0 → f 1 = 1 → ((∀ z, f z = z) ∨ (∀ z, f z = conj z))
```

but the proof I had for `linear_isometry_complex_aux`

is almost 100 lines.. (maybe I didn't use the shortest path to get to it or I haven't used enough simplification tactics) but I'm asking because I'm guessing that at some point too many lines may not be preferable in the mathlib library.

#### Yury G. Kudryashov (Mar 31 2021 at 03:52):

In this case it looks like the `aux`

lemma is an important particular case, and it can be used separately, so it should be a separate lemma.

#### Yury G. Kudryashov (Mar 31 2021 at 03:53):

"To split or not to split" is a matter of taste. I'm not sure what's more readable: a long proof with many named `have`

s or a series of short lemmas.

#### Yury G. Kudryashov (Mar 31 2021 at 03:54):

Sure, if one of `have`

s is a useful lemma, then it should be formulated separately. Otherwise it's OK to have long proofs.

#### Yakov Pechersky (Mar 31 2021 at 03:55):

The proof for the aux lemma, in my mind, is something like

```
show that the real parts must match up (you've done this, 2 lines)
show that I maps to either I or -I
every z is a linear combination of a + b * I, so the properties you've proved so far transfer
```

#### Yakov Pechersky (Mar 31 2021 at 03:55):

And the first two can be their own lemmas, I think (?)

#### François Sunatori (Mar 31 2021 at 03:56):

ok yea I like that split. I'll try it that way

#### François Sunatori (Mar 31 2021 at 03:56):

thanks @Yury G. Kudryashov and @Yakov Pechersky !

#### Yakov Pechersky (Mar 31 2021 at 03:57):

Haven't done complex analysis in a long time, so my assumptions about what's easy or what implies what might be wrong here.

#### François Sunatori (Mar 31 2021 at 04:18):

so actually the way I had it for the `linear_isometry_complex_aux`

(at a high level) was this way:

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
...
}
```

since the last 2 (`hf_re`

and `hf_im`

) are rather general I think I'll move them to their own lemmas and maybe the other cases would stay in the proof. I don't know how conventional it is to split a proof up this way in terms of the `have`

s but it felt easier to follow for me when I did the original write up.

#### Heather Macbeth (Mar 31 2021 at 04:21):

To tweak the statement a little further, how about

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₁ : f 1 = 1) :
f = linear_isometry.id ∨ f = conj_li
```

You don't need `h₀`

, it's true automatically.

#### François Sunatori (Mar 31 2021 at 04:24):

ok sure! it looks more concise!

#### Heather Macbeth (Mar 31 2021 at 04:30):

Yakov Pechersky said:

The proof for the aux lemma, in my mind, is something like

`show that the real parts must match up (you've done this, 2 lines) show that I maps to either I or -I every z is a linear combination of a + b * I, so the properties you've proved so far transfer`

I noticed a lemma that might help carrying out Yakov's idea: docs#is_basis.ext

#### Heather Macbeth (Mar 31 2021 at 04:31):

applied to docs#complex.is_basis_one_I

#### Yakov Pechersky (Mar 31 2021 at 04:32):

With a `fin_cases`

somewhere in there

#### Scott Morrison (Mar 31 2021 at 06:11):

Heather Macbeth said:

And I might guess (not sure, though) that it's less sensitive to ordering of hypotheses in things like

`library_search`

.

library_search (and indeed many tactics) can't tell the difference between arguments before vs after the colon.

#### François Sunatori (Apr 03 2021 at 14:21):

Hi, I'm continuing on the following lemma:

```
import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry
open complex
local notation `|` x `|` := complex.abs x
lemma hf_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h₁ : ∀ z, |f z| = |z|) (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) :
(f z).im = z.im ∨ (f z).im = -z.im := by {
conv at h₁ {
find (_ = _) {
simp [complex.abs],
rw [real.sqrt_inj, norm_sq_apply (f z), norm_sq_apply z, h₂, add_left_cancel_iff,
mul_self_eq_mul_self_iff],
-- exact norm_sq_nonneg (f z),
},
},
}
```

When I apply `rw real.sqrt_inj`

, 2 more subgoals appear and I'm not sure within a `conv`

how I can do a `swap`

.

Is it doable? or do I need to go at this a different way?

Thanks!

(I'm using `conv at h₁`

because of the ` ∀ z`

)

#### Kevin Buzzard (Apr 03 2021 at 14:58):

Maybe this is easier?

```
lemma hf_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h₁ : ∀ z, |f z| = |z|) (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) :
(f z).im = z.im ∨ (f z).im = -z.im :=
begin
specialize h₁ z,
simp [complex.abs] at h₁,
rw [real.sqrt_inj, norm_sq_apply (f z), norm_sq_apply z, h₂, add_left_cancel_iff,
mul_self_eq_mul_self_iff] at h₁,
...
```

#### François Sunatori (Apr 03 2021 at 15:07):

I hadn't used `specialize`

yet. Thanks! it's much easier this way :)

#### François Sunatori (Apr 04 2021 at 02:54):

Hi, I managed to write up the proofs for all the `have`

s here:

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
sorry
}
```

what is left is the last `sorry`

.

I'm trying to get `(∀ z, f z = z) ∨ (∀ z, f z = conj z)`

from `hf_re`

and `hf_im`

.

After doing

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0' : ∀ z, |f z| = |z| := sorry,
have hf1' : ∀ z, |f z - 1| = |z - 1| := sorry,
have h₃' : ∀ z, f z + conj (f z) = z + conj z := sorry,
have hf_re' : ∀ z, (f z).re = z.re := sorry,
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
conv {
congr,
find (_ = _) {
rw ext_iff,
},
},
conv {
congr,
skip,
find (_ = _) {
rw ext_iff,
rw conj_re,
rw conj_im,
},
},
```

I end up with

```
(∀ (z : ℂ), (⇑f z).re = z.re ∧ (⇑f z).im = z.im) ∨ ∀ (z : ℂ), (⇑f z).re = z.re ∧ (⇑f z).im = -z.im
```

I tried a few things but wasn't able to get to

```
(∀ (z : ℂ), (⇑f z).re = z.re) ∧ (∀ (z : ℂ), (⇑f z).im = z.im ∨ (⇑f z).im = -z.im)
```

the closest I got was

```
(∀ (x : ℂ), (⇑f x).re = x.re) ∧ ∀ (x : ℂ), (∀ (x : ℂ), (⇑f x).im = x.im) ∨ (⇑f x).im = -x.im
```

but I still have a `∀ (x : ℂ)`

too many (it's redundant but I don't know how to get rid of it).. Is there a way to simplify this expression to

```
(∀ (z : ℂ), (⇑f z).re = z.re) ∧ (∀ (z : ℂ), (⇑f z).im = z.im ∨ (⇑f z).im = -z.im)
```

or am I taking a difficult path?

Thanks!

#### Heather Macbeth (Apr 04 2021 at 05:25):

It is worthwhile to try to carry through your own method, and probably someone will be able to help you with the details ... but I wanted to check that you also saw the advice from me and Yakov Pechersky above,

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear_isometry_complex/near/232534975

about a different method using docs#is_basis.ext.

#### Damiano Testa (Apr 04 2021 at 05:32):

I am on mobile, so I may be misunderstanding the issue, but you could try `and_distrib`

(or something similar) to split/unsplit and-or statements.

#### François Sunatori (Apr 04 2021 at 05:44):

@Heather Macbeth thanks, yes I had seen your and Yakov Pechersky's advice but I wasn't sure yet how to approach it that way so I wanted to try a first go at it with the tools that I already know and then on a second pass maybe try that advice. But maybe if it turns out that the path I'm taking is giving me too much trouble I might jump directly to trying docs#is_basis.ext.

#### Damiano Testa (Apr 04 2021 at 06:39):

Ok, this allows you to use some of your assumptions, but leaves still a tangled mess of foralls/ors!

```
rw [forall_and_distrib, forall_and_distrib, ← and_or_distrib_left, ← forall_or_distrib_left],
refine ⟨hf_re', _⟩,
```

#### Damiano Testa (Apr 04 2021 at 06:39):

I am actually not even sure if what you want to prove is true...

#### Greg Price (Apr 04 2021 at 08:25):

I think this might take you in a helpful direction:

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
specialize hf_im I,
cases hf_im,
{
left,
-- f: ℂ →ₗᵢ[ℝ] ℂ
-- h: ⇑f 1 = 1
-- hf_I : (⇑f I).im = I.im
-- ⊢ ∀ (z : ℂ), ⇑f z = z
sorry
},
{
right,
-- ...
-- hf_I : (⇑f I).im = -I.im
-- ⊢ ∀ (z : ℂ), ⇑f z = ⇑conj z
sorry
},
}
```

#### François Sunatori (Apr 04 2021 at 15:56):

@Greg Price the problem I get with using `specialize hf_im I`

is that I still need to prove

```
∀ (z : ℂ), ⇑f z = ⇑conj z
```

but now the hypothesis I would like to use (`∀ z, (f z).im = z.im ∨ (f z).im`

) is specialized at `I`

.

#### Kevin Buzzard (Apr 04 2021 at 16:04):

then you can do `have hf_im_I := hf_im I,`

or just `cases hf_im I`

#### François Sunatori (Apr 08 2021 at 02:14):

My proof was getting more and more complicated to follow, so I'm starting to look into the docs#is_basis.ext direction.

I'm not sure how to start though...

I'm guessing that

- I'll want to use
`is_basis.ext`

with`is_basis_one_I`

as one of its arguments. - I need to supply 2 linear maps in order to show with
`is_basis.ext`

that they correspond everywhere, so I would use`f`

as one of the linear maps and the other would be the identity map in once case and the conj map in the other?

or will I be using one of these as the last argument to `is_basis.ext`

```
have hf_re' : ∀ z, (f z).re = z.re := sorry
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry
```

?

Also I'm unsure how I'll be using `fin_cases`

.. maybe the path will be clearer to me once I know how to call `is_basis.ext`

..

Thanks again for all the help!

#### Heather Macbeth (Apr 08 2021 at 02:56):

François Sunatori said:

I'm guessing that

- I'll want to use
`is_basis.ext`

with`is_basis_one_I`

as one of its arguments.- I need to supply 2 linear maps in order to show with
`is_basis.ext`

that they correspond everywhere, so I would use`f`

as one of the linear maps and the other would be the identity map in once case and the conj map in the other?

This sounds good!

#### Heather Macbeth (Apr 08 2021 at 02:57):

François Sunatori said:

or will I be using one of these as the last argument to

`is_basis.ext`

`have hf_re' : ∀ z, (f z).re = z.re := sorry have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry`

I don't think you should have to consider real and imaginary parts separately. But feel free to show us the setup if this seems to be forced on you.

#### François Sunatori (Apr 08 2021 at 03:10):

ok thanks for helping point the way..

so I'll try using `is_basis.ext is_basis_one_I <a proposition involving f and id>`

`<a proposition involving f and id>`

needs to be of type `(h : ∀i, f (v i) = g (v i))`

where `i : ι`

and `ι : Type*`

is the `i`

used to parametrize the dimension of the vector space having `v`

as an element?

#### François Sunatori (Apr 17 2021 at 02:52):

I'm still unsure how to move forward at this point...

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
sorry
}
```

(all but the last `sorry`

have been proven)

I haven't found how to apply `is_basis.ext`

and `is_basis_one_I`

here.

it looks like Lean expects the next argument to be of type `∀ (i : fin 1.succ), ⇑?m_4 (![1, I] i) = ⇑?m_5 (![1, I] i)`

I have a few questions here:

- what does
`!`

mean? - what is the
`i`

of type`fin 1.succ`

?`def fin (n : ℕ) := {i : ℕ // i < n}`

so it's a natural number that is smaller than`1.succ`

?

Where can I get this number from my current setup?

Thanks

#### François Sunatori (Apr 17 2021 at 03:00):

Ok actually for `!`

I found "The notation `![a, b, ...]`

expands to `vec_cons a (vec_cons b ...)`

"

so I'm guessing `![1, I]`

is just the way that Lean represents vectors.

#### François Sunatori (Apr 17 2021 at 03:52):

ok so my understanding is that `i`

is the index of the length of the vector `![1, I]`

which in this case is `1.succ`

#### François Sunatori (Apr 17 2021 at 04:12):

I tried as a test to add hypothesis `h4`

(that would have the expected type for the 2nd argument of `is_basis.ext`

```
lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0' : ∀ z, |f z| = |z| := hf0,
have hf1' : ∀ z, |f z - 1| = |z - 1| := hf1 h,
have h₃' : ∀ z, f z + conj (f z) = z + conj z := h₃ hf1',
have hf_re' : ∀ z, (f z).re = z.re := hf_re h₃',
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := hf_im hf0 hf_re',
have h2 : ∀ z, f z = z := sorry,
have h3 : ∀ z, f z = conj z := sorry,
have h4 : ∀ (i : fin 1.succ), f (![1, I] i) = id (![1, I] i) := sorry,
exact is_basis.ext is_basis_one_I h4,
```

However I get the error

```
invalid field notation, type is not of the form (C ...) where C is a constant
1
has type
?m_1
```

when mousing over `1.succ`

.

it seems to me that `fin n`

is a dependent type depending on a natural number.

when I change it to `2`

I don't get the error anymore, but I now get

```
type mismatch at application
is_basis_one_I.ext h4
term
h4
has type
∀ (i : fin 2), ⇑f (![1, I] i) = id (![1, I] i)
but is expected to have type
∀ (i : fin 1.succ), ⇑?m_4 (![1, I] i) = ⇑?m_5 (![1, I] i)
```

How can I get `∀ (i : fin 1.succ), ⇑f (![1, I] i) = id (![1, I] i)`

to work here?

#### Johan Commelin (Apr 17 2021 at 05:26):

@François Sunatori Right `![a,b,c,x,y,z]`

is just notation for the vector `(a,b,c,x,y,z)`

in 6-dim space.

And `i : fin 1.succ`

means some term of type `fin 1.succ`

where `1.succ : nat`

is just `2`

. So `i = 0`

or `i = 1`

.

In total `![1, I] i`

means the `i`

th component of the vector `(1,I)`

. So this is `1`

if `i = 0`

and `I`

if `i = 1`

.

#### Ruben Van de Velde (Apr 17 2021 at 09:20):

Unpolished but sorry-free:

#### François Sunatori (Apr 17 2021 at 10:17):

@Ruben Van de Velde oh that's quite a bit more than what I was asking for, but maybe I can go over it and try to learn from it and I may ask a few questions about some sections just so that I can learn and compare with what I had. Thanks

#### François Sunatori (Apr 18 2021 at 17:46):

I'm now working on changing the initial statement to

```
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li
```

I defined `rotation`

like so

```
import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry
open complex
local notation `|` x `|` := complex.abs x
def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a * z,
map_add' := λ x y, mul_add a x y,
map_smul' := by {
intros m x,
simp,
rw ← mul_assoc a m x,
rw mul_comm a m,
exact mul_assoc ↑m a x,
},
norm_map' := by {
intro x,
simp,
rw ha,
rw one_mul,
},
}
```

but am getting the error

```
definition 'rotation' is noncomputable, it depends on 'complex.normed_field'
```

I'm not sure what this error means.

I thought I was not exposing `normed_field`

and tried using `open complex.normed_field`

but that gives the error `invalid namespace name 'complex.normed_field'`

.

Am I missing something here?

Thanks :)

#### Hanting Zhang (Apr 18 2021 at 17:50):

Add `noncomputable def ...`

to the beginning

#### François Sunatori (Apr 18 2021 at 17:53):

@Hanting Zhang thanks!

I just saw in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

The standard library also defines a choice principle that is entirely antithetical to a computational interpretation, since it magically produces “data” from a proposition asserting its existence. Its use is essential to some classical constructions, and users can import it when needed. But expressions that use this construction to produce data do not have computational content, and in Lean we are required to mark such definitions as noncomputable to flag that fact.

#### François Sunatori (Apr 18 2021 at 17:54):

If I understand well, I need to use `noncomputable def`

when I use a record type to use it as data?

#### Hanting Zhang (Apr 18 2021 at 17:57):

I'm not sure what you mean by record type, but my understanding is that `noncomputable`

means Lean can't produce bytecode for the data your working with. So you can't do `#print ...`

, but otherwise everything else works as normal

#### Alex J. Best (Apr 18 2021 at 17:59):

It's only some types that are `noncomputable`

, things like `complex`

and `real`

are some of them. If you just want to prove theorems the standard advice is to put the line `noncomputable theory`

at the top of your file (below the imports), and lean will stop bothering you about

```
definition 'rotation' is noncomputable, it depends on 'complex.normed_field'
```

you don't really lose anything by doing this.

#### Kevin Buzzard (Apr 18 2021 at 18:46):

I remember as a beginner being really concerned/confused about what the ramifications of all this noncomputable stuff was, as I was trying to formalise random undergraduate maths from my intro to proof course, and it turned out some was computable and some was not. The thing which took a while to dawn on me was this: if you make noncomputable stuff, then `#eval`

and `#reduce`

might not work -- but if you just want to prove theorems you never use these things anyway, you just use `theorem`

. So `noncomputable`

doesn't matter at all. The majority of the perfectoid space repo was noncomputable, for example.

#### François Sunatori (Apr 18 2021 at 21:56):

I'm trying to get from

```
f = rotation ha ∨ f = (rotation ha).comp conj_li
```

to

```
((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))
```

so that I can reuse the proof I have for

```
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))
```

This is what I have:

```
import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry
open complex
local notation `|` x `|` := complex.abs x
noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a * z,
map_add' := λ x y, mul_add a x y,
map_smul' := by {
intros m x,
simp,
rw ← mul_assoc a m x,
rw mul_comm a m,
exact mul_assoc ↑m a x,
},
norm_map' := by {
intro x,
simp,
rw ha,
rw one_mul,
},
}
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li := by {
let a := f 1,
use a,
split,
{
rw rotation,
left,
change f = λ z, a * z,
sorry,
},
{
sorry
}
}
```

Specifically for now, I'm trying to get from

```
f = rotation ha
```

to

```
∀ z, f z = a * z
```

I tried to use the `come_on_lean`

tactic (`to_fun := λ (z : ℂ), a * z`

because I want to get `λ (z : ℂ), a * z`

"out" of `rotation`

) to go from

```
f = rotation ha
```

to

```
f = λ z, a * z
```

but I get this error

```
type mismatch at application
f = λ (z : ℂ), a * z
term
λ (z : ℂ), a * z
has type
ℂ → ℂ
but is expected to have type
ℂ →ₗᵢ[ℝ] ℂ
```

Is there a way for me to isolate the `to_fun`

from the `rotation`

linear isometry in this case?

Thanks!

#### Hanting Zhang (Apr 18 2021 at 22:12):

Is this true or am I missing something? `f`

doesn't need to be a rotation, but you are asserting that it is?

#### Eric Wieser (Apr 18 2021 at 22:16):

You want the proof that `coe_fn`

is injective

#### Eric Wieser (Apr 18 2021 at 22:17):

Something like docs#linear_map.coe_injective, but for ` →ₗᵢ[ℝ]`

. Edit: ah, docs#linear_isometry.coe_fn_injective

#### François Sunatori (Apr 18 2021 at 22:18):

@Hanting Zhang sorry, here I'm assuming `|a| = 1`

so it `a = e^iθ`

and I'm not considering translations

#### Eric Wieser (Apr 18 2021 at 22:20):

Oh, actually just tactic#ext should do the trick

#### Hanting Zhang (Apr 18 2021 at 22:21):

Oh nevermind, I missed the little `ₗᵢ`

subscript, sorry!

#### François Sunatori (Apr 18 2021 at 22:21):

@Eric Wieser Thanks! I'll look into docs#linear_isometry.coe_fn_injective. By the way, I've been seeing `coe`

a lot and I think it has to do with `⇑`

but I still don't really understand what it means... Could you enlighten me or point me to a doc about it? Thank you!

#### Eric Wieser (Apr 18 2021 at 22:27):

I don't know what `come_on_lean`

refers to, but the trick is to add a helper lemma as soon as you've made the definition:

```
noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ norm_map' := λ z, by simp [ha],
to_linear_map := algebra.lmul ℝ ℂ a, }
@[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl
```

#### François Sunatori (Apr 18 2021 at 22:29):

`come_on_lean`

refers to the comment

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear_isometry_complex/near/231253906

#### Eric Wieser (Apr 18 2021 at 22:29):

Then you can get back to doing maths rather than fighting lean with:

```
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li :=
begin
refine ⟨f 1, _, _⟩,
{ sorry, },
{ left,
ext1,
rw rotation_apply,
sorry },
end
```

#### François Sunatori (Apr 18 2021 at 22:31):

Eric Wieser said:

I don't know what

`come_on_lean`

refers to, but the trick is to add a helper lemma as soon as you've made the definition:`noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ := { norm_map' := λ z, by simp [ha], to_linear_map := algebra.lmul ℝ ℂ a, } @[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl`

wow that's much simpler than what I had written.. I hope I can write concisely like that at some point

#### Eric Wieser (Apr 18 2021 at 22:32):

The trick there was knowing that docs#algebra.lmul already existed

#### Eric Wieser (Apr 18 2021 at 22:32):

But all you actually needed to get out of your struggle is that `rotation_apply`

lemma

#### Eric Wieser (Apr 18 2021 at 22:33):

When you define a bundled map `some_func`

, you almost never want to `rw some_func`

; you usually want to define an `_apply`

lemma like I do there

#### François Sunatori (Apr 18 2021 at 22:34):

ok yes, I recall seeing some `_apply`

lemmas where there was just a `rfl`

as proof.

I'll keep in mind that I better add those when I have a `def`

for a function inside a record

#### Eric Wieser (Apr 18 2021 at 22:35):

Sometimes its more useful to define `coe_some_func`

instead of `some_func_apply`

, especially if you didn't actually end up using a `λ`

to define the function:

```
@[simp] lemma coe_rotation {a : ℂ} (ha : |a| = 1) :
⇑(rotation ha) = algebra.lmul ℝ ℂ a := rfl
```

#### Eric Wieser (Apr 18 2021 at 22:36):

But that can often lead simp in a direction that's unhelpful

#### François Sunatori (Apr 18 2021 at 22:45):

ok so, when I see `coe_`

and `_apply`

I can assume they are used for a similar purpose? The one of getting a "field" out of a record.

#### François Sunatori (Apr 18 2021 at 22:46):

and is the `⇑`

linked to `coe`

(coercion)?

#### Eric Wieser (Apr 18 2021 at 22:47):

Strictly `⇑`

is docs#coe_fn

#### Eric Wieser (Apr 18 2021 at 22:48):

`↑`

is docs#coe, `↥`

is docs#coe_sort. Lots of lemma names are pretty lax about the difference, especially since sometimes `↑`

ends up meaning one of the other arrows

#### François Sunatori (Apr 18 2021 at 22:49):

ah ok, great! thanks.. it's getting clearer to me :)

#### François Sunatori (Apr 19 2021 at 01:05):

I managed to get a little further by adding `conj_li_apply`

:

```
import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry
noncomputable theory
open complex
local notation `|` x `|` := complex.abs x
noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ norm_map' := λ z, by simp [ha],
to_linear_map := algebra.lmul ℝ ℂ a, }
@[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl
lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li :=
begin
let a := f 1,
refine ⟨a, _, _⟩,
{
change ∥a∥ = 1,
simp only [a],
rw linear_isometry.norm_map,
simp,
},
{
conv {
congr,
},
-- left,
-- ext1 z,
-- rw rotation_apply,
-- right,
-- ext1 z,
-- norm_num,
},
end
```

Now I need to use `conv`

followed by `congr`

to change the 2 sides of the `∨`

in `f = rotation _ ∨ f = (rotation _).comp conj_li`

.

I would like to apply the commented out sections to the 2 sides of the `∨`

, but I don't know how to use `ext1`

in conversion tactic mode. What should I be using once in `conv`

?

Thanks!

#### François Sunatori (Apr 19 2021 at 01:33):

I looked for all instances of `conv`

in mathlib but haven't seen an example of an `ext`

being used in a `conv`

block.. and I couldn't find something doing the equivalent of an `ext`

either..

Is it possible that it can't be used in a `conv`

block and that I should approach this from a different direction?

#### Alex J. Best (Apr 19 2021 at 01:49):

Does funext work in this context?

#### Eric Rodriguez (Apr 19 2021 at 01:50):

`ext`

wouldn't work in `conv`

i don't think, as presumably it'd have to write it as (`∀ z, <stuff> ∨ ∀ z, <stuff>`

whilst `ext`

immediately `intros`

. not sure how feasible it is but maybe just do the work in some `have`

s and then `rw`

#### Eric Rodriguez (Apr 19 2021 at 01:50):

just tried it alex, it basically seems to be a noop

#### François Sunatori (Apr 19 2021 at 01:58):

right, no `funext`

didn't work.. I'll try with some `have`

s then. Thanks!

#### Eric Wieser (Apr 19 2021 at 07:36):

Ideally at this point you'd use the maths proof to decide whether the left or right of the or is true

Last updated: May 19 2021 at 02:10 UTC