case nil
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a : α
⊢ (∀ (b : α), b ∈ pwFilter R [] → R a b) → ∀ (b : α), b ∈ [] → R a b

case cons
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → ∀ (b : α), b ∈ x :: l → R a b
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a : α
l : List α
⊢ (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
induction' l with x l IH
case cons
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
case cons
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → ∀ (b : α), b ∈ x :: l → R a b
simp only [forall_mem_cons]
case pos
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x

case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
case cons
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
by_cases h : ∀ y ∈ pwFilter R l, R x y <;> dsimp at h
no goals
case nil
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a : α
⊢ (∀ (b : α), b ∈ pwFilter R [] → R a b) → ∀ (b : α), b ∈ [] → R a b
exact fun _ _ h => (not_mem_nil _ h).elim
case pos
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ R a x → (∀ (x : α), x ∈ pwFilter R l → R a x) → R a x ∧ ∀ (x : α), x ∈ l → R a x
case pos
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
simp only [pwFilter_cons_of_pos h, forall_mem_cons, and_imp]
no goals
case pos
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ R a x → (∀ (x : α), x ∈ pwFilter R l → R a x) → R a x ∧ ∀ (x : α), x ∈ l → R a x
exact fun r H => ⟨r, IH H⟩
case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R l → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R (x :: l) → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
rw [pwFilter_cons_of_neg h]
case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
⊢ R a x
case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ (∀ (b : α), b ∈ pwFilter R l → R a b) → R a x ∧ ∀ (x : α), x ∈ l → R a x
refine' fun H => ⟨_, IH H⟩
case neg.none
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
e : find? (fun y => decide ¬R x y) (pwFilter R l) = none
⊢ R a x

case neg.some
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
⊢ R a x
case neg
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
⊢ R a x
cases' e : find? (fun y => ¬R x y) (pwFilter R l) with k
case neg.none
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
e : find? (fun y => decide ¬R x y) (pwFilter R l) = none
⊢ ∀ (x_1 : α), x_1 ∈ pwFilter R l → ¬(decide ¬R x x_1) = true → R x x_1
case neg.none
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
e : find? (fun y => decide ¬R x y) (pwFilter R l) = none
⊢ R a x
refine' h.elim (BAll.imp_right _ (find?_eq_none.1 e))
no goals
case neg.none
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
e : find? (fun y => decide ¬R x y) (pwFilter R l) = none
⊢ ∀ (x_1 : α), x_1 ∈ pwFilter R l → ¬(decide ¬R x x_1) = true → R x x_1
exact fun y _ => by simp
no goals
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
e : find? (fun y => decide ¬R x y) (pwFilter R l) = none
y : α
x✝ : y ∈ pwFilter R l
⊢ ¬(decide ¬R x y) = true → R x y
simp
case neg.some
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
this : (decide ¬R x k) = true
⊢ R a x
case neg.some
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
⊢ R a x
have := find?_some e
no goals
case neg.some
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
this : (decide ¬R x k) = true
⊢ R a x
exact (neg_trans (H k (find?_mem e))).resolve_right (by simpa)
no goals
α : Type u_1
β : Type ?u.53307
R S T : α → α → Prop
a✝ : α
l✝ : List α
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
this : (decide ¬R x k) = true
⊢ ¬R x k
simpa