α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise
      (fun a a' =>
        ∀ (b : α),
          b ∈ Option.guard (fun x => decide (p x) = true) a →
            ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) a' → R b b')
      l ↔
    Pairwise (fun x y => p x → p y → R x y) l
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise R (filter (fun b => decide (p b)) l) ↔ Pairwise (fun x y => p x → p y → R x y) l
rw [← filterMap_eq_filter, pairwise_filterMap]
case H
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ ∀ (a b : α),
    (∀ (b_1 : α),
        b_1 ∈ Option.guard (fun x => decide (p x) = true) a →
          ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) b → R b_1 b') ↔
      p a → p b → R a b
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise
      (fun a a' =>
        ∀ (b : α),
          b ∈ Option.guard (fun x => decide (p x) = true) a →
            ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) a' → R b b')
      l ↔
    Pairwise (fun x y => p x → p y → R x y) l
apply Pairwise.iff
case H
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
a✝ b✝ : α
⊢ (∀ (b : α),
      b ∈ Option.guard (fun x => decide (p x) = true) a✝ →
        ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) b✝ → R b b') ↔
    p a✝ → p b✝ → R a✝ b✝
case H
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ ∀ (a b : α),
    (∀ (b_1 : α),
        b_1 ∈ Option.guard (fun x => decide (p x) = true) a →
          ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) b → R b_1 b') ↔
      p a → p b → R a b
intros
no goals
case H
α : Type u_1
β : Type ?u.15897
R S T : α → α → Prop
a : α
l✝ : List α
p : α → Prop
inst✝ : DecidablePred p
l : List α
a✝ b✝ : α
⊢ (∀ (b : α),
      b ∈ Option.guard (fun x => decide (p x) = true) a✝ →
        ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) b✝ → R b b') ↔
    p a✝ → p b✝ → R a✝ b✝
simp only [decide_eq_true_eq, Option.mem_def, Option.guard_eq_some, and_imp, forall_eq']