Unclear what the state to proof means

Stream: new members

[Lode Vermeulen]

I am porting some Lean3 code right now, and I am getting stuck on the final part of a proof where the state is ?refine_1.intro.intro.a ∈ M₁_wo_c.edgeSet. I am unsure what this means and how I can prove this. See the following environment for the relevant code)

[Ruben Van de Velde]

It means that you need to prove something is in M₁_wo_c.edgeSet, but you haven't told lean what yet

[Ruben Van de Velde]

There will be another goal further down with label refine_1.intro.intro.a where the goal is the type of the value you need

[Ruben Van de Velde]

If you already have a hypothesis hx : x ∈ M₁_wo_c.edgeSet, you can write exact hx and lean will figure out the rest

[Lode Vermeulen]

Ruben Van de Velde said:

There will be another goal further down with label refine_1.intro.intro.a where the goal is the type of the value you need

Right, it states as a second goal Sym2 V. I guess then this is the type of refine_1.intro.intro.a of which I need to show membership?

[Notification Bot]

Lode Vermeulen has marked this topic as resolved.

[Notification Bot]

Lode Vermeulen has marked this topic as unresolved.

[Lode Vermeulen]

Ruben Van de Velde said:

It means that you need to prove something is in M₁_wo_c.edgeSet, but you haven't told lean what yet

And the goal is that I need to prove that something is in M₁_wo_c.edgeSet, i.e. it is not empty?

[Ruben Van de Velde]

Well, depends

[Ruben Van de Velde]

In this case I think so, but generally you may have another goal where you need to prove something else about this specific value ?refine_1.intro.intro.a ∈ M₁_wo_c.edgeSet

[Lode Vermeulen]

Ruben Van de Velde said:

generally you may have another goal where you need to prove something else about this specific value ?refine_1.intro.intro.a ∈ M₁_wo_c.edgeSet

Wouldn't the variable you need to prove membership of be named in that case? Otherwise you wouldn't know what it is referencing to.

[Ruben Van de Velde]

refine_1.intro.intro.a is a name, if not a great one :)

[Ruben Van de Velde]

You can see more clearly what's going on with

      have := symmDiffDisjoint h1 h2
      simp only [Set.bot_eq_empty, Set.le_eq_subset, Set.subset_empty_iff] at this
      sorry

It turns out that you need to prove False given that your set is empty; that is, your set is not empty

[Lode Vermeulen]

Oh wow, that is great

[Lode Vermeulen]

With the set in question being M₁_wo_c.edgeSet?

[Ruben Van de Velde]

Yep