# Zulip Chat Archive

## Stream: new members

### Topic: Way to rewrite goal containing \in

#### Nicolò Cavalleri (Jun 16 2020 at 16:51):

Since a set looks to be defined as a function from the type to propositions and is specified as a proposition that the elements of a type need to satisfy in order to be an element of the set, I was wondering if there is a convenient tactic to rewrite a goal of the form `a ∈ A`

as the proposition `a`

needs to satisfy in order to be a member of `A`

#### Jalex Stark (Jun 16 2020 at 16:58):

it's `A`

#### Kevin Buzzard (Jun 16 2020 at 16:58):

That's breaking the interface but it's also the correct answer: `A a`

is the proposition which is true iff a is in A

#### Jalex Stark (Jun 16 2020 at 16:59):

maybe you want `rw set.mem_def`

#### Nicolò Cavalleri (Jun 16 2020 at 17:58):

I am not really sure I understand! What I meant was that `a ∈ A`

is the goal and I want to put it in a more explicit form. In my case the set `A`

depends on many parameters, and if copy the set name in the proof Lean does not recognize these parameters (I have no idea why since they are defined). On the other hand `rw set.mem_def`

just rewrites `a ∈ A`

as `A a`

and does not make anything explicit. I attach the pictures Annotazione-2020-06-16-195745.png Annotazione-2020-06-16-195616.png Annotazione-2020-06-16-195540.png of the two propose tactics for clearance.

#### Jalex Stark (Jun 16 2020 at 18:02):

give us code we can cut/paste into our local editors (the jargon for this here is #mwe)

#### Reid Barton (Jun 16 2020 at 18:04):

Your question doesn't seem to be about set membership, but rather the definition of the specific set you're interested in

#### Nicolò Cavalleri (Jun 16 2020 at 18:06):

```
import geometry.manifold.real_instances
import algebra.group.defs
noncomputable theory
instance prod_manifold (H : Type*) [topological_space H] (M : Type*) [topological_space M] [manifold H M]
(H' : Type*) [topological_space H'] (M' : Type*) [topological_space M'] [manifold H' M'] : manifold (H×H') (M×M') :=
sorry,
instance prod_smooth_manifold_with_corners {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
{H' : Type*} [topological_space H'] (I' : model_with_corners 𝕜 E' H')
(M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
(M' : Type*) [topological_space M'] [manifold H' M'] [smooth_manifold_with_corners I' M'] :
smooth_manifold_with_corners (I.prod I') (M×M') :=
{
compatible :=
begin
intro f,
intro g,
intro h_f,
intro h_g,
cases h_f with f1 temp,
cases temp with hf1 temp2,
cases temp2 with f2 temp3,
cases temp3 with hf2 hf,
rw hf,
cases h_g with g1 temp,
cases temp with hg1 temp2,
cases temp2 with g2 temp3,
cases temp3 with hg2 hg,
rw hg,
simp,
rw set.mem_def,
end,
}
```

#### Nicolò Cavalleri (Jun 16 2020 at 18:08):

Well the specific set I am interested in is a set defined by a property:

#### Jalex Stark (Jun 16 2020 at 18:12):

`dsimp`

or `unfold members`

might do it

#### Jalex Stark (Jun 16 2020 at 18:13):

`tidy`

might do something useful, and you can interrogate it with `tidy?`

#### Jalex Stark (Jun 16 2020 at 18:15):

your example breaks for me at the first cases, maybe my mathlib is outdated

```
def x := {n : ℕ | 2 < n ∧ n < 4}
example {α : Type} {n : ℕ} (hn : x n) : n = 3 :=
begin
cases hn,
linarith,
end
```

#### Jalex Stark (Jun 16 2020 at 18:16):

the "operation" you're trying to do is to replace something with something else that's defeq

#### Jalex Stark (Jun 16 2020 at 18:16):

so whatever you wanted to do after unfolding the definition, you can probably already do it

#### Nicolò Cavalleri (Jun 16 2020 at 18:20):

Sorry, this should work! I might have put a sorry where I did not have to

```
import geometry.manifold.real_instances
import algebra.group.defs
noncomputable theory
instance prod_manifold (H : Type*) [topological_space H] (M : Type*) [topological_space M] [manifold H M]
(H' : Type*) [topological_space H'] (M' : Type*) [topological_space M'] [manifold H' M'] : manifold (H×H') (M×M') :=
{ atlas := λ f : (local_homeomorph (M×M') (H×H')),
∃ g, (g ∈ (manifold.atlas H M)) ∧ (∃ h, (h ∈ (manifold.atlas H' M')) ∧ (f = (local_homeomorph.prod g h))),
chart_at := (λ x: (M×M'), local_homeomorph.prod (manifold.chart_at H x.1) (manifold.chart_at H' x.2)),
/- Why only H??? -/
mem_chart_source := λ x, by simp,
chart_mem_atlas :=
begin
intro x,
use (manifold.chart_at H x.1),
split,
simp,
use (manifold.chart_at H' x.2),
simp,
end,}
instance prod_smooth_manifold_with_corners {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
{H' : Type*} [topological_space H'] (I' : model_with_corners 𝕜 E' H')
(M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
(M' : Type*) [topological_space M'] [manifold H' M'] [smooth_manifold_with_corners I' M'] :
smooth_manifold_with_corners (I.prod I') (M×M') :=
{
compatible :=
begin
intro f,
intro g,
intro h_f,
intro h_g,
cases h_f with f1 temp,
cases temp with hf1 temp2,
cases temp2 with f2 temp3,
cases temp3 with hf2 hf,
rw hf,
cases h_g with g1 temp,
cases temp with hg1 temp2,
cases temp2 with g2 temp3,
cases temp3 with hg2 hg,
rw hg,
simp,
end,
}
```

#### Jalex Stark (Jun 16 2020 at 18:22):

i don't understand all this geometry, but maybe you find `split; dsimp,`

interesting after the last line of your proof so far

#### Nicolò Cavalleri (Jun 16 2020 at 18:41):

Thanks for your help! Basically what I was trying to do was simply to find a way to make the property explicit so that I could understand why `rw prod_coe_symm`

, where

```
@[simp] lemma prod_coe_symm (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
((e.prod e').symm : β × δ → α × γ) = λp, (e.symm p.1, e'.symm p.2) := rfl
```

fails:

```
rewrite tactic failed, did not find instance of the pattern in the target expression
⇑((local_homeomorph.prod ?m_9 ?m_10).symm)
state:
𝕜 : Type ?,
_inst_1 : nondiscrete_normed_field 𝕜,
E : Type ?,
_inst_2 : normed_group E,
_inst_3 : normed_space 𝕜 E,
E' : Type ?,
_inst_4 : normed_group E',
_inst_5 : normed_space 𝕜 E',
H : Type ?,
_inst_6 : topological_space H,
I : model_with_corners 𝕜 E H,
H' : Type ?,
_inst_7 : topological_space H',
I' : model_with_corners 𝕜 E' H',
M : Type ?,
_inst_8 : topological_space M,
_inst_9 : manifold H M,
_inst_10 : smooth_manifold_with_corners I M,
M' : Type ?,
_inst_11 : topological_space M',
_inst_12 : manifold H' M',
_inst_13 : smooth_manifold_with_corners I' M',
f g : local_homeomorph (M × M') (H × H'),
f1 : local_homeomorph M H,
hf1 : f1 ∈ atlas H M,
f2 : local_homeomorph M' H',
hf2 : f2 ∈ atlas H' M',
hf : f = f1.prod f2,
g1 : local_homeomorph M H,
hg1 : g1 ∈ atlas H M,
g2 : local_homeomorph M' H',
hg2 : g2 ∈ atlas H' M',
hg : g = g1.prod g2
⊢ (f1.prod f2).symm.trans (g1.prod g2) ∈ (times_cont_diff_groupoid ⊤ (I.prod I')).members
```

indeed it looks pretty easy to me to see where the instance of the pattern in the target expression is (`(f1.prod f2).symm`

) and I do not understand why Lean does not recognize it.

In particular I was not really looking to go on with the proof but simply to find out why I cannot rewrite this lemma, but I guess there is not a simple way to make this goal explicit (the tactic you suggested either time out or require me to write the set name inside the code, and Lean does not recognize the set name). Do you have any idea why lean does not recognize the target expression?

#### Kevin Buzzard (Jun 16 2020 at 18:54):

I think the issue is that the lemma is about the coercion of `(f1.prod f2).symm`

to a function, but your goal does not have this coercion.

#### Kevin Buzzard (Jun 16 2020 at 18:58):

Your goal is an assertion about a local homeomorphism, not a function. You might think "a local homeomorphism _is_ a function!" but this is not true in Lean -- they have different types so it's meaningless to say that they're equal. There's an "invisible function" which takes the local homeo to a function, and this invisible function isn't there in the goal, but it is there in the lemma you're trying to use to rewrite.

#### Reid Barton (Jun 16 2020 at 18:59):

it's also in the name `coe`

#### Kevin Buzzard (Jun 16 2020 at 18:59):

The invisible function in this case is called a coercion.

#### Patrick Massot (Jun 16 2020 at 19:01):

And it's not invisible in the error message `⇑((local_homeomorph.prod ?m_9 ?m_10).symm)`

, that's the first character.

#### Kevin Buzzard (Jun 16 2020 at 19:01):

indeed, Lean can see it -- it's just invisible to mathematicians :-)

#### Patrick Massot (Jun 16 2020 at 19:11):

If you want to go to concrete goals, you can use `rw [times_cont_diff_groupoid, mem_groupoid_of_pregroupoid], simp, split,`

but I'm not sure it's the recomended way (only Sébastien could tell us).

#### Sebastien Gouezel (Jun 16 2020 at 20:26):

First, I would clean up the expression of your map. Can you prove lemmas such as

```
lemma prod_symm (e : local_homeomorph α β) (e' : local_homeomorph γ δ) :
(e.prod e').symm = (e.symm.prod e'.symm) :=
sorry
lemma prod_comp {η : Type*} {ε : Type*} [topological_space η] [topological_space ε]
(e : local_homeomorph α β) (f : local_homeomorph β γ)
(e' : local_homeomorph δ η) (f' : local_homeomorph η ε):
(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
sorry
```

(When you want to prove that two objects are equal, a good method is to start with `ext x`

. Sometimes, `ext`

tries to do too much, and then `ext x : 1`

is better).

#### Sebastien Gouezel (Jun 16 2020 at 20:27):

(These should be in the library, but you just found one of many holes: it just means that until now no one has really needed to use thoroughly products of local homeos).

#### Sebastien Gouezel (Jun 16 2020 at 20:32):

I have posted working proofs at https://gist.github.com/sgouezel/d8ea6cc252be22590f5c16574eb47608, but in case you want to come up with your own solutions I am not posting them here to avoid spoiling.

#### Nicolò Cavalleri (Jun 17 2020 at 16:24):

Ok, thanks a lot to everybody! I admit I had no idea what coercion was so I did not recognize `coe`

in the name of the function. Now that I know about its existence I proved and used the lemma `prod_symm`

by Sebastian to rewrite the goal as I wanted and it worked. However, I still have no idea whatsoever on how to approach hypotheses and goals of the form `e ∈ times_cont_diff_groupoid ⊤ I`

. I gave up on rewriting it as the defining propositions as I cannot mange to make the suggested tactics work. As Jalex suggested I am trying to think `e ∈ times_cont_diff_groupoid ⊤ I`

as if its defining property were written instead. As `e ∈ (times_cont_diff_groupoid ⊤ I)`

is defined to be `e ∈ (times_cont_diff_groupoid ⊤ I).members`

and in this case `(times_cont_diff_groupoid ⊤ I).members`

is defined to be ` {e : local_homeomorph H H | PG.property e e.source ∧ PG.property e.symm e.target}`

for some pregroupoid `PG`

I would expect to make some progress with a hypothesis`h: (e ∈ times_cont_diff_groupoid ⊤ I)`

by writing ` cases h with h1 h2`

and obtain something I can work with, however when doing so I get the following:

```
h1:
{property := λ (f : H → H) (s : set H),
times_cont_diff_on 𝕜 ⊤ (⇑I ∘ f ∘ ⇑(I.symm)) (⇑(I.symm) ⁻¹' s ∩ set.range ⇑I),
comp := _,
id_mem := _,
locality := _,
congr := _}.property
⇑e
e.to_local_equiv.source,
h2 :
{property := λ (f : H → H) (s : set H),
times_cont_diff_on 𝕜 ⊤ (⇑I ∘ f ∘ ⇑(I.symm)) (⇑(I.symm) ⁻¹' s ∩ set.range ⇑I),
comp := _,
id_mem := _,
locality := _,
congr := _}.property
⇑(e.symm)
e.to_local_equiv.target
```

suggesting things are not really going as I expect and suggesting that even if `times_cont_diff_groupoid ⊤ I`

should be a groupoid, things are stored inside still as a pregroupoid. If it were actually a groupoid I would use the lemma `mem_groupoid_of_pregroupoid`

, but lean won't accept this because indeed `times_cont_diff_groupoid ⊤ I`

is a groupoid (is there a way to have it back as a pregroupoid)? So I am still looking for some advice on how to deal with hypotheses and goals of this kind, if anybody has some!

#### Jalex Stark (Jun 17 2020 at 16:26):

`dsimp at h1`

should make things a little nicer

#### Reid Barton (Jun 17 2020 at 16:27):

You can always just use `change`

to unfold definitions to the form you want

#### Reid Barton (Jun 17 2020 at 16:27):

that said, I would also expect your `cases h`

to work so maybe something else is going on

#### Nicolò Cavalleri (Jun 17 2020 at 16:35):

Jalex Stark said:

`dsimp at h1`

should make things a little nicer

The problem with `simp`

, `dsimp`

, `rw`

and all of those tactics is that they just rewrite the hypotheses in a way which is almost identical with the definition. For example `dsimp`

rewrites `e ∈ (times_cont_diff_groupoid ⊤ I)`

as `e ∈ (times_cont_diff_groupoid ⊤ I).members`

and this does not really help me as I already knew the two were equivalent and what I need to do here is to transform things so that I get everything expressed with `times_cont_diff`

from calculus and then I can use the lemmas from the calculus library.

#### Reid Barton (Jun 17 2020 at 16:37):

`dsimp [times_cont_diff_groupoid] at h1`

maybe

#### Jalex Stark (Jun 17 2020 at 16:38):

Sorry, I only meant that it should collapse `{property := x, ...}.property`

into `x`

#### Nicolò Cavalleri (Jun 17 2020 at 16:46):

Jalex Stark said:

Sorry, I only meant that it should collapse

`{property := x, ...}.property`

into`x`

Oh right sorry to you, I just got confused between the notation I am using in my file and I thought you meant a different thing. What you suggest does make things nicer even if things are still a bit different from what I expect: they are not just the properties defining the set applied to `e`

but a lot of coercions (shift symbols) seem to appear, so I will try to read a bit more from the tutorial before going on as I don't really know about them. Thanks a lot fot the help!

#### Sebastien Gouezel (Jun 17 2020 at 17:13):

If you give a #mwe I can have a look.

#### Nicolò Cavalleri (Jun 17 2020 at 17:48):

Ok thanks a lot! I will try a bit more on my own and then come back if I won't have managed!

Last updated: Dec 20 2023 at 11:08 UTC