# Zulip Chat Archive

## Stream: new members

### Topic: Forced to use @

#### Pontus Sundqvist (Feb 28 2021 at 16:44):

I'm probably missing something really simple here, but is there a way to avoid using `@`

in this situation? Shouldn't Lean see that `a`

can be used?

```
def property_1 (i : ℕ) : Prop := true
def property_2 (i : ℕ) [property_1 i] : Prop := true
-- This does not work
theorem test1 (i : ℕ)
(a : property_1 i)
(b : property_2 i)
: i = i := sorry
-- But this works... is there anyway to avoid having to use `@`?
theorem test2 (i : ℕ)
(a : property_1 i)
(b : @property_2 i a)
: i = i := sorry
```

#### Yakov Pechersky (Feb 28 2021 at 16:48):

Have you read #tpil about explicit, implicit, and typeclass arguments?

#### Pontus Sundqvist (Feb 28 2021 at 16:49):

No... I probably should do that.

#### Yakov Pechersky (Feb 28 2021 at 16:51):

Making the first `def`

a `class`

makes your `test1`

work.

```
class property_1 (i : ℕ) : Prop := true
def property_2 (i : ℕ) [property_1 i] : Prop := true
-- This now works
theorem test1 (i : ℕ)
(a : property_1 i)
(b : property_2 i)
: i = i := sorry
```

#### Yakov Pechersky (Feb 28 2021 at 16:51):

But what's the larger problem? #xy

#### Pontus Sundqvist (Feb 28 2021 at 17:15):

I encountered the problem several times, but an example was in the following code:

```
import data.fintype.basic
import data.matrix.basic
universes u
variables {a b p q : Type u}
[fintype a] [fintype b] [fintype p] [fintype q]
[linear_order a] [linear_order b] [linear_order p] [linear_order q]
def conserves_order
(f : a -> b)
: Prop := ∀ a1 a2, (a1 < a2) ↔ (f a1 < f a2)
def submatrix
(m : matrix a b ℕ)
(f : p -> a) (g : q -> b) [conserves_order f] [conserves_order g] [function.injective f] [function.injective g]
: matrix p q ℕ
:= λ i j, m (f i) (g j)
theorem submatrix_is_minor
(m : matrix a b ℕ)
(f : p -> a) (g : q -> b) [conserves_order f] [conserves_order g] [function.injective f] [function.injective g]
(i : p) (j : q)
: (submatrix m f g) i j = (m.minor f g) i j
-- Lean: failed to synthesize type class instance [at submatrix] for [function.injective/conserves_order f/g]
:= sorry
```

I feel like using the same restrictions on f (and g) in the definition and the theorem should make it obvious that they satisfy the requirements.

#### Pontus Sundqvist (Feb 28 2021 at 17:16):

I should read up on classes, I haven't used them yet.

#### Eric Wieser (Feb 28 2021 at 17:26):

If you're going to put things in square brackets, they need to be tagged with `@[class]`

#### Eric Wieser (Feb 28 2021 at 17:27):

I think what you probably want to do is replace `(f : p -> a) [conserves_order f] [function.injective f]`

with `(f : p ↪o a)`

, docs#order_embedding

Last updated: Dec 20 2023 at 11:08 UTC