Subdivision-aware Bound Proving

The interval_bound_subdiv tactic uses interval subdivision when the direct approach fails.

def LeanCert.Tactic.Auto.tacticInterval_bound_subdiv__ : Lean.ParserDescr

The interval_bound_subdiv tactic.

Equations

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