can `cc` do apply, assumption?

Stream: general

[Kevin Buzzard]

Should I expect cc to be able to solve this? It doesn't. Is there a tactic which does?

example (X : Type) (U V : set (X × X)) (hUV : U ⊆ V) (d : X → X → ℤ) (ε : ℤ)
  (hεU : ∀ (x y : X), d x y ≤ ε → (x, y) ∈ U) (x y : X)
  (hxy : d x y ≤ ε) :
(x, y) ∈ V :=
begin
  apply hUV,
  apply hεU,
  assumption
end

[Chris Hughes]

tauto

[Kevin Buzzard]

Great, thanks Chris. For years now I have been quite happy to write proofs such as the above, but I am now getting lazy :-)

[Kevin Buzzard]

I thought tauto just did propositional logic goals, but after reading the docstring I now discover that solve_by_elim also closes the goal.

[Kevin Buzzard]

In fact it seems that solve_by_elim was designed specifically to solve this kind of goal. :light_bulb: