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

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

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

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

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

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

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

State before:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ 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 : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ C ∪ D
Tactic:
trans D
State after:
α : Type
inst✝ : DecidableEq α
A B C D : Finset α
h1 : A ⊆ C
h2 : B ⊆ D
⊢ B ⊆ D

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

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

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