The observe tactic.

observe hp : p asserts the proposition p, and tries to prove it using exact?.

def Mathlib.Tactic.LibrarySearch.observe : Lean.ParserDescr

observe hp : p asserts the proposition p as a hypothesis named hp, and tries to prove it using exact?. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p := by exact?.

• observe : p uses the name this for the new hypothesis.
• observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.

def Mathlib.Tactic.LibrarySearch.«tacticObserve?__:_» : Lean.ParserDescr

observe hp : p asserts the proposition p as a hypothesis named hp, and tries to prove it using exact?. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p := by exact?.

• observe : p uses the name this for the new hypothesis.
• observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.

def Mathlib.Tactic.LibrarySearch.«tacticObserve?__:_Using__,,» : Lean.ParserDescr

observe hp : p asserts the proposition p as a hypothesis named hp, and tries to prove it using exact?. If no proof is found, the tactic fails. In other words, this tactic is equivalent to have hp : p := by exact?.

• observe : p uses the name this for the new hypothesis.
• observe? hp : p will emit a trace message of the form have hp : p := proof_term. This may be particularly useful to speed up proofs.