| [[have-tactic\|have]]`hHypotheses :` _Type_ `:= by` _Proof_by_tactics_ | add hypothesis `hHypotheses` to the context after proving it in tactics mode. | | ---------------------------------------------------------------------- | ----------------------------------------------------------------------------- | | [[have-tactic\|have]]`hHypotheses :` _Type_ `:=` _Proof_by_terms_ | add hypothesis `hHypotheses` to the context after proving it in term mode. | ## Examples - Lean code: - Video: ## Searching for <font color="#de7802">have</font> applications | <font color="#de7802">have?</font> `using h1, h2` | Search for hypothesis that can be concluded by using both `h1` and `h2`. | | | ------------------------------------------------- | ------------------------------------------------------------------------ | --- | ## Meaning and Semantics - **Mathematical Context**: It mirrors the "assert" or "suppose we know that..." step in a paper proof. You prove a smaller statement first before using it to advance the larger proof. - **Lean 4 Semantics**: [[have-tactic|have]]`hHypotheses :` _Type_ `:= by` _Proof_by_tactics_ evaluates the expression _Proof_by_tactics_ to verify it has type _Type_. If successful, it binds the resulting term to the identifier `hHypotheses` in the local context for the remainder of the proof block. If the proof is omitted (<font color="#de7802">have</font> `hHypotheses :` _Type_), Lean creates a new goal for _Type_. ## Related and Opposite Tactics ![[under-construction.png]] ***Under construction*** - **Similar Tactics**: - `let`: Defines a local value or computable expression rather than a logical proposition and proof. - `suffices`: Reverses the proof direction by stating that to prove the goal, it is enough to first prove a new intermediate statement. - `calc`: Organizes a chain of equalities or inequalities step-by-step. [1](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/The-Tactic-Language/) - **Pseudo-opposite Tactics**: - `clear`: Removes a hypothesis from the local context. - `generalize`: Replaces a subterm with a fresh variable, moving a hypothesis backward into a more general form. [1](https://lean-forward.github.io/logical-verification/2018/31_notes.html) --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date`**: 2026-08-20