Easier way to show superset of infinite set is infinite?

Stream: new members

[Patrick Lutz]

I want to show that if $s \subseteq t$ and $s$ is infinite then so is $t$. I can do so as follows

import data.set.finite

example (X : Type) (s : set X) (t : set X) (hst : s ⊆ t) (hs : s.infinite) : t.infinite :=
begin
    revert hs,
    contrapose,
    intro ht,
    have : s.finite := set.finite.subset (show t.finite, by finish) hst,
    tauto,
end

But it's a little annoying, especially if I want to use it in the middle of some other proof. Is there a better way to do this? I don't mind using classical logic btw.

[Patrick Lutz]

Also, in the above example, how can I get contrapose! to give me t.finite → s.finite instead of ¬t.infinite → ¬s.infinite? Once again, I don't mind using classical logic.

[Reid Barton]

Rather than contrapose, you can just apply mt

[Reid Barton]

example (X : Type) (s : set X) (t : set X) (hst : s ⊆ t) (hs : s.infinite) : t.infinite :=
mt (λ ht, ht.subset hst) hs