# Zulip Chat Archive

## Stream: new members

### Topic: Let tactic

#### Patrick Johnson (Nov 17 2021 at 21:25):

Documentation seems to be unclear regarding the `let`

tactic. What does it actually do? The `let`

tactic introduces a hypothesis of the form `x : t := v`

. What does it exactly mean? What is the `:=`

operator here? Is it the meta-operator (like in `def`

of something), or is it a term-level syntactic operator defined inductively (like `=`

)? How to use such a hypothesis? Consider this example:

```
example
(P : ℕ → ℕ → Prop)
(h : ∀ (a b : ℕ), P a b ↔ a = b) :
(∃ (f : ℕ → Prop), f 0) ∧ (∃ (f : ℕ → Prop), ¬f 1) :=
begin
let f := λ (x : ℕ), P x 0,
split,
use f,
simp only [f],
exact (h 0 0).mpr rfl,
use f,
simp only [f],
intro h1,
exact one_ne_zero ((h 1 0).mp h1),
end
```

Is the `simp only [f]`

preferred way to use such hypothesis? Why do `rw`

and `unfold`

fail? Is there a way to split

```
x : t := v
```

into two hypothesis

```
x : t
hx : x = v
```

#### Kevin Buzzard (Nov 17 2021 at 21:26):

You can use `set`

if you want `hx`

.

#### Kevin Buzzard (Nov 17 2021 at 21:27):

`set f := λ (x : ℕ), P x 0 with hf,`

#### Kyle Miller (Nov 17 2021 at 21:46):

The `let`

tactic constructs a `let ... in ...`

expression. Modulo some details, its effect is as if you turned

```
begin
let f := foo,
...
end
```

into

```
let f := foo
in begin
...
end
```

#### Kyle Miller (Nov 17 2021 at 21:47):

I'm not sure why `simp only [f]`

works but `rw f`

doesn't. I think it has something to do with the fact that `f`

is only `let`

-bound so doesn't have the "equation lemmas" that definitions get.

#### Kyle Miller (Nov 17 2021 at 21:50):

In the goal window, `x : t := v`

is just how it writes a hypothesis that actually knows its value (unlike a hypothesis from an argument, or a hypothesis from `have`

that intentionally forgets its value). It's supposed to represent the `:=`

in a `let`

or a `def`

.

#### Eric Rodriguez (Nov 17 2021 at 22:06):

simp has special code for let iirc

Last updated: Dec 20 2023 at 11:08 UTC