Documentation

Mathlib.Tactic.TryThis

Additions to "Try this" support #

This file could be upstreamed to Std.

Add a suggestion for have : t := e.

Instances For

    Add a suggestion for rw [h₁, ← h₂] at loc.

    Instances For