case pos
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l

case neg
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
⊢ pwFilter R (x :: l) <+ x :: l
by_cases h : ∀ y ∈ pwFilter R l, R x y
case pos
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ x :: pwFilter R l <+ x :: l
case pos
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l
rw [pwFilter_cons_of_pos h]
no goals
case pos
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ x :: pwFilter R l <+ x :: l
exact (pwFilter_sublist l).cons_cons _
case neg
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R l <+ x :: l
case neg
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l
rw [pwFilter_cons_of_neg h]
no goals
case neg
α : Type u_1
β : Type ?u.50704
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R l <+ x :: l
exact sublist_cons_of_sublist _ (pwFilter_sublist l)