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

case neg
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (pwFilter R (x :: l))
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
⊢ Pairwise R (pwFilter R (x :: l))
by_cases h : ∀ y ∈ pwFilter R l, R x y
case pos
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (x :: pwFilter R l)
case pos
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (pwFilter R (x :: l))
rw [pwFilter_cons_of_pos h]
no goals
case pos
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (x :: pwFilter R l)
exact pairwise_cons.2 ⟨h, pairwise_pwFilter l⟩
case neg
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (pwFilter R l)
case neg
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (pwFilter R (x :: l))
rw [pwFilter_cons_of_neg h]
no goals
case neg
α : Type u_1
β : Type ?u.51574
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ Pairwise R (pwFilter R l)
exact pairwise_pwFilter l