Theorem: subset_union_sdiff (Ray/Misc/Finset.lean)

State before:
A B : Finset ℕ
⊢ B ⊆ A ∪ B \ A
Tactic:
rw [Finset.subset_iff]
State after:
A B : Finset ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ B → x ∈ A ∪ B \ A

State before:
A B : Finset ℕ
⊢ ∀ ⦃x : ℕ⦄, x ∈ B → x ∈ A ∪ B \ A
Tactic:
intro x Bx
State after:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∪ B \ A

State before:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∪ B \ A
Tactic:
rw [Finset.mem_union, Finset.mem_sdiff]
State after:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A

State before:
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
by_cases Ax : x ∈ A
State after:
case pos
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A

case neg
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A

State before:
case pos
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
left
State after:
case pos.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A

State before:
case pos.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∈ A
⊢ x ∈ A
Tactic:
exact Ax
State after:
no goals

State before:
case neg
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ A ∨ x ∈ B ∧ x ∉ A
Tactic:
right
State after:
case neg.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ B ∧ x ∉ A

State before:
case neg.h
A B : Finset ℕ
x : ℕ
Bx : x ∈ B
Ax : x ∉ A
⊢ x ∈ B ∧ x ∉ A
Tactic:
exact ⟨Bx, Ax⟩
State after:
no goals