## 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