Using structures in theorem

Stream: new members

[Brandon Brown]

I have a definition of a partition:

[Brandon Brown]

structure partition (X : Type*) :=
(F : set (set X))
(disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ F, x ∈ A)
(nonempty : ∀ A ∈ F, A ≠ ∅)

And let's say I have a proof that if two sets in a partition share an element, it implies they're the same set.

lemma partition_els_eq_if_share_el'
{X : Type*} {F : partition X} {A B : set X} {h₁ : A ∈ F.F}
{h₂ : B ∈ F.F} : (∃ x : X, x ∈ A ∧ x ∈ B) → A = B := sorry

The problem is if I use this lemma in some other proof the type inference system (elaborator?) tries to find a term of the form "?.F" so it searches for a partition in the context to match, but I want it to just fill with a set of sets in the context with the proofs that it is a partition also in the context. I.e. as currently written, my goal turns into this undesirable metavariable: A ∈ ?m_1.F

I can fix this by re-writing my lemma as so but it requires me to copy the definition of a partition, which is annoying.

lemma partition_els_eq_if_share_el
{F : set (set X)}
{disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅}
{cover : ∀ x : X, ∃ A ∈ F, x ∈ A}
{nonempty : ∀ A ∈ F, A ≠ ∅}
{A B ∈ F}
(h : ∃ x : X, x ∈ A ∧ x ∈ B) : A = B

Is there another way to salvage the first, more concise lemma?

[Kevin Buzzard]

Just make some stuff explicit in partition_els_eq_if_share_el'

[Kevin Buzzard]

You're using { } for inputs and Lean can't guess the inputs. Change some of the brackets to ( ) and supply them yourself.

[Mario Carneiro]

h1 and h2 should not be implicit in partition_els_eq_if_share_el' since they can't be inferred

[Kevin Buzzard]

lemma partition_els_eq_if_share_el'
{X : Type*} {F : partition X} {A B : set X} (h₁ : A ∈ F.F)
(h₂ : B ∈ F.F) : (∃ x : X, x ∈ A ∧ x ∈ B) → A = B := sorry

[Mario Carneiro]

and your problem suggests that F may also need to be explicit

[Brandon Brown]

ohh right, that should work. I'm expecting too much of type inference. Thanks!