Let tactic

Stream: new members

[Patrick Johnson]

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]

You can use set if you want hx.

[Kevin Buzzard]

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

[Kyle Miller]

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]

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]

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]

simp has special code for let iirc