# Zulip Chat Archive

## Stream: new members

### Topic: Composition with metavariable

#### Brandon Brown (Jun 01 2020 at 02:20):

I have two functions `F : setoid ?M_1 → partition ?M_1`

and `G : partition ?M_1 → setoid ?M_1`

and I want to prove `function.left_inverse G F`

or that `(G ∘ F) = id`

. If I do `#check function.left_inverse G F`

I get `Prop`

which is what I expect, but if I try to prove this e.g. `example : function.left_inverse G F`

I get an error `don't know how to synthesize placeholder.`

Which I think is due to the metavariables since setoid and partition are not referring to particular types yet. What is the proper way to do this with these kind of functions?

#### Bryan Gin-ge Chen (Jun 01 2020 at 02:22):

#mwe ?

#### Brandon Brown (Jun 01 2020 at 02:24):

```
import data.setoid
import data.equiv.basic
open set
open setoid
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 ≠ ∅)
def F {X : Type*} (S : setoid X) : partition X :=
partition.mk
(
classes S
)
( -- ⊢ (disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
begin
intros,
apply eq_of_subset_of_subset,
{
intro x,
intros,
rw mem_empty_eq,
apply a,
cases a_1,
--have F : set (set X), from classes S,
apply eq_of_mem_classes,
repeat {assumption},
},
{
apply set.empty_subset,
}
end
)
( -- ⊢ (cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
begin
intros,
split,
use x,
simp,
end
)
( -- ⊢ (nonempty : ∀ A ∈ ℱ, A ≠ ∅)
begin
intros,
intro aqn,
apply empty_not_mem_classes,
rwa ← aqn,
end
)
#check F
/-
Q3 : now define a map the other way
-/
def G {X : Type*} (P : partition X) : setoid X :=
begin
intros,
apply setoid.setoid_of_disjoint_union,
swap 3,
exact P.F,
apply eq_of_subset_of_subset,
intro p1,
intros,
trivial,
intro p1,
intros,
dsimp at *,
apply P.cover,
unfold set.pairwise_disjoint,
unfold set.pairwise_on,
intros,
unfold disjoint,
have z : x ∩ y = ∅, apply P.disjoint,
repeat {assumption},
finish,
end
#check function.left_inverse G F -- Prop
example : function.left_inverse G F := sorry --error
```

#### Yury G. Kudryashov (Jun 01 2020 at 02:31):

You need to explicitly provide one of the types: `function.left_inverse (G : partition X → setoid X) F`

.

#### Yury G. Kudryashov (Jun 01 2020 at 02:32):

Otherwise Lean doesn't know that `G`

takes `partition X`

and not `partition Y`

or `partition nat`

.

#### Yury G. Kudryashov (Jun 01 2020 at 02:32):

BTW, we have this equivalence in `mathlib`

, see `data/setoid/partition`

.

#### Bryan Gin-ge Chen (Jun 01 2020 at 02:33):

You may have to update mathlib first, since I see from the code you posted that you're importing `data.setoid`

which was split up a few days ago.

#### Yury G. Kudryashov (Jun 01 2020 at 02:34):

partitions were in `data.setoid`

.

#### Bryan Gin-ge Chen (Jun 01 2020 at 02:36):

Yeah, I guess the code was just moved, not changed.

#### Yury G. Kudryashov (Jun 01 2020 at 02:36):

As `{s // is_partition s}`

.

#### Yury G. Kudryashov (Jun 01 2020 at 02:39):

There were a few minor changes, see #2853

#### Brandon Brown (Jun 01 2020 at 11:03):

I see, thanks! And I'm just doing this for practice which is why I'm not just using the mathlib version.

Last updated: May 12 2021 at 04:19 UTC