# Documentation

Mathlib.Tactic.Have

Uses checkColGt to prevent

have h
exact Nat


From being interpreted as

have h
exact Nat

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.haveLetCore (goal : Lean.MVarId) (name : ) (bis : ) (t : ) (keepTerm : Bool) :
Equations
• One or more equations did not get rendered due to their size.