case nil
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
l : List α
p✝ : Pairwise R l
p : Pairwise R []
⊢ pwFilter R [] = []

case cons
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝¹ : List α
inst✝ : DecidableRel R
l✝ : List α
p✝ : Pairwise R l✝
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p : Pairwise R (x :: l)
⊢ pwFilter R (x :: l) = x :: l
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
l : List α
p : Pairwise R l
⊢ pwFilter R l = l
induction' l with x l IH
case cons.intro
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝¹ : List α
inst✝ : DecidableRel R
l✝ : List α
p✝¹ : Pairwise R l✝
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
⊢ pwFilter R (x :: l) = x :: l
case cons
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝¹ : List α
inst✝ : DecidableRel R
l✝ : List α
p✝ : Pairwise R l✝
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p : Pairwise R (x :: l)
⊢ pwFilter R (x :: l) = x :: l
cases' pairwise_cons.1 p with al p
no goals
case cons.intro
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝¹ : List α
inst✝ : DecidableRel R
l✝ : List α
p✝¹ : Pairwise R l✝
x : α
l : List α
IH : Pairwise R l → pwFilter R l = l
p✝ : Pairwise R (x :: l)
al : ∀ (a' : α), a' ∈ l → R x a'
p : Pairwise R l
⊢ pwFilter R (x :: l) = x :: l
rw [pwFilter_cons_of_pos (BAll.imp_left (pwFilter_subset l) al), IH p]
no goals
case nil
α : Type u_1
β : Type ?u.52180
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
l : List α
p✝ : Pairwise R l
p : Pairwise R []
⊢ pwFilter R [] = []
rfl