a unifier trick

unifier_trick.lean

universes u v
variables {ι : Type u} {α : Type v}

/- the usual definitions of indexed union and intersection -/

def Union (s : ι → set α) : set α := { a | ∃ i, a ∈ s i }
def Inter (s : ι → set α) : set α := { a | ∀ i, a ∈ s i }
notation `⋃` binders `, ` r:(scoped f, Union f) := r
notation `⋂` binders `, ` r:(scoped f, Inter f) := r

/- two simple properties -/

theorem subset_Union (s : ι → set α) (i : ι) : s i ⊆ (⋃ i, s i) :=
λ x xmem, exists.intro i xmem

theorem Inter_subset (s : ι → set α) (i : ι) : (⋂ i, s i) ⊆ s i :=
λ x xmem, xmem i

/- the problem with apply -/

-- works fine
example (s : ι → set α) (t : set α) (i : ι) : (⋂ i, s i ∪ t) ⊆ s i ∪ t :=
by apply Inter_subset

-- fails: the unifier tries the lhs first
example (s : ι → set α) (t : set α) (i : ι) : s i ∪ t ⊆ (⋃ i, s i ∪ t) :=
by apply subset_Union

-- works fine
example (s : ι → set α) (t : set α) (i : ι) : s i ∪ t ⊆ (⋃ i, s i ∪ t) :=
by apply subset_Union _ i

/- workaround for apply: make a version of the theorem that turns the target around -/

theorem Union_supset (s : ι → set α) (i : ι) : (⋃ i, s i) ⊇ s i := subset_Union s i

private meta def by_apply_Union_supset : tactic unit := `[ apply Union_supset ]

theorem subset_Union' (s t : set α) (ts : t ⊇ s . by_apply_Union_supset) : s ⊆ t := ts

example (s : ι → set α) (t : set α) (i : ι) : s i ∪ t ⊆ (⋃ i, s i ∪ t) :=
by apply subset_Union'