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

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ∪ B ⊆ (C ∪ D) \ E
Tactic:
apply Finset.union_subset_iff.mpr
State after:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ (C ∪ D) \ E ∧ B ⊆ (C ∪ D) \ E

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

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

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

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

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ A ⊆ C \ E
Tactic:
exact h1
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C \ E ⊆ (C ∪ D) \ E
Tactic:
apply Finset.sdiff_subset_sdiff
State after:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C ⊆ C ∪ D

case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E

State before:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ C ⊆ C ∪ D
Tactic:
exact Finset.subset_union_left C D
State after:
no goals

State before:
case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E
Tactic:
rfl
State after:
no goals

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

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

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ B ⊆ D \ E
Tactic:
exact h2
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D \ E ⊆ (C ∪ D) \ E
Tactic:
apply Finset.sdiff_subset_sdiff
State after:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D ⊆ C ∪ D

case hvu
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ E ⊆ E

State before:
case hst
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C \ E
h2 : B ⊆ D \ E
⊢ D ⊆ C ∪ D
Tactic:
exact Finset.subset_union_right C D
State after:
no goals