Theorem: Finset.diff_union_subset (FOL/Finset.lean)

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
have s1 : (A ∪ B) \ E = (A \ E) ∪ (B \ E)
State after:
case s1
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E = A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D

State before:
case s1
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
⊢ (A ∪ B) \ E = A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
exact Finset.union_sdiff_distrib A B E
State after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ C ∪ D
Tactic:
trans (A \ E) ∪ (B \ E)
State after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ A \ E ∪ B \ E

α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ C ∪ D

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ (A ∪ B) \ E ⊆ A \ E ∪ B \ E
Tactic:
simp only [s1]
State after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ A \ E ∪ B \ E

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ A \ E ∪ B \ E
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A \ E ⊆ C
h2 : B \ E ⊆ D
s1 : (A ∪ B) \ E = A \ E ∪ B \ E
⊢ A \ E ∪ B \ E ⊆ C ∪ D
Tactic:
exact Finset.union_subset_left_right (A \ E) (B \ E) C D h1 h2
State after:
no goals