-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Pairwise.lean
theorem forall_mem_pwFilter [DecidableRel (α := α) R]
    (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z) (a : α) (l : List α) :
    (∀ b ∈ pwFilter R l, R a b) ↔ ∀ b ∈ l, R a b

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
refine ⟨?_, fun h b hb => h _ <| pwFilter_subset (R := R) _ hb⟩

Result:
α : Type u_1
R : α → α → Prop
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

Proof state:
case cons
α : Type u_1
R : α → α → Prop
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

Tactic:
simp only [forall_mem_cons]

Result:
case cons
α : Type u_1
R : α → α → Prop
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

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
have := find?_some e

Result:
α : Type u_1
R : α → α → Prop
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

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
match e : find? (fun y => ¬R x y) (pwFilter R l) with
| none => exact h.elim fun y hy => by simpa using find?_eq_none.1 e y hy
| some k =>
  have := find?_some e
  apply (neg_trans (H k (mem_of_find?_eq_some e))).resolve_right
  rw [decide_eq_true_iff] at this; exact this

Result:
no goals

Proof state:
case nil
α : Type u_1
R : α → α → Prop
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

Tactic:
exact fun _ _ h => (not_mem_nil _ h).elim

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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 : α
hy : y ∈ pwFilter R l
⊢ R x y

Tactic:
simpa using find?_eq_none.1 e y hy

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
simpa [pwFilter_cons_of_pos h] using fun r H => ⟨r, IH H⟩

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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 : ¬R x k
⊢ ¬R x k

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
induction l with
| nil => exact fun _ _ h => (not_mem_nil _ h).elim
| cons x l IH =>
  simp only [forall_mem_cons]
  if h : ∀ y ∈ pwFilter R l, R x y then
    simpa [pwFilter_cons_of_pos h] using fun r H => ⟨r, IH H⟩
  else
    refine pwFilter_cons_of_neg h ▸ fun H => ⟨?_, IH H⟩
    match e : find? (fun y => ¬R x y) (pwFilter R l) with
    | none => exact h.elim fun y hy => by simpa using find?_eq_none.1 e y hy
    | some k =>
      have := find?_some e
      apply (neg_trans (H k (mem_of_find?_eq_some e))).resolve_right
      rw [decide_eq_true_iff] at this; exact this

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
exact h.elim fun y hy => by simpa using find?_eq_none.1 e y hy

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
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

Tactic:
if h : ∀ y ∈ pwFilter R l, R x y then
  simpa [pwFilter_cons_of_pos h] using fun r H => ⟨r, IH H⟩
else
  refine pwFilter_cons_of_neg h ▸ fun H => ⟨?_, IH H⟩
  match e : find? (fun y => ¬R x y) (pwFilter R l) with
  | none => exact h.elim fun y hy => by simpa using find?_eq_none.1 e y hy
  | some k =>
    have := find?_some e
    apply (neg_trans (H k (mem_of_find?_eq_some e))).resolve_right
    rw [decide_eq_true_iff] at this; exact this

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
refine pwFilter_cons_of_neg h ▸ fun H => ⟨?_, IH H⟩

Result:
α : Type u_1
R : α → α → Prop
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

Proof state:
α : Type u_1
R : α → α → Prop
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

Tactic:
apply (neg_trans (H k (mem_of_find?_eq_some e))).resolve_right

Result:
α : Type u_1
R : α → α → Prop
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