Theorem: Set.diff_union_eq_union_of_subset (Matroid/ForMathlib/Set.lean)

State before:
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
⊢ s \ t ∪ r = s ∪ r
Tactic:
ext x
State after:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s \ t ∪ r ↔ x ∈ s ∪ r

State before:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s \ t ∪ r ↔ x ∈ s ∪ r
Tactic:
simp only [mem_union, mem_diff]
State after:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s ∧ x ∉ t ∨ x ∈ r ↔ x ∈ s ∨ x ∈ r

State before:
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s ∧ x ∉ t ∨ x ∈ r ↔ x ∈ s ∨ x ∈ r
Tactic:
tauto
State after:
no goals