no goals
case refine'_1
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x => x ∈ t₁) s ∪ filter (fun x => ¬x ∈ t₁) s = s
simp [filter_union_right, em]
case refine'_2
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∈ t₁) s) → x ∈ t₁
case refine'_2
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => x ∈ t₁) s) ⊆ t₁
intro x
no goals
case refine'_2
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∈ t₁) s) → x ∈ t₁
simp
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => ¬x ∈ t₁) s) → x ∈ t₂ \ t₁
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => ¬x ∈ t₁) s) ⊆ t₂ \ t₁
intro x
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → ¬x ∈ t₁ → x ∈ t₂ ∧ ¬x ∈ t₁
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => ¬x ∈ t₁) s) → x ∈ t₂ \ t₁
simp
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : ¬x ∈ t₁
⊢ x ∈ t₂ ∧ ¬x ∈ t₁
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → ¬x ∈ t₁ → x ∈ t₂ ∧ ¬x ∈ t₁
intro hx hx₂
no goals
case refine'_3
α : Type u_1
β : Type ?u.400981
γ : Type ?u.400984
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : ¬x ∈ t₁
⊢ x ∈ t₂ ∧ ¬x ∈ t₁
refine' ⟨Or.resolve_left (h hx) hx₂, hx₂⟩