# Zulip Chat Archive

## Stream: general

### Topic: intro vs assume

#### Siyuan Yan (Nov 03 2022 at 21:12):

what's the difference? Here's what's from the tutorial of mathlib, demonstrating two ways of proving the same thing. In the first example there's `intro h`

and it can be changed to `assume h`

. But the second `assume h`

can't be changed to intro h.

```
lemma le_of_le_add_eps {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
-- Let's prove the contrapositive, asking Lean to push negations right away.
contrapose!,
-- Assume `h : x < y`.
intro h,
-- We need to find `ε` such that `ε` is positive and `x + ε < y`.
-- Let's use `(y-x)/2`
use ((y-x)/2),
-- we now have two properties to prove. Let's do both in turn, using `linarith`
split,
linarith,
linarith,
end
/-
Next we will study a compressed version of that proof:
-/
example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
contrapose!,
exact assume h, ⟨(y-x)/2, by linarith, by linarith⟩,
end
```

#### Adam Topaz (Nov 03 2022 at 21:27):

When you write `exact ...`

the `...`

needs to be the exact term that solves the goal in question. `intro`

is a tactic and cannot be used in term-mode. You can replace `assume`

with a lambda if you want.

#### Adam Topaz (Nov 03 2022 at 21:29):

I guess `assume`

is also a tactic. I don't think anyone actually uses `assume`

in real life (i.e. outside of the tutorials). We usually use lambdas or `intro(s)`

.

#### Eric Rodriguez (Nov 03 2022 at 21:43):

Adam Topaz said:

I guess

`assume`

is also a tactic. I don't think anyone actually uses`assume`

in real life (i.e. outside of the tutorials). We usually use lambdas or`intro(s)`

.

`assume`

is used like ~700+ times in mathlib, and in fact I think a few people are in favour of keeping those and not removing them

#### Adam Topaz (Nov 03 2022 at 21:45):

How many times does mathlib use `intro/intros/rintro/rintros`

?

#### Adam Topaz (Nov 03 2022 at 21:45):

I bet the number of `assume`

s is infinitesimal compared to those

#### Adam Topaz (Nov 03 2022 at 21:46):

I don't think `assume`

should be removed, I'm just saying that people usually forget about `assume`

pretty quickly once they actually start using Lean

#### Junyan Xu (Nov 03 2022 at 21:59):

I think they're mostly used in term mode; did people back then have trouble typing λ? :joy:

#### Eric Wieser (Nov 03 2022 at 22:10):

`assume`

is also a synonym for `fun`

and `λ`

#### Reid Barton (Nov 04 2022 at 05:57):

It used to be a stylistic thing to use `assume`

in proofs and `λ`

in functions, I think

#### Kalle Kytölä (Nov 04 2022 at 07:15):

Hopefully the answers above settled the original question (tactic vs term mode and lots of synonyms), but I would still add two comments.

In tactic mode `intros`

and `assume`

seem to behave completely identically; in particular they can do multiple introductions/assumptions at a time, whereas `intro`

only does one at a time.

As a stylistic matter, reiterating Reid's point above, I find it very strange when people "assume data". In teaching math with Lean (rather than teaching Lean) I would (try to) be very careful to only ever use `assume`

when the assumption is a `Prop`

, and I would use `intro/intros`

where mathematicians would write "let x be something" (data). In the converse direction, I do realize that in logic `intro/intros`

makes sense also for `Prop`

s as an introduction rule for connectives/quantifies, but this does not in my opinion correspond to pen-and-paper math use, so in teaching I'd have a preference for `assume`

for propositions. In mathlib, on the other hand, I think using `intro/intros`

throughout is commonplace and makes a lot of sense (we buy into Curry-Howard or understand the logic etymology and don't attempt to produce code for direct math pedagogical consumption).

#### Eric Wieser (Nov 04 2022 at 08:43):

In tactic mode `assume`

is closer to `rintro`

than to `intro`

; it let's you specify the type of the thing being introd as `assume a : A`

, with semantics `intro a, change A at a`

#### Mario Carneiro (Nov 04 2022 at 13:22):

Also, `assume`

(in both term and tactic mode) has an additional feature not shared with `intro`

/ `\lam`

: you can omit the identifier and it is named `this`

. So `assume A, e`

or `assume A,`

as a tactic mean the same as `λ this : A, e`

or `rintro (this : A),`

respectively

#### Eric Wieser (Nov 04 2022 at 13:25):

I assume you meant `assume : A`

, `assume A`

means "call the variable A"

#### Mario Carneiro (Nov 04 2022 at 13:28):

ah, yes I forget the syntax since I never use it :see_no_evil:

Last updated: Aug 03 2023 at 10:10 UTC