# Zulip Chat Archive

## Stream: new members

### Topic: typing error for ⊆

#### Justus Springer (Mar 18 2021 at 18:15):

Hello!

I'm currently learning lean and when playing around with basic properties of sets and images, I encountered a behavior which I find strange:

```
import data.set.basic
variables (X Y : Type) (f : X → Y)
open set
-- (1) works
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
begin
split,
{ intros h x hxS,
exact h (mem_image_of_mem f hxS) },
{ rintros h y ⟨x, hxS, hfx⟩,
rw ← hfx,
exact h hxS,
}
end
-- (2) works
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
begin
split,
{ exact λ h x hxS, h (mem_image_of_mem f hxS) },
{ exact λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS, }
end
-- (3) doesn't work: "function expected at h, term has type f '' S ⊆ T"
/-
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩
-/
-- (4) works (??)
example (S : set X) (T : set Y) : f '' S ⊆ T → S ⊆ f⁻¹' T :=
λ h x hxS, h (mem_image_of_mem f hxS)
```

I tried to incrementally translate the tactic-style proof of (1) into a term-proof. However, example (3), which I believed to be a quite canonical translation of (2) into a term proof, throws me the following error at the application of `h`

:

```
function expected at
h
term has type
f '' S ⊆ T
```

I find this weird because I thought the term `X ⊆ Y`

was _definitionally equal_ to `∀ ⦃a⦄, a ∈ X → a ∈ Y`

, i.e. a function type. Even weirder, when I only prove one implication as in (4), it works fine. Can someone help me understand what's going on here? Thanks!

#### Anne Baanen (Mar 19 2021 at 08:44):

The error goes away if you remind Lean of what you're trying to do:

```
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨show f '' S ⊆ T -> S ⊆ f⁻¹' T, from λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩
```

#### Anne Baanen (Mar 19 2021 at 08:45):

With `set_option pp.all true`

, we can find a metavariable in the type of `h`

:

```
function expected at
h
term has type
@has_subset.subset.{0} (set.{0} Y) ?m_1 (@set.image.{0 0} X Y f S) T
```

#### Anne Baanen (Mar 19 2021 at 08:47):

The metavariable is the `?m_1`

, which means there are some implicit arguments that Lean hasn't figured out by the time it checks that `h`

is a function.

#### Anne Baanen (Mar 19 2021 at 08:49):

If we look at the definition of `has_subset.subset`

, we see that this is the `has_subset (set Y)`

instance, i.e. the definition of "`S \subset T`

for sets is just `∀ {x], x ∈ S -> x ∈ T`

".

#### Anne Baanen (Mar 19 2021 at 08:53):

Why this happen in term mode and not in tactic mode is that the elaborator, which fills in these metavariables, tries to solve problems in a specific order, and apparently this order did not work well for this proof.

#### Justus Springer (Mar 19 2021 at 11:27):

Thank you, that has helped me a lot!

#### Mario Carneiro (Mar 19 2021 at 21:09):

Here's another version that works:

```
theorem T (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩
```

The only difference is that the `example`

is now a `theorem`

#### Mario Carneiro (Mar 19 2021 at 21:10):

The issue is that it hasn't figured out what `has_subset`

instance is being used by the time it sees `h`

being used as a function. This is only a problem when the statement and proof are elaborated together, as happens in `example`

and `def`

Last updated: May 08 2021 at 03:17 UTC