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 : Option Lean.Syntax)
(bis : Array Lean.Syntax)
(t : Option Lean.Syntax)
(keepTerm : Bool)
:

## Equations

- One or more equations did not get rendered due to their size.