Theorem: finset_partition (Ray/Misc/Bounds.lean)

State before:
A B : Finset ℕ
⊢ A = A \ B ∪ A ∩ B
Tactic:
apply Finset.ext
State after:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A \ B ∪ A ∩ B

State before:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A \ B ∪ A ∩ B
Tactic:
simp only [Finset.mem_union, Finset.mem_sdiff, Finset.mem_inter]
State after:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A ∧ a ∉ B ∨ a ∈ A ∧ a ∈ B

State before:
case a
A B : Finset ℕ
⊢ ∀ (a : ℕ), a ∈ A ↔ a ∈ A ∧ a ∉ B ∨ a ∈ A ∧ a ∈ B
Tactic:
intro x
State after:
case a
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ↔ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

State before:
case a
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ↔ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
constructor
State after:
case a.mp
A B : Finset ℕ
x : ℕ
⊢ x ∈ A → x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

case a.mpr
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B → x ∈ A

State before:
case a.mp
A B : Finset ℕ
x : ℕ
⊢ x ∈ A → x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
intro a
State after:
case a.mp
A B : Finset ℕ
x : ℕ
a : x ∈ A
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

State before:
case a.mp
A B : Finset ℕ
x : ℕ
a : x ∈ A
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
by_cases b : x ∈ B
State after:
case pos
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

case neg
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B

State before:
case pos
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
right
State after:
case pos.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∈ B

State before:
case pos.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∈ B
⊢ x ∈ A ∧ x ∈ B
Tactic:
use a,b
State after:
no goals

State before:
case neg
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
Tactic:
left
State after:
case neg.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B

State before:
case neg.h
A B : Finset ℕ
x : ℕ
a : x ∈ A
b : x ∉ B
⊢ x ∈ A ∧ x ∉ B
Tactic:
use a,b
State after:
no goals

State before:
case a.mpr
A B : Finset ℕ
x : ℕ
⊢ x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B → x ∈ A
Tactic:
intro h
State after:
case a.mpr
A B : Finset ℕ
x : ℕ
h : x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
⊢ x ∈ A

State before:
case a.mpr
A B : Finset ℕ
x : ℕ
h : x ∈ A ∧ x ∉ B ∨ x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
cases' h with m m
State after:
case a.mpr.inl
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∉ B
⊢ x ∈ A

case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A

State before:
case a.mpr.inl
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∉ B
⊢ x ∈ A

case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
repeat exact m.1
State after:
no goals

State before:
case a.mpr.inr
A B : Finset ℕ
x : ℕ
m : x ∈ A ∧ x ∈ B
⊢ x ∈ A
Tactic:
exact m.1
State after:
no goals