Theorem: Finset.union_subset_union_left_right (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.union_subset_union_left
State after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ C ⊆ C ∪ D

State before:
case h
α : 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 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.union_subset_union_left
State after:
case h
α : Type
inst✝ : DecidableEq α
A B C D E : Finset α
h1 : A ⊆ C ∪ E
h2 : B ⊆ D ∪ E
⊢ D ⊆ C ∪ D

State before:
case h
α : 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