Way to rewrite goal containing \in

Stream: new members

[Nicolò Cavalleri]

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]

it's A

[Kevin Buzzard]

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]

maybe you want rw set.mem_def

[Nicolò Cavalleri]

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]

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

[Reid Barton]

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

[Nicolò Cavalleri]

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]

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

[Jalex Stark]

dsimp or unfold members might do it

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Nicolò Cavalleri]

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]

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]

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]

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]

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]

it's also in the name coe

[Kevin Buzzard]

The invisible function in this case is called a coercion.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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]

(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]

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]

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 hypothesish: (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]

dsimp at h1 should make things a little nicer

[Reid Barton]

You can always just use change to unfold definitions to the form you want

[Reid Barton]

that said, I would also expect your cases h to work so maybe something else is going on

[Nicolò Cavalleri]

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]

dsimp [times_cont_diff_groupoid] at h1 maybe

[Jalex Stark]

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

[Nicolò Cavalleri]

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]

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

[Nicolò Cavalleri]

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