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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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