mathlib

mathlib copied to clipboard

Example

import tactic.apply
import data.set.basic
example {α : Type*} (a b : set α) : a ⊆ b :=
by refl' -- closes the goal
-- by apply' set.subset.refl -- same behavior

Note, the following script shows that refl' (or apply') really makes no progress, and therefore should fail instead.

by { refl', recover, change a ⊆ b, }