tactic for assoc and comm of Finset unions and subsets

Stream: Is there code for X?

[Kayla Thomas]

I can prove this by various applications of commutativity and associativity lemmas, but I'm curious if there is a tactic that would be simpler.

A B C D: Finset alpha
x: alpha
h1: A ⊆ C ∪ {x}
h2: B ⊆ D ∪ {x}
⊢ A ∪ B ⊆ C ∪ D ∪ {x}

[Kayla Thomas]

(deleted)

[Kayla Thomas]

Similarly

A B C D: Finset alpha
x: alpha
h1: A ⊆ C \ {x}
h2: B ⊆ D \ {x}
⊢ A ∪ B ⊆ C ∪ D \ {x}

[Kevin Buzzard]

IIRC the corresponding questions for Set alpha could be tackled with ext; finish in lean 3, but finish was never ported. How does ext; simp; tauto/aesop do?

Oh hmm that was for equalities; how about reducing the question to "x in this implies x in that" first (probably ext doesn't do this) and then trying the logic tactics?

[Yaël Dillies]

I actually have a tactic idea that would solve those kinds of goals.