# Documentation

Lean.Meta.Tactic.Assumption

Return a local declaration whose type is definitionally equal to type.

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

Return true if managed to close goal mvarId using an assumption.

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

Close goal mvarId using an assumption. Throw error message if failed.

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