how to _really_ use `let`

Stream: general

[Eric Rodriguez]

let is often confusing me, for example in the same way that Manuel is confused in this comment chain, but sometimes even simp struggles with it:

import tactic

example {α : Type*} (a : α) [decidable_eq α] (arr : α → option α) : false :=
begin
  let f := λ t : α → option α, λ k, (λ x : α, if x = a then k else t x),
  suffices : function.injective (f arr), by sorry,
  intros x y h, rw function.funext_iff at h, specialize h a,
  -- DOESN'T WORK:
  -- simp only [f, if_true, eq_self_iff_true] at h, assumption
  -- this line effectively does `simp only [f]`
  -- DOES WORK:
  simp only [f] at h, simp only [if_true, eq_self_iff_true] at h, assumption
end

Is there a way to work more harmoniously with let?

[Eric Wieser]

The unhelpful answer here is "make a standalone definition instead". The nice thing about that answer in this case is that that definition already exists, its docs#function.update.

[Eric Rodriguez]

is there much disadvantage to using a dite when an ite will do? (in the way function.update does)

[Mario Carneiro]

function.update uses dite because it supports a dependent function type

[Mario Carneiro]

In your case the function is not dependent so ite is fine

[Mario Carneiro]

but if you are reusing function.update I wouldn't worry about the distinction

[Eric Wieser]

Note the implementation of function.update is:

/-- Replacing the value of a function at a given point by a given value. -/
def update (f : Πa, β a) (a' : α) (v : β a') (a : α) : β a :=
if h : a = a' then eq.rec v h.symm else f a

so the h is used

[Horatiu Cheval]

Are lets in general safe to use in definitions you intend to reason about or should they be avoided? I had cases where some lets would appear in proofs after some simplifications, but eventually they simplified out, but I'm still worried at some point I might get a let that gets more significantly in the way.

[Yakov Pechersky]

It's hard to rewrite across a let.