the "have" tactic

Stream: new members

[Sarah El Boustany]

I am working through Mathematics in Lean and I still haven’t grasped how “have” works exactly. In particular, there’s the solution to this example in section 3 of chapter 1:

import MIL.Common
import Mathlib.Data.Real.Basic
namespace C03S03

section
variable (a b : ℝ)

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def FnHasLb (f : ℝ → ℝ) :=
  ∃ a, FnLb f a

variable (f : ℝ → ℝ)

example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f := by
  rintro ⟨a, ha⟩
  rcases h a with ⟨x, hx⟩
  have := ha x
  linarith

I don’t know how to unpack what the "have := ha x" means. How come “have” is followed by “:=“ and not “:” like it usually is?

[Yaël Dillies]

have := ha x is shorthand for have : _ := ha x. In general, the syntax is have name : type := value and means "Let name be the proof of type as provided by value"

[Yaël Dillies]

If you only give value, then Lean can oftentimes recover what type is just from value. This is indeed what's going on in the have name := value syntax

[Arthur Paulino]

It's the second time this question comes up btw

[Sarah El Boustany]

Thank you for the explanation! I'm sorry I missed the original question, I did try searching through the topics but I guess I didn't know exactly what to filter for

[Arthur Paulino]

Oh, I didn't mean you were expected to find the original question, sorry. I'm just saying that #mil doesn't seem to be self-contained enough yet

[Arthur Paulino]

Oh, the tactic have has a comprehensive docstring, which shows up on hover:
image.png

[Sarah El Boustany]

When I hovered over have I wasn't really sure which case have := ha x fell under. Would it be have pat := e then?

[Michael Rothgang]

Hm, that looks like an opportunity to improve the have tactic doc-string!

[Philippe Duchon]

Looks like the have := e version: you provide a value (and let Lean figure out the type) and the name will be the default this.

[Michael Rothgang]

By the way: have you seen the mathlib tactic manual? It has documentation for all mathlib tactics: https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/#tactics
If you want to get an overview of "what tactic could help me here", that might be useful.

[Michael Rothgang]

There is also a cheat sheet, which is a bit more compact: https://leanprover-community.github.io/papers/lean-tactics.pdf

[Sarah El Boustany]

Oh, I hadn't seen that cheatsheet, thank you!