# Zulip Chat Archive

## Stream: new members

### Topic: supply implicit argument?

#### abaaba (Oct 22 2021 at 02:52):

`nat.one_div_pos_of_nat {n : ℕ} : 0 < 1 / (n + 1 : ℝ)`

, the only argument is implicit. How should I use it?

#### abaaba (Oct 22 2021 at 02:52):

`have triv : 0 < 1 / (N + 1) := by nat.one_div_pos_of_nat N,`

doesn't work, neither does `have triv : 0 < 1 / (N + 1) := by nat.one_div_pos_of_nat,`

#### Kevin Buzzard (Oct 22 2021 at 02:55):

Kill the `by`

, you don't want to be in tactic mode if you're supplying the term. And in general we prefer #mwe s in questions because it reduces confusion overall

#### abaaba (Oct 22 2021 at 02:57):

i think it's still not working ... This is the 0074 from tutorial

```
-- 0074
example :
(∀ u : ℕ → ℝ, seq_limit u x₀ → seq_limit (f ∘ u) (f x₀)) →
continuous_at_pt f x₀ :=
begin
-- if forall sequence approaching x0, f(u) approaches f(x0),
-- then f is continuous at x0
by_cases x₀ > 0, {
intro h,
unfold seq_limit at *,
unfold continuous_at_pt at *,
intros ε εg0,
set u: ℕ -> ℝ := λ(n:ℕ), ((x₀ + 1 / (n + 1)):ℝ) with hu, -- STAR have forget definition, only declaration
-- it remains to show seq_limit u x0
have premise := limit_const_add_inv_succ x₀,
specialize h u premise ε εg0,
-- nat.one_div_pos_of_nat {n : ℕ} : 0 < 1 / (n + 1 : ℝ)
-- inv_succ_le_all : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1/(n + 1 : ℝ) ≤ ε
cases h with N h,
unfold seq_limit at premise,
use u N, split,
rw hu,
have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat N,
}
end
```

#### Kevin Buzzard (Oct 22 2021 at 02:59):

What's the error?

#### abaaba (Oct 22 2021 at 03:01):

```
function expected at
nat.one_div_pos_of_nat
term has type
linear_ordered_field.lt 0 (1 / (?m_3 + 1))
Additional information:
/tutorials/src/my_exercises/exercises/09_limits_final.lean:219:36: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
too many arguments
```

#### Kyle Miller (Oct 22 2021 at 03:03):

If you want to explicitly give an implicit argument, put `@`

before the name of the function/theorem. For example, `@nat.one_div_pos_of_nat N`

.

#### Kyle Miller (Oct 22 2021 at 03:04):

Lean can also infer implicit arguments, like

```
have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat
```

should work.

#### abaaba (Oct 22 2021 at 03:04):

Kyle Miller said:

If you want to explicitly give an implicit argument, put

`@`

before the name of the function/theorem. For example,`@nat.one_div_pos_of_nat N`

.

this fails with

```
type mismatch at application
nat.one_div_pos_of_nat
term
N
has type
ℕ : Type
but is expected to have type
Type ? : Type (?+1)
```

#### abaaba (Oct 22 2021 at 03:04):

Kyle Miller said:

Lean can also infer implicit arguments, like

`have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat`

should work.

this fails with

```
invalid type ascription, term has type
0 < 1 / (?m_3 + 1)
but is expected to have type
0 < 1 / (N + 1)
```

#### Kyle Miller (Oct 22 2021 at 03:05):

Could you give the output of the following?

```
#check @nat.one_div_pos_of_nat
```

#### Kyle Miller (Oct 22 2021 at 03:05):

(Put this on a line outside the theorem you're proving.)

#### abaaba (Oct 22 2021 at 03:06):

Kyle Miller said:

Could you give the output of the following?

`#check @nat.one_div_pos_of_nat`

```
nat.one_div_pos_of_nat : ∀ {α : Type u_1} [_inst_1 : linear_ordered_field α] {n : ℕ}, 0 < 1 / (n + 1)
```

#### Kyle Miller (Oct 22 2021 at 03:07):

Ok, so this is saying it has three implicit arguments, not just one, which is what caused the earlier type mismatch.

#### Kyle Miller (Oct 22 2021 at 03:08):

Let's ignore that for a moment, since I expect this should work:

```
have triv: 0 < 1 / (N + 1 : ℝ) := nat.one_div_pos_of_nat
```

(Sorry I haven't tried it.)

#### Kyle Miller (Oct 22 2021 at 03:09):

I think the problem was that `N + 1`

is a natural number by default, but we need to tell Lean we expect it to be a real number.

#### abaaba (Oct 22 2021 at 03:10):

it indeed worked :joy:

#### abaaba (Oct 22 2021 at 03:12):

and also the `@nat.one_div_pos_of_nat _ _ N`

worked too once the `:\R`

added to 1 + N

#### Kyle Miller (Oct 22 2021 at 03:13):

Yep, Lean is solving for that `N`

automatically in the implicit version. You should also be able to put `\R`

in for the first underscore if you wanted to be more explicit.

#### Kyle Miller (Oct 22 2021 at 03:14):

(or if you wanted to write `have triv := @nat.one_div_pos_of_nat ℝ _ N`

))

#### Patrick Massot (Oct 22 2021 at 06:31):

@abaaba all those explanations are good to know, but the intended use in the tutorial is to write

```
have triv: 0 < 1 / (N + 1 : ℝ) := nat.one_div_pos_of_nat,
```

as in the indication.

#### Patrick Massot (Oct 22 2021 at 06:32):

That being said, `nat.one_div_pos_of_nat`

should have `n`

as an explicit argument. The library should be fixed.

Last updated: Dec 20 2023 at 11:08 UTC