let vs have vs set vs obtain

Stream: new members

[Dan Abramov]

It took me several months to really appreciate the difference between let, have,set, and obtain. Maybe I was reading the wrong educational resources but I was surprised that this doesn't seem to be centered in explanations despite it being fairly essential.

Here's my current condensed understanding. I'd appreciate any corrections:

• let is the simplest one. It's just giving a local name to a thing. If you have let a := foo, and later you have some expression with a, you can unfold a to "see" that it's "really" foo. You can also include a in simps, like simp only [a], to unfold it. I noticed that sometimes rw and simp on the underlying foo will "pierce through" a anyway but sometimes they won't; I'm not sure why that is, but unfold a will generally always work and you can later try removing it.

• have is like let but more "opaque". You can't unwrap it! It's like it forgets what you put there. So have a := foo now introduces a as its own thing, and you can't ever go back to seeing it as a foo. If you need to unwrap that connection later, don't use have — use let. This is handy for "forgetting" unnecessary details. It's also why have is often used for proofs since the internals of a proof should never matter (even though technically a proof is just another value). Again, you can't unwrap have, that's why putting it in unfold or simp won't work. It's also why, if you declare objects with have, you risk "forgetting" some of their properties you might need for later.

• set ... I'm actually not sure it does anything special compared to let when you just do set a := foo. I used to think it does something special (compared to have) but that was before I learned about let. So now I just assume it's like let but also has some additional syntax (set ... with ...) which I've never needed so far.

• obtain is, from what I understand, like have but it gets rid of the stuff it "consumes". So obtain ⟨h1, h2⟩ := h will remove h from the context. So it's nice for keeping the tactic state clean. Other than that I presume it has no differences from let.

All of the above is in the tactic mode. In term mode, my understanding is that:

• let is (mostly?) same as above.
• have is (mostly?) same as above.
• set and obtain don't exist.

---

As a meta-comment, I think it's interesting that there is no obvious place to read about all of these and compare them. Yes, TPIL explains this in a few places, but you have to dig for these comparisons, and they're pretty deep in the book.

In a programming language tutorial, a distinction like this would be one of the first things being discussed. IMO the fact that I only managed to learn about these a few months in (by explicitly googling it) and it turned out to be so crucial (I didn't understand how important unfold-ability of let is) means it probably wouldn't hurt to push this explanation way up in common resources. For example, maybe MIL could explain this better. That's feedback for MIL though.

Is the understanding above mostly correct? Did I misrepresent anything?

Thanks!

[Kenny Lau]

@Dan Abramov I should say that actually if you hover over them, it gives you some sort of description of what they do

[Kenny Lau]

import Mathlib.Tactic

example : True := by
  let n := 7
  have m := 7
  set p := 7
  trivial

[Kenny Lau]

image.png

[Kenny Lau]

Here are the docstrings:

The let tactic is for adding definitions to the local context of the main goal.

• let x : t := e adds the definition x : t := e if e is a term of type t.
• let x := e uses the type of e for t.
• let : t := e and let := e use this for the name of the hypothesis.
• let pat := e for a pattern pat is equivalent to match e with | pat => _,
  where _ stands for the tactics that follow this one.
  It is convenient for types that let only one applicable constructor.
  For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the
  local variables x : α, y : β, and z : γ.

[Kenny Lau]

The have tactic is for adding hypotheses to the local context of the main goal.

• have h : t := e adds the hypothesis h : t if e is a term of type t.
• have h := e uses the type of e for t.
• have : t := e and have := e use this for the name of the hypothesis.
• have pat := e for a pattern pat is equivalent to match e with | pat => _,
  where _ stands for the tactics that follow this one.
  It is convenient for types that have only one applicable constructor.
  For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the
  hypotheses h₁ : p, h₂ : q, and h₃ : r.

[Kenny Lau]

set a := t with h is a variant of let a := t. It adds the hypothesis h : a = t to
the local context and replaces t with a everywhere it can.

set a := t with ← h will add h : t = a instead.

set! a := t with h does not do any replacing.

example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
  set y := x with ← h2
  sorry
/-
x : Nat
y : Nat := x
h : y + y - y = 3
h2 : x = y
⊢ y + y - y = 3
-/

[Kenny Lau]

I will agree with you that the docstrings for let vs have are a bit subtle, but the key points are there:

• let adds a definition, and have adds a hypothesis, this information is in the first sentences of the docstrings

[Kenny Lau]

The obtain tactic is a combination of have and rcases. See rcases for
a description of supported patterns.

obtain ⟨patt⟩ : type := proof

is equivalent to

have h : type := proof
rcases h with ⟨patt⟩

If ⟨patt⟩ is omitted, rcases will try to infer the pattern.

If type is omitted, := proof is required.

[Kenny Lau]

so obtain allows you to do case matching, and the other three don't

[Dan Abramov]

Thanks! I did read through all of those.

Personally I find “adds a defintion” vs “adds a hypothesis” more confusing than helpful. Them being introduced like this is actually one of the main causes of my overall confusion.

It’s just untrue. You’re perfectly able to define hypotheses (which I understand as terms whose type is some prop) via let. One is also perfectly able to define arbitrary bindings like have a : Nat := 1 with have (so have seems to have no actual semantics related to hypotheses).

What these allude to seem to be assumptions about common usage (“if you define proofs via have and other things via let, you’ll follow the intended usage and run into fewer problems”). But since they don’t explain the critical bit (use have when you want an opaque definition, use let when you want an unfoldable definition, use unfold to pierce through a let). This information seems critical to me and it actually explains why have is used for proofs.

Hope that makes sense.

[Dan Abramov]

Maybe another way to phrase it: I think let should be taught together with unfold. It’s crucial to understand both to be able to progress in a proof. One undoes what the other does (at least in InfoView).

Then when have is first taught, it can be noted that unfold doesn’t work with it. That explains why it’s different from let. There’s no point to unfolding proofs so this also explains why have is used for proofs.

I’m maybe slightly exaggerating (okay, not the first explanation, but maybe the first chapter). But this connection between defining and unfolding and opaqueness was competently lost on me until I started googling precisely this thing.

[Dan Abramov]

Another point is that Lean has a bunch of ways to do the same thing that accommodate different writing styles or are baggage from past versions. So it’s hard to guess that let and have are actually subtly different and aren’t just two conventional words that mathematicians like to use for definitions and theorems.

[Kenny Lau]

Dan Abramov said:

you’ll follow the intended usage and run into fewer problems

but this is true

[Kenny Lau]

I think teaching the intended usage is more important than teaching all the details

[Dan Abramov]

Should there be a linter that disallows declaring proofs with let? And non-proofs with have? Or are there legit exceptions?

[Aaron Liu]

no???

[Dan Abramov]

(typo)

[Aaron Liu]

oh

[Aaron Liu]

yeah it's still no

[Aaron Liu]

sometimes I have data because I don't want to look inside

[Julian Berman]

The docstring Kenny quoted mentions this but just to call it out again explicitly --

set ... I'm actually not sure it does anything special compared to let when you just do set a := foo. I used to think it does something special (compared to have) but that was before I learned about let. So now I just assume it's like let but also has some additional syntax (set ... with ...) which I've never needed so far.

set is "give a name to an expression, and also update all the spots that that expression appears throughout the goal state anywhere". So it does something special to other hypotheses other than the new one that is being added by using set. (It's convenient for giving a name to something you decide you need at some point through a proof, and then simultaneously ensuring that all the spots the expression already appears in immediately use the new name you gave it.)

[Aaron Liu]

this also stops the typechecker from getting stuck trying to unfold it since it shouldn't need to do that

[Dan Abramov]

Btw I generally agree that teaching intended usage is important but I also think “unfolding” and opaqueness are part of “intended usage” and not just implementation details.

[Dan Abramov]

Thanks @Julian Berman, now I remember that’s what I used to think it does! But for some reason I couldn’t always get it working consistently, and then I thought I misunderstood. I’ll need to check if I can repro…

[Julian Berman]

Also on obtain -- and I always forget whether this is 100% accurate or not so Aaron may remind me I'm wrong -- but I think obtain (== rcases) supports all the things have does, plus additional patterns-- though not the ones you mentioned, that one have can do too. But e.g. compare:

example (p : a ∧ b) : 37 = 37 := by
  have ⟨x, y⟩ := p
  rfl

example (p : a ∨ b) : 37 = 37 := by
  obtain x | y := p
  rfl
  rfl

(where have cannot do the case split from the second one if you try changing to have).

So yeah (unless I'm forgetting something which someone will point out) have is "pointless", obtain dominates it as a tactic, but have is the lower level tactic so it doesn't go away, and clearly it's still ubiquitous.

[Johan Commelin]

have and obtain have slightly non-overlapping patterns: #mathlib4 > Is cases' deprecated? @ 💬

[Jireh Loreaux]

Dan Abramov said:

but I also think “unfolding” and opaqueness are part of “intended usage”

For what it's worth I (almost) never unfold anything. More often than not, if you are unfolding, it means you are missing API lemmas.

[Ruben Van de Velde]

Johan Commelin said:

have and obtain have slightly non-overlapping patterns: #mathlib4 > Is cases' deprecated? @ 💬

Yeah, but I still think the ideal outcome would be to merge them and pick one or the other where they don't agree

[Robert Maxton]

Dan Abramov said:

It’s just untrue. You’re perfectly able to define hypotheses (which I understand as terms whose type is some prop) via let. One is also perfectly able to define arbitrary bindings like have a : Nat := 1 with have (so have seems to have no actual semantics related to hypotheses).

I mean, it's perfectly true as long as you understand what the difference between a definition and a hypothesis is in Lean. Which I suppose could be explained more clearly. But ultimately, the difference is precisely that a hypothesis is a value-less definition, where the only accessible information is its type; this is definitely sufficient whenever the value is a Prop, is usually sufficient when the value is a typeclass instance, and may be sufficient in misc other cases.

I also agree that unfold is rarely used, though in part that's because simp and simp_rw will do the same thing.

[Johan Commelin]

I was thinking there could be a tactic xyzzy, such that
(syntax very preliminary, please improve!)

xyzzy x : my type := some value  -- let
xyzzy h : my prop := by some proof -- have
xyzzy +opaque x : my type := some value  -- have
xyzzy ⟨a, b⟩ | c := t -- obtain
xyzzy +generalize x := some expr -- generalize/set
xyzzy +generalize (eq := hx) x := some expr -- set x := some expr with hx
xyzzy +generalize (eq := hn) _ | n : Nat := some subexpr -- we don't have a one-liner for this

That last line would be a combination of generalize/set and rcases, where you get two subgoals,

1. hn : 0 = some subexpr -- and the rest of the context has 0 where some subexpr used to be
2. hn : n+1 = some subexpr -- and the rest of the context has n+1 where some subexpr used to be

[Yaël Dillies]

I think it would be very useful also to have a way to combine let/set with clear_value, as it is often the case that one wants to forget the value to be able to eg do induction on the new variable

[Yaël Dillies]

set foo := bar with foo_eq_bar
clear_value foo

is halfway between let foo := bar and have foo := bar, in the sense that foo isn't defeq to bar, but you still have foo = bar in context

[Yaël Dillies]

To me, this is what xyzzy +opaque x : my type := some value could mean

[suhr]

By the way, why would you prefer have over let? Why is forgetting definitions useful?

[Etienne Marion]

To me this is a bit like asking "why use theorem instead of def?" Remembering a proof is useless because all proofs are equal so it’s just noise, have is cleaner.

[suhr]

That's a not a very convincing explanation. Even though proofs are irrelevant, why would you need to actively forget them?

[Etienne Marion]

You don’t need, it’s just nicer.

[Damiano Testa]

Dan Abramov said:

Should there be a linter that disallows declaring proofs with let? And non-proofs with have? Or are there legit exceptions?

There is half of such a linter, it is just not active by default:

import Mathlib.Tactic

set_option linter.haveLet 2

example : True := by
  let n := 7
  have m := 7
  set p := 7
  trivial

[Damiano Testa]

The linter warns you when have is used for a non-Prop.

The linter has 3 behaviours:

0. set_option linter.haveLet 0 means that the linter says nothing;
1. set_option linter.haveLet 1 means that the linter warns on have introducing a non-Prop, but only in incomplete proofs.
2. set_option linter.haveLet 2 means that the linter warns on have introducing a non-Prop, regardless of whether the proof is complete or not.

The "normal" behaviour of the linter, were it not set to 0, would be 1.

[Johan Commelin]

Yaël Dillies said:

To me, this is what xyzzy +opaque x : my type := some value could mean

Plus the (eq := foo_eq_bar) option (modulo syntax improvements).

[Dan Abramov]

Thanks for the discussion! I want to clarify a few points.

First, I want to clarify the reason for my posting. I have a fair amount of experience programming and I found this distinction confusing and under-explained. Or rather, explained in a way that doesn't make the consequences clear and that caused me to stumble in proofs. I try to report things like these because, having been on the other end (having worked on developer tooling), stumbling blocks like this are easy to forget as you get deeper into practice. So they're underreported: beginners don't know that they misunderstand something, and experienced people don't remember that they ever misunderstood it. I try to report confusing things while I still remember they're confusing. This makes me look like a bit of a clown but I hope it's worth bringing up for consideration.

As such, more RTFM-y responses aren't necessarily helpful since I've already RTFM'd; I'm just sharing that more people might be confused by this who wouldn't know to report it, and that it might be worth tweaking early educational materials and/or linters for this. Ideally, the goal is that the next person wouldn't stumble the same exact way as I did.

Now, coming back to the topic, I understand that you're "not supposed" to unfold things. However, this seems more of a "best practices" thing which, in my opinion, builds on top of a good understanding of the syntax and semantics. You can't always learn bottom-up either of course, so it's a balance. But in reality I think there's multiple situations in the beginning of the learning process where unfolding is an important tool:

• Some common things, like Function.Bijective, don't seem to have an "API". I guess you can just constructor on them directly. But if you don't know what to do, unfold is useful to "peek" into it.
• As an exploratory tool, unfold is the equivalent of Cmd+Clicking but it's more convenient because it's applied to the exact thing you already have. I often unfold specific things in specific goals before I decide whether to pursue a certain route. It's much more convenient than doing many clicks (and works much better with more complex hypotheses because I see the result applied inline). I'm not saying I'll keep unfold in the code (I get the importance of an "API"); I'm saying that unfold is a very useful tool for "exploring" what I'm dealing with. I think I can be trusted to use it, and if I say that I find it helpful, it is because it has actually been helpful for me in a way other tools haven't.
• Regardless of the above, I brought up unfold in the context of unfolding my own local bindings, not some library (so the question about it being unidiomatic is irrelevant). My own local bindings don't have an API. In fact, creating that API (even locally) is when the distinction between have and let becomes crucial. Before I understood the actual difference between have and let, it seemed mysterious that sometimes rewrites were able to "pierce through" my bindings and sometimes not. I could pass some things to simp and some I couldn't. Sometimes I'd see a and have no idea how to turn it back into foo. It seemed arbitrary and confusing. What I'm saying is, it took me a while to notice that the choice of let vs have actually has to do with definitions — and that lets are "unfoldable" (whether with unfold, simp, or whatever) while haves are opaque.

To give a more concrete example of what I'm describing, here's a little fragment of the proof:

Screenshot 2025-08-14 at 13.29.01.png

This works fine. But if I change just one line near the top, it no longer works:

Screenshot 2025-08-14 at 13.28.37.png

The fact that the choice of let vs have has the effect that I'm unable to progress on a proof (or even have any idea about how to progress on it — assuming I don't know unfold can unfold a let) is IMO significant. In my learner shoes (yes, I get how it works now; I'm explaining how it felt) it just seems like I'm stuck on the proof. With a programming background, the idea that I can further "peel off" something that "looks like a variable" is just plain weird! It's not how programming works. I understand this is not programming. But I'm saying that, for a programming audience, teaching that definitions are unfoldable together with let seems beneficial. And also teaching that have is opaque around the same time also seems beneficial. Then they won't get stuck like I used to. (When I was a beginner, I was trying to "solve my way out of this" by doing rw [a] which of course doesn't work.)

Finally, I want to note that, while I did RTFM both docstrings, they feel too similar—almost as if they were copy-pasted with a string replace for hypothesis/definition.

Screenshot 2025-08-14 at 13.32.43.png
Screenshot 2025-08-14 at 13.32.48.png

I understand (and support) the desire for consistency. But I do think that one-sentence mention that let is unfoldable (on the let docstring) and that have is opaque (on the have docstring) would have helped here.

Alternatively, like I mentioned, a lint that nudges you the right way in introductory materials (e.g. MIL repo, FM course, etc) would've also worked. But as we see above there's some discussion about whether hiding non-proofs intentionally is sometimes useful. Which is why I thought it might be better addressed educationally.

Also, I want to emphasize again that "use this for definitions, use this for proofs" doesn't feel strong enough of a hint that you can unfold one but not the other. I didn't think this crucial distinction (without understanding which you can get stuck) was obvious, and that's why I'm posting. If Lean was known for always having "one right way" to do each thing, I would agree more that a recommendation (like "have is for proofs") is enough. But given that in Lean, there's a myriad way to do the same thing (rintro vs intro, have vs obtain, cases vs cases' vs rcases vs match, apply vs refine vs exact, constructor vs use), it's not obvious that this particular one is actually a deep distinction that, although you seemingly can use it either way, will bite you half the proof later with no obvious indication of what bit you.

[Dan Abramov]

Yet another option for improving this may be to catch "silly" attempts to rewrite. Since trying to rw it away is the first thing I (and I presume many others) tried.

For example, this:

Screenshot 2025-08-14 at 13.47.37.png

Could have a special-cased error message that suggests "Did you mean to unfold acc?" or such. And then once I try to do that:

Screenshot 2025-08-14 at 13.48.19.png

This error message could be special-case to say something like "Cannot unfold acc because acc is declared with have. Only let bindings can be unfolded."

Then I would have organically learned about both unfold and let/have distinction guided by the tool, at the point where it actually became important.

[Yaël Dillies]

Dan Abramov said:

This error message could be special-case to say something like "Cannot unfold acc because acc is declared with have. Only let bindings can be unfolded."

I am not sure this is technically possible: I do not think the context remembers how a variable entered it

[Aaron Liu]

I think we can do that actually

[Aaron Liu]

since have now produces nondependent ldecls

[Aaron Liu]

instead of cdecls

[Aaron Liu]

docs#Lean.LocalDecl

[Yaël Dillies]

Oh god, that's a hack

[Aaron Liu]

is it?

[Yaël Dillies]

No actually I don't get it, sorry. How do you differentiate

have foo : Nat := 0

from

have ⟨foo⟩ : Nonempty Nat := inferInstance

?

[Aaron Liu]

well one of them is a nondep ldecl and the other one is a cdecl I'm guessing

[Yaël Dillies]

In the second one, it makes no sense to say that have could be replaced by let

[Yaël Dillies]

Aaron Liu said:

well one of them is a nondep ldecl and the other one is a cdecl I'm guessing

Can you try?

[Aaron Liu]

import Lean

example : True := by
  have k : Nat := 0
  have ⟨foo⟩ : Nonempty Nat := inferInstance
  run_tac Lean.Elab.Tactic.withMainContext do
    let lctx ← Lean.getLCtx
    for decl in lctx do
      match decl with
      | .ldecl idx fvarId name type value nondep kind =>
        Lean.logInfo m!"{name} is {repr kind} {bif nondep then "non" else ""}dep ldecl"
      | .cdecl idx fvarId name type binderInfo kind =>
        Lean.logInfo m!"{name} is {repr kind} cdecl"
  trivial

[Kenny Lau]

aha, nice

[Yakov Pechersky]

Again, you can't unwrap have, that's why putting it in unfold or simp won't work.

I think phrasing is a bit confusing. Let's say I had the following tactic

let a := foo
have b := bar
[...]
simp [a] -- expecting to unfold `a` in the goal
simp [b] -- expecting to _use the proposition whose proof I named `b` to simplify_

That is, when one has have b := bar, or often, have b : somePropStatement := bar, then the importance of b isn't in the term that defined it, but rather the _type_ of b. Because the type of b is the proposition we care about, and the term of b is irrelevant, the only important thing about it is that the type is inhabited -- we have a proof of the proposition.

So when one says "putting it in simp won't work" -- these are two very different uses of simp. And the value of have is to provide a fact that some (Prop) type is inhabited, not locally declaring some particular term.

[Jireh Loreaux]

@Dan Abramov sorry if my response seemed like a call to RTFM, it was not intended as such. And I agree, the let / have hovers are far too close to being identical for comfort. I think your suggestion here is a good one. Although honestly, Johan's suggestion to combine everything into "ash krimpul durbatulûk" (i.e., one tool to rule them all) seems like the ideal choice to me, so long as it includes a fantastic docstring!

[Jireh Loreaux]

I've copied Johan's suggestion here: #general > "Missing Tactics" list @ 💬

[Alex Kontorovich]

isn't the difference between let and have the same as the difference between def and theorem? Lean doesn't care how the theorem is proved, just that it's proved (in fact that's essential, so you can use a fact without reference to its proof). But if you def something, you actually need to remember the construction. Same thing with let vs have; the latter can forget the proof, but it's needed for the former.

[Aaron Liu]

yeah it's similar

[Kyle Miller]

Johan Commelin said:

I was thinking there could be a tactic xyzzy, such that [...]

That tactic is called let :-)

Though, to be fair, it just does a subset of what you propose:

• have x : ty := v is let with the +nondep option (let +nondep x : ty := v). Maybe opaque could be a synonym; nondep was chosen since internally a have expression is a "nondependent let", i.e., the body cannot depend on the value of the variable.
• Both let and have support the +generalize option.
• Both let and have support the (eq := h) option to create an equation. If you want multiple cases in the pattern, we have the match tactic, and maybe match should be preferred in that case since it promotes writing structured proofs.

[Kyle Miller]

Yaël Dillies said:

I do not think the context remembers how a variable entered it

You are correct, this is not something we can know in general. There's no guarantee that a "nondep ldecl" will not eventually be turned into a cdecl. Plus, variables can enter the context through tactics in other ways, and we shouldn't expose internal details about the workings of tactics.

There aren't too many ways a variable can enter a context at least, so if someone tries to unfold a variable that doesn't have a value, it's reasonably safe to give a hint like "if this variable was introduced with have, recall that it is opaque and cannot be unfolded, and perhaps you meant to use let".

[Kyle Miller]

Dan Abramov said:

Should there be a linter that disallows declaring proofs with let? And non-proofs with have? Or are there legit exceptions?

lean4#3559 is an older issue about this. (Mathlib has a linter too, mentioned by Damiano earlier: #new members > let vs have vs set vs obtain @ 💬)

There are legitimate reasons for automation performance to use have as much as possible — but, using have for data can bite you in really confusing ways. What we did in core this year was make Lean responsible for aggressively turning lets into haves, so that way people can comfortably use let for data and have for proofs without having to worry about simp performance implications.

By the way, I just made lean4#9956 to extend the let/have tactic docstrings.

Looking at your screenshots, something that I find interesting to know is that you're finding the keyword have to be meaningful for defining functions. That's something we were debating when we were finalizing what the keywords should be. There were a lot of ideas for possible keywords for them (let, have, const, let_fun, let_dep, nondep_let, opaque, opaque_let, and so on), and there was an argument that no one would ever see "have" in any sense but "having an additional fact", but I thought people would get used to seeing "have" for data, in the more general sense of "having something". That's part of the mnemonic for me: "let x be such-and-such" vs "have x, from such-and-such". The first more actively says that x stands for something else, but the second is that we merely have something, provided there's evidence that such a thing exists.

[Rado Kirov]

Just a +1 as a new comer to theorem proving (but a long time programmer) having very similar experiences to @Dan Abramov . I did accidentally use ‘have’ by habit for a term that should have been ‘let’ and took me a bit of time to debug, but it wasn’t too bad. Docstrings definitely help, but it does feel some of this is so foundational to theorem proving with lean that somewhat surprising it was not in the tutorials I read (or it was there but I didn’t retain it)

[Aaron Liu]

the infoview is your friend

[Aaron Liu]

when you use let the infoview shows a hypothesis that look like name : type := value but when you use have the infoview shows name : type with no value

[Aaron Liu]

this has helped me catch problems with let vs have twice

[Dan Abramov]

I realized part of the reason I picked up bad habit of using have for data is because I often do have := ... for messing around with tactic state (before I commit to naming things) and I can't do let := (that's a syntax error) so I just started doing have := on everything.

[Aaron Liu]

is let := still a syntax error?

[Aaron Liu]

I thought the name was changed to be optional

[Dan Abramov]

Oh nice! I'm on an old version it seems