[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
n : ℕ
h : Pairwise R (a :: l)
⊢ Pairwise R (List.drop (n + 1) (a :: l))
[PROOFSTEP]
rw [List.drop]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
n : ℕ
h : Pairwise R (a :: l)
⊢ Pairwise R (List.drop n l)
[PROOFSTEP]
exact Pairwise.drop (pairwise_cons.mp h).right
[GOAL]
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ : List α
S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b
p : Pairwise R l
⊢ Pairwise S l
[PROOFSTEP]
induction p with
| nil => constructor
| @cons a l r _ ih =>
  constructor
  · exact BAll.imp_right (fun x h ↦ H (mem_cons_self _ _) (mem_cons_of_mem _ h)) r
  · exact ih fun {a b} m m' ↦ H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
[GOAL]
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ : List α
S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b
p : Pairwise R l
⊢ Pairwise S l
[PROOFSTEP]
induction p with
| nil => constructor
| @cons a l r _ ih =>
  constructor
  · exact BAll.imp_right (fun x h ↦ H (mem_cons_self _ _) (mem_cons_of_mem _ h)) r
  · exact ih fun {a b} m m' ↦ H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ : List α
S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []
[PROOFSTEP]

| nil => constructor
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ : List α
S : α → α → Prop
l : List α
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)
[PROOFSTEP]

| @cons a l r _ ih =>
  constructor
  · exact BAll.imp_right (fun x h ↦ H (mem_cons_self _ _) (mem_cons_of_mem _ h)) r
  · exact ih fun {a b} m m' ↦ H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)
[PROOFSTEP]
constructor
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'
[PROOFSTEP]
exact BAll.imp_right (fun x h ↦ H (mem_cons_self _ _) (mem_cons_of_mem _ h)) r
[GOAL]
case cons.a
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a✝¹ : α
l✝¹ : List α
S : α → α → Prop
l✝ : List α
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l
[PROOFSTEP]
exact ih fun {a b} m m' ↦ H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
x✝ : Pairwise R l ∧ Pairwise S l
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l
[PROOFSTEP]
induction' hR with a l R1 R2 IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
x✝¹ : Pairwise R l ∧ Pairwise S l
hS✝ : Pairwise S l
x✝ : Pairwise R [] ∧ Pairwise S []
hS : Pairwise S []
⊢ Pairwise (fun a b => R a b ∧ S a b) []
[PROOFSTEP]
simp only [Pairwise.nil, pairwise_cons] at *
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
x✝¹ : Pairwise R l✝ ∧ Pairwise S l✝
hS✝ : Pairwise S l✝
a : α
l : List α
R1 : ∀ (a' : α), a' ∈ l → R a a'
R2 : Pairwise R l
IH : Pairwise R l ∧ Pairwise S l → Pairwise S l → Pairwise (fun a b => R a b ∧ S a b) l
x✝ : Pairwise R (a :: l) ∧ Pairwise S (a :: l)
hS : Pairwise S (a :: l)
⊢ Pairwise (fun a b => R a b ∧ S a b) (a :: l)
[PROOFSTEP]
simp only [Pairwise.nil, pairwise_cons] at *
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
x✝¹ : Pairwise R l✝ ∧ Pairwise S l✝
hS✝ : Pairwise S l✝
a : α
l : List α
R1 : ∀ (a' : α), a' ∈ l → R a a'
R2 : Pairwise R l
IH : Pairwise R l ∧ Pairwise S l → Pairwise S l → Pairwise (fun a b => R a b ∧ S a b) l
x✝ : ((∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l) ∧ (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
hS : (∀ (a' : α), a' ∈ l → S a a') ∧ Pairwise S l
⊢ (∀ (a' : α), a' ∈ l → R a a' ∧ S a a') ∧ Pairwise (fun a b => R a b ∧ S a b) l
[PROOFSTEP]
exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH ⟨R2, hS.2⟩ hS.2⟩
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
H : ∀ (x y : α), R x y
⊢ Pairwise R l
[PROOFSTEP]
induction l <;> [exact Pairwise.nil; simp only [*, pairwise_cons, forall₂_true_iff, and_true_iff]]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
H : ∀ (x y : α), R x y
⊢ Pairwise R l
[PROOFSTEP]
induction l
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
H : ∀ (x y : α), R x y
⊢ Pairwise R []
[PROOFSTEP]
exact Pairwise.nil
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
H : ∀ (x y : α), R x y
head✝ : α
tail✝ : List α
tail_ih✝ : Pairwise R tail✝
⊢ Pairwise R (head✝ :: tail✝)
[PROOFSTEP]
simp only [*, pairwise_cons, forall₂_true_iff, and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ a ∈ l ∧ b ∈ l ∧ R a b)
[PROOFSTEP]
simp (config := { contextual := true }) only [true_and_iff, iff_self_iff, forall₂_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ a ∈ l → b ∈ l → R a b)
[PROOFSTEP]
simp (config := { contextual := true }) only [forall_prop_of_true, iff_self_iff, forall₂_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
h₁ : ∀ (x : α), x ∈ l → R x x
h₂ : Pairwise R l
h₃ : Pairwise (flip R) l
⊢ ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
h₁✝ : ∀ (x : α), x ∈ l → R x x
h₂✝ : Pairwise R l
h₃✝ : Pairwise (flip R) l
h₁ : ∀ (x : α), x ∈ [] → R x x
h₂ : Pairwise R []
h₃ : Pairwise (flip R) []
⊢ ∀ ⦃x : α⦄, x ∈ [] → ∀ ⦃y : α⦄, y ∈ [] → R x y
[PROOFSTEP]
exact forall_mem_nil _
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
a : α
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
h₁ : ∀ (x : α), x ∈ a :: l → R x x
h₂ : Pairwise R (a :: l)
h₃ : Pairwise (flip R) (a :: l)
⊢ ∀ ⦃x : α⦄, x ∈ a :: l → ∀ ⦃y : α⦄, y ∈ a :: l → R x y
[PROOFSTEP]
rw [pairwise_cons] at h₂ h₃
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
a : α
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
h₁ : ∀ (x : α), x ∈ a :: l → R x x
h₂ : (∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α⦄, x ∈ a :: l → ∀ ⦃y : α⦄, y ∈ a :: l → R x y
[PROOFSTEP]
simp only [mem_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
a : α
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
h₁ : ∀ (x : α), x ∈ a :: l → R x x
h₂ : (∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
⊢ ∀ ⦃x : α⦄, x = a ∨ x ∈ l → ∀ ⦃y : α⦄, y = a ∨ y ∈ l → R x y
[PROOFSTEP]
rintro x (rfl | hx) y (rfl | hy)
[GOAL]
case cons.inl.inl
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
y : α
h₁ : ∀ (x : α), x ∈ y :: l → R x x
h₂ : (∀ (a' : α), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R y y
[PROOFSTEP]
exact h₁ _ (l.mem_cons_self _)
[GOAL]
case cons.inl.inr
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
x : α
h₁ : ∀ (x_1 : α), x_1 ∈ x :: l → R x_1 x_1
h₂ : (∀ (a' : α), a' ∈ l → R x a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R x a') ∧ Pairwise (flip R) l
y : α
hy : y ∈ l
⊢ R x y
[PROOFSTEP]
exact h₂.1 _ hy
[GOAL]
case cons.inr.inl
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
x : α
hx : x ∈ l
y : α
h₁ : ∀ (x : α), x ∈ y :: l → R x x
h₂ : (∀ (a' : α), a' ∈ l → R y a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R y a') ∧ Pairwise (flip R) l
⊢ R x y
[PROOFSTEP]
exact h₃.1 _ hx
[GOAL]
case cons.inr.inr
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
h₁✝ : ∀ (x : α), x ∈ l✝ → R x x
h₂✝ : Pairwise R l✝
h₃✝ : Pairwise (flip R) l✝
a : α
l : List α
ih : (∀ (x : α), x ∈ l → R x x) → Pairwise R l → Pairwise (flip R) l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
h₁ : ∀ (x : α), x ∈ a :: l → R x x
h₂ : (∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l
h₃ : (∀ (a' : α), a' ∈ l → flip R a a') ∧ Pairwise (flip R) l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
⊢ R x y
[PROOFSTEP]
exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
H : Symmetric R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ : Pairwise R l
⊢ Pairwise (flip fun x => R x) l
[PROOFSTEP]
rwa [H.flip_eq]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
[PROOFSTEP]
apply Pairwise.forall_of_forall
[GOAL]
case H
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun x y => x ≠ y → R x y
[PROOFSTEP]
exact fun a b h hne => hR (h hne.symm)
[GOAL]
case H₁
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x
[PROOFSTEP]
exact fun _ _ hx => (hx rfl).elim
[GOAL]
case H₂
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun x y => x ≠ y → R x y) l
[PROOFSTEP]
exact hl.imp (@fun a b h _ => by exact h)
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
hR : Symmetric R
hl : Pairwise R l
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
R✝ S T : α → α → Prop
a✝ : α
l : List α
R : α → α → Prop
a : α
⊢ Pairwise R [a]
[PROOFSTEP]
simp [Pairwise.nil]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
a b : α
⊢ Pairwise R [a, b] ↔ R a b
[PROOFSTEP]
simp only [pairwise_cons, mem_singleton, forall_eq, forall_prop_of_false (not_mem_nil _), forall_true_iff, Pairwise.nil,
  and_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
[PROOFSTEP]
have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) → ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y :=
  fun l₁ l₂ a x xm y ym ↦ s (a y ym x xm)
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁)
[PROOFSTEP]
simp only [pairwise_append, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
s : Symmetric R
l₁ l₂ : List α
this :
  ∀ (l₁ l₂ : List α), (∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) → ∀ (x : α), x ∈ l₂ → ∀ (y : α), y ∈ l₁ → R x y
⊢ (Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b) ↔
    Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₂ → ∀ (b : α), b ∈ l₁ → R a b
[PROOFSTEP]
rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
s : Symmetric R
a : α
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
[PROOFSTEP]
rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
s : Symmetric R
a : α
l₁ l₂ : List α
⊢ (Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔
    Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b
[PROOFSTEP]
simp only [mem_append, or_comm]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
f : β → α
⊢ Pairwise R (map f []) ↔ Pairwise (fun a b => R (f a) (f b)) []
[PROOFSTEP]
simp only [map, Pairwise.nil]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
f : β → α
b : β
l : List β
⊢ Pairwise R (map f (b :: l)) ↔ Pairwise (fun a b => R (f a) (f b)) (b :: l)
[PROOFSTEP]
simp only [map, pairwise_cons, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, pairwise_map]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
f : β → Option α
l : List β
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l
[PROOFSTEP]
let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b'
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l
[PROOFSTEP]
simp only [Option.mem_def]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
[PROOFSTEP]
induction' l with a l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f []) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') []
[PROOFSTEP]
simp only [filterMap, Pairwise.nil]
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)
[PROOFSTEP]
cases' e : f a with b
[GOAL]
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
e : f a = none
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)
[PROOFSTEP]
rw [filterMap_cons_none _ _ e, propext IH, pairwise_cons]
[GOAL]
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
e : f a = none
⊢ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l ↔
    (∀ (a' : β), a' ∈ l → ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') ∧
      Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
[PROOFSTEP]
simp only [e, forall_prop_of_false not_false, forall₃_true_iff, true_and_iff]
[GOAL]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)
[PROOFSTEP]
rw [filterMap_cons_some _ _ _ e]
[GOAL]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise R (b :: filterMap f l) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)
[PROOFSTEP]
simp only [pairwise_cons, mem_filterMap, forall_exists_index, and_imp, IH, e, Option.some.injEq, forall_eq',
  and_congr_left_iff]
[GOAL]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l →
    ((∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b')
[PROOFSTEP]
intro _
[GOAL]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝¹ : α
l✝ : List α
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
a✝ : Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ (∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b'
[PROOFSTEP]
exact ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [← filterMap_eq_filter, pairwise_filterMap]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply Pairwise.iff
[GOAL]
case H
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
intros
[GOAL]
case H
α : Type u_1
β : Type u_2
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✝
[PROOFSTEP]
simp only [decide_eq_true_eq, Option.mem_def, Option.guard_eq_some, and_imp, forall_eq']
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
p : β → Prop
f : (b : β) → p b → α
l : List β
h : ∀ (x : β), x ∈ l → p x
⊢ Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
[PROOFSTEP]
induction' l with a l ihl
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
p : β → Prop
f : (b : β) → p b → α
l : List β
h✝ : ∀ (x : β), x ∈ l → p x
h : ∀ (x : β), x ∈ [] → p x
⊢ Pairwise R (pmap f [] h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
[PROOFSTEP]
obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
⊢ p a ∧ ∀ (b : β), b ∈ l → p b
[PROOFSTEP]
simpa using h
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise R (pmap f (a :: l) h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) (a :: l)
[PROOFSTEP]
simp only [ihl hl, pairwise_cons, bex_imp, pmap, and_congr_left_iff, mem_pmap]
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
⊢ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l →
    ((∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a') ↔
      ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂))
[PROOFSTEP]
refine' fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, _⟩
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
⊢ (∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)) →
    ∀ (a' : α) (x : β) (h_1 : x ∈ l), f x (_ : p x) = a' → R (f a (_ : p a)) a'
[PROOFSTEP]
rintro H _ b hb rfl
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝¹ : List α
p : β → Prop
f : (b : β) → p b → α
l✝ : List β
h✝ : ∀ (x : β), x ∈ l✝ → p x
a : β
l : List β
ihl :
  ∀ (h : ∀ (x : β), x ∈ l → p x),
    Pairwise R (pmap f l h) ↔ Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
h : ∀ (x : β), x ∈ a :: l → p x
left✝ : p a
hl : ∀ (b : β), b ∈ l → p b
x✝ : Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
H : ∀ (a' : β), a' ∈ l → ∀ (h₁ : p a) (h₂ : p a'), R (f a h₁) (f a' h₂)
b : β
hb : b ∈ l
⊢ R (f a (_ : p a)) (f b (_ : p b))
[PROOFSTEP]
exact H b hb _ _
[GOAL]
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ Pairwise S (List.pmap f l h)
[PROOFSTEP]
refine' (pairwise_pmap h).2 (Pairwise.imp_of_mem _ hl)
[GOAL]
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → R a b → ∀ (h₁ : p a) (h₂ : p b), S (f a h₁) (f b h₂)
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ S (f a✝³ h₁✝) (f b✝ h₂✝)
[PROOFSTEP]
apply hS
[GOAL]
case a
α : Type u_1
β : Type u_2
R S✝ T : α → α → Prop
a : α
l✝ l : List α
hl : Pairwise R l
p : α → Prop
f : (a : α) → p a → β
h : ∀ (x : α), x ∈ l → p x
S : β → β → Prop
hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)
a✝³ b✝ : α
a✝² : a✝³ ∈ l
a✝¹ : b✝ ∈ l
a✝ : R a✝³ b✝
h₁✝ : p a✝³
h₂✝ : p b✝
⊢ R a✝³ b✝
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
L : List (List α)
⊢ Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
[PROOFSTEP]
induction' L with l L IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
⊢ Pairwise R (join []) ↔
    (∀ (l : List α), l ∈ [] → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) []
[PROOFSTEP]
simp only [join, Pairwise.nil, forall_prop_of_false (not_mem_nil _), forall_const, and_self_iff]
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (l_1 : List α), l_1 ∈ l :: L → Pairwise R l_1) ∧
      Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) (l :: L)
[PROOFSTEP]
have :
  (∀ x : α, x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ a' : List α, a' ∈ L → ∀ x : α, x ∈ l → ∀ y : α, y ∈ a' → R x y :=
  ⟨fun h a b c d e => h c d e a b, fun h c d e a b => h a b c d e⟩
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ Pairwise R (join (l :: L)) ↔
    (∀ (l_1 : List α), l_1 ∈ l :: L → Pairwise R l_1) ∧
      Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) (l :: L)
[PROOFSTEP]
simp only [join, pairwise_append, IH, mem_join, exists_imp, and_imp, this, forall_mem_cons, pairwise_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
L : List (List α)
IH :
  Pairwise R (join L) ↔
    (∀ (l : List α), l ∈ L → Pairwise R l) ∧ Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
this :
  (∀ (x : α), x ∈ l → ∀ (y : α) (x_1 : List α), x_1 ∈ L → y ∈ x_1 → R x y) ↔
    ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y
⊢ (Pairwise R l ∧
      ((∀ (l : List α), l ∈ L → Pairwise R l) ∧
          Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L) ∧
        ∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ↔
    (Pairwise R l ∧ ∀ (l : List α), l ∈ L → Pairwise R l) ∧
      (∀ (a' : List α), a' ∈ L → ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ a' → R x y) ∧
        Pairwise (fun l₁ l₂ => ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₂ → R x y) L
[PROOFSTEP]
simp only [and_assoc, and_comm, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
R✝ S T : α → α → Prop
a : α
l✝ : List α
R : β → β → Prop
l : List α
f : α → List β
⊢ Pairwise R (List.bind l f) ↔
    (∀ (a : α), a ∈ l → Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → R x y) l
[PROOFSTEP]
simp [List.bind, List.pairwise_join, List.mem_map, List.pairwise_map]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr : ∀ (a : α), 1 < count a l → r a a
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hr : ∀ (a : α), 1 < count a [] → r a a
h : ∀ (a : α), a ∈ [] → ∀ (b : α), b ∈ [] → a ≠ b → r a b
⊢ Pairwise r []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ Pairwise r (hd :: tl)
[PROOFSTEP]
rw [List.pairwise_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ (∀ (a' : α), a' ∈ tl → r hd a') ∧ Pairwise r tl
[PROOFSTEP]
constructor
[GOAL]
case cons.left
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ ∀ (a' : α), a' ∈ tl → r hd a'
[PROOFSTEP]
intro x hx
[GOAL]
case cons.left
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
⊢ r hd x
[PROOFSTEP]
by_cases H : hd = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
H : hd = x
⊢ r hd x
[PROOFSTEP]
rw [H]
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
H : hd = x
⊢ r x x
[PROOFSTEP]
refine' hr _ _
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
H : hd = x
⊢ 1 < count x (hd :: tl)
[PROOFSTEP]
simpa [count_cons, H, Nat.succ_lt_succ_iff, count_pos] using hx
[GOAL]
case neg
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
H : ¬hd = x
⊢ r hd x
[PROOFSTEP]
exact h hd (mem_cons_self _ _) x (mem_cons_of_mem _ hx) H
[GOAL]
case cons.right
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ Pairwise r tl
[PROOFSTEP]
refine' IH _ _
[GOAL]
case cons.right.refine'_1
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ ∀ (a : α), 1 < count a tl → r a a
[PROOFSTEP]
intro x hx
[GOAL]
case cons.right.refine'_1
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : 1 < count x tl
⊢ r x x
[PROOFSTEP]
refine' hr _ _
[GOAL]
case cons.right.refine'_1
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : 1 < count x tl
⊢ 1 < count x (hd :: tl)
[PROOFSTEP]
rw [count_cons]
[GOAL]
case cons.right.refine'_1
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : 1 < count x tl
⊢ 1 < if x = hd then succ (count x tl) else count x tl
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝¹ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : 1 < count x tl
h✝ : x = hd
⊢ 1 < succ (count x tl)
[PROOFSTEP]
exact hx.trans (Nat.lt_succ_self _)
[GOAL]
case neg
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝¹ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : 1 < count x tl
h✝ : ¬x = hd
⊢ 1 < count x tl
[PROOFSTEP]
exact hx
[GOAL]
case cons.right.refine'_2
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
⊢ ∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b
[PROOFSTEP]
intro x hx y hy
[GOAL]
case cons.right.refine'_2
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableEq α
l : List α
r : α → α → Prop
hr✝ : ∀ (a : α), 1 < count a l → r a a
h✝ : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
hd : α
tl : List α
IH : (∀ (a : α), 1 < count a tl → r a a) → (∀ (a : α), a ∈ tl → ∀ (b : α), b ∈ tl → a ≠ b → r a b) → Pairwise r tl
hr : ∀ (a : α), 1 < count a (hd :: tl) → r a a
h : ∀ (a : α), a ∈ hd :: tl → ∀ (b : α), b ∈ hd :: tl → a ≠ b → r a b
x : α
hx : x ∈ tl
y : α
hy : y ∈ tl
⊢ x ≠ y → r x y
[PROOFSTEP]
exact h x (mem_cons_of_mem _ hx) y (mem_cons_of_mem _ hy)
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ Pairwise r l
[PROOFSTEP]
classical
refine' pairwise_of_reflexive_on_dupl_of_forall_ne (fun a ha' => _) fun a ha b hb _ => h a ha b hb
have ha := List.one_le_count_iff_mem.1 ha'.le
exact h a ha a ha
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ Pairwise r l
[PROOFSTEP]
refine' pairwise_of_reflexive_on_dupl_of_forall_ne (fun a ha' => _) fun a ha b hb _ => h a ha b hb
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
⊢ r a a
[PROOFSTEP]
have ha := List.one_le_count_iff_mem.1 ha'.le
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
ha : a ∈ l
⊢ r a a
[PROOFSTEP]
exact h a ha a ha
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
hr : Reflexive r
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
[PROOFSTEP]
classical exact pairwise_of_reflexive_on_dupl_of_forall_ne (fun _ _ => hr _) h
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
hr : Reflexive r
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
[PROOFSTEP]
exact pairwise_of_reflexive_on_dupl_of_forall_ne (fun _ _ => hr _) h
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
⊢ Pairwise R [] ↔ ∀ (i j : Fin (length [])), i < j → R (get [] i) (get [] j)
[PROOFSTEP]
simp only [Pairwise.nil, true_iff_iff]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
⊢ ∀ (i j : Fin (length [])), i < j → R (get [] i) (get [] j)
[PROOFSTEP]
exact fun i j _h => (Nat.not_lt_zero j).elim j.2
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
⊢ Pairwise R (a :: l) ↔ ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
[PROOFSTEP]
rw [pairwise_cons, pairwise_iff_get]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
⊢ ((∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)) ↔
    ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
[PROOFSTEP]
refine' ⟨fun H i j hij => _, fun H => ⟨fun a' m => _, fun i j hij => _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i j : Fin (length (a :: l))
hij : i < j
⊢ R (get (a :: l) i) (get (a :: l) j)
[PROOFSTEP]
cases' j with j hj
[GOAL]
case refine'_1.mk
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : j < length (a :: l)
hij : i < { val := j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := j, isLt := hj })
[PROOFSTEP]
cases' j with j
[GOAL]
case refine'_1.mk.zero
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
hj : zero < length (a :: l)
hij : i < { val := zero, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := zero, isLt := hj })
[PROOFSTEP]
exact (Nat.not_lt_zero _).elim hij
[GOAL]
case refine'_1.mk.succ
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
i : Fin (length (a :: l))
j : ℕ
hj : succ j < length (a :: l)
hij : i < { val := succ j, isLt := hj }
⊢ R (get (a :: l) i) (get (a :: l) { val := succ j, isLt := hj })
[PROOFSTEP]
cases' i with i hi
[GOAL]
case refine'_1.mk.succ.mk
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : i < length (a :: l)
hij : { val := i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
[PROOFSTEP]
cases' i with i
[GOAL]
case refine'_1.mk.succ.mk.zero
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
hi : zero < length (a :: l)
hij : { val := zero, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := zero, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
[PROOFSTEP]
exact H.1 _ (get_mem l _ _)
[GOAL]
case refine'_1.mk.succ.mk.succ
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : (∀ (a' : α), a' ∈ l → R a a') ∧ ∀ (i j : Fin (length l)), i < j → R (get l i) (get l j)
j : ℕ
hj : succ j < length (a :: l)
i : ℕ
hi : succ i < length (a :: l)
hij : { val := succ i, isLt := hi } < { val := succ j, isLt := hj }
⊢ R (get (a :: l) { val := succ i, isLt := hi }) (get (a :: l) { val := succ j, isLt := hj })
[PROOFSTEP]
exact H.2 _ _ (Nat.lt_of_succ_lt_succ hij)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
a' : α
m : a' ∈ l
⊢ R a a'
[PROOFSTEP]
rcases get_of_mem m with ⟨n, h, rfl⟩
[GOAL]
case refine'_2.intro.refl
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
⊢ R a (get l n)
[PROOFSTEP]
have := H ⟨0, show 0 < (a :: l).length from Nat.succ_pos _⟩ ⟨n.succ, Nat.succ_lt_succ n.2⟩ (Nat.succ_pos n)
[GOAL]
case refine'_2.intro.refl
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
n : Fin (length l)
m : get l n ∈ l
this :
  R (get (a :: l) { val := 0, isLt := (_ : 0 < length (a :: l)) })
    (get (a :: l) { val := ↑(Fin.succ n), isLt := (_ : succ ↑n < succ (length l)) })
⊢ R a (get l n)
[PROOFSTEP]
simpa
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
a : α
l : List α
H : ∀ (i j : Fin (length (a :: l))), i < j → R (get (a :: l) i) (get (a :: l) j)
i j : Fin (length l)
hij : i < j
⊢ R (get l i) (get l j)
[PROOFSTEP]
simpa using H i.succ j.succ (show i.1.succ < j.1.succ from Nat.succ_lt_succ hij)
[GOAL]
α✝ : Type u_1
β : Type u_2
R S T : α✝ → α✝ → Prop
a : α✝
l : List α✝
α : Type u_3
r : α → α → Prop
x : α
hx : r x x
⊢ Pairwise r (replicate 0 x)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
R S T : α✝ → α✝ → Prop
a : α✝
l : List α✝
α : Type u_3
r : α → α → Prop
x : α
hx : r x x
n : ℕ
⊢ Pairwise r (replicate (n + 1) x)
[PROOFSTEP]
simp only [replicate, add_eq, add_zero, pairwise_cons, mem_replicate, ne_eq, and_imp, forall_eq_apply_imp_iff', hx,
  implies_true, pairwise_replicate hx n, and_self]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
⊢ pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))
[PROOFSTEP]
have h' : ∀ b : β, b ∈ pwFilter (fun x y : β => R (f x) (f y)) xs → R (f x) (f b) := fun b hb =>
  h _ (by rw [pwFilter_map f xs]; apply mem_map_of_mem _ hb)
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
b : β
hb : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
⊢ f b ∈ pwFilter R (map f xs)
[PROOFSTEP]
rw [pwFilter_map f xs]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
b : β
hb : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
⊢ f b ∈ map f (pwFilter (fun x y => R (f x) (f y)) xs)
[PROOFSTEP]
apply mem_map_of_mem _ hb
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
h' : ∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
⊢ pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))
[PROOFSTEP]
rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
⊢ pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))
[PROOFSTEP]
have h' : ¬∀ b : β, b ∈ pwFilter (fun x y : β => R (f x) (f y)) xs → R (f x) (f b) := fun hh =>
  h fun a ha => by
    rw [pwFilter_map f xs, mem_map] at ha
    rcases ha with ⟨b, hb₀, hb₁⟩
    subst a
    exact hh _ hb₀
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
hh : ∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
a : α
ha : a ∈ pwFilter R (map f xs)
⊢ R (f x) a
[PROOFSTEP]
rw [pwFilter_map f xs, mem_map] at ha
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
hh : ∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
a : α
ha : ∃ a_1, a_1 ∈ pwFilter (fun x y => R (f x) (f y)) xs ∧ f a_1 = a
⊢ R (f x) a
[PROOFSTEP]
rcases ha with ⟨b, hb₀, hb₁⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
hh : ∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
a : α
b : β
hb₀ : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
hb₁ : f b = a
⊢ R (f x) a
[PROOFSTEP]
subst a
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
hh : ∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
b : β
hb₀ : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
⊢ R (f x) (f b)
[PROOFSTEP]
exact hh _ hb₀
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
h' : ¬∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)
⊢ pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))
[PROOFSTEP]
rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg h', pwFilter_map f xs]
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
⊢ pwFilter R (x :: l) <+ x :: l
[PROOFSTEP]
by_cases h : ∀ y ∈ pwFilter R l, R x y
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l
[PROOFSTEP]
rw [pwFilter_cons_of_pos h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ∀ (y : α), y ∈ pwFilter R l → R x y
⊢ x :: pwFilter R l <+ x :: l
[PROOFSTEP]
exact (pwFilter_sublist l).cons_cons _
[GOAL]
case neg
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R (x :: l) <+ x :: l
[PROOFSTEP]
rw [pwFilter_cons_of_neg h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
⊢ pwFilter R l <+ x :: l
[PROOFSTEP]
exact sublist_cons_of_sublist _ (pwFilter_sublist l)
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
x : α
l : List α
⊢ Pairwise R (pwFilter R (x :: l))
[PROOFSTEP]
by_cases h : ∀ y ∈ pwFilter R l, R x y
[GOAL]
case pos
α : Type u_1
β : Type u_2
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))
[PROOFSTEP]
rw [pwFilter_cons_of_pos h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact pairwise_cons.2 ⟨h, pairwise_pwFilter l⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
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))
[PROOFSTEP]
rw [pwFilter_cons_of_neg h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact pairwise_pwFilter l
[GOAL]
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
l : List α
p : Pairwise R l
⊢ pwFilter R l = l
[PROOFSTEP]
induction' l with x l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
inst✝ : DecidableRel R
l : List α
p✝ : Pairwise R l
p : Pairwise R []
⊢ pwFilter R [] = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases' pairwise_cons.1 p with al p
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [pwFilter_cons_of_pos (BAll.imp_left (pwFilter_subset l) al), IH p]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
induction' l with x l IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact fun _ _ h => (not_mem_nil _ h).elim
[GOAL]
case cons
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [forall_mem_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
by_cases h : ∀ y ∈ pwFilter R l, R x y
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [pwFilter_cons_of_pos h, forall_mem_cons, and_imp]
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact fun r H => ⟨r, IH H⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [pwFilter_cons_of_neg h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' fun H => ⟨_, IH H⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases' e : find? (fun y => ¬R x y) (pwFilter R l) with k
[GOAL]
case neg.none
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
refine' h.elim (BAll.imp_right _ (find?_eq_none.1 e))
[GOAL]
case neg.none
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact fun y _ => by simp
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp
[GOAL]
case neg.some
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have := find?_some e
[GOAL]
case neg.some
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact (neg_trans (H k (find?_mem e))).resolve_right (by simpa)
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simpa


[GOAL]
α : Type u_1
β : Type u_2
head✝ : α
l : List α
⊢ (head✝ :: l) ×ˢ [] = []
[PROOFSTEP]
simp [product_cons, product_nil]
[GOAL]
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
a : α
b : β
⊢ (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
[PROOFSTEP]
simp_all [SProd.sprod, product, mem_bind, mem_map, Prod.ext_iff, exists_prop, and_left_comm, exists_and_left,
  exists_eq_left, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ length (l₁ ×ˢ l₂) = length l₁ * length l₂
[PROOFSTEP]
induction' l₁ with x l₁ IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
l₂ : List β
⊢ length ([] ×ˢ l₂) = length [] * length l₂
[PROOFSTEP]
exact (zero_mul _).symm
[GOAL]
case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : length (l₁ ×ˢ l₂) = length l₁ * length l₂
⊢ length ((x :: l₁) ×ˢ l₂) = length (x :: l₁) * length l₂
[PROOFSTEP]
simp only [length, product_cons, length_append, IH, right_distrib, one_mul, length_map, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
head✝ : α
l : List α
⊢ (List.sigma (head✝ :: l) fun a => []) = []
[PROOFSTEP]
simp [sigma_cons, sigma_nil]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ List.sigma l₁ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
[PROOFSTEP]
simp [List.sigma, mem_bind, mem_map, exists_prop, exists_and_left, and_left_comm, exists_eq_left, heq_iff_eq,
  exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
[PROOFSTEP]
induction' l₁ with x l₁ IH
[GOAL]
case nil
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
⊢ length (List.sigma [] l₂) = sum (map (fun a => length (l₂ a)) [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
σ : α → Type u_3
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : length (List.sigma l₁ l₂) = sum (map (fun a => length (l₂ a)) l₁)
⊢ length (List.sigma (x :: l₁) l₂) = sum (map (fun a => length (l₂ a)) (x :: l₁))
[PROOFSTEP]
simp only [map, sigma_cons, length_append, length_map, IH, sum_cons]


[GOAL]
p : Prop
⊢ TFAE [p]
[PROOFSTEP]
simp [TFAE, -eq_iff_iff]
[GOAL]
a b : Prop
l : List Prop
h : b ∈ l
H : TFAE (a :: l)
⊢ a ∈ a :: l
[PROOFSTEP]
simp
[GOAL]
a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ TFAE l → TFAE (a :: l)
[PROOFSTEP]
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
[GOAL]
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
⊢ a ↔ a
[PROOFSTEP]
rfl
[GOAL]
case intro.head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
q : Prop
hq : Mem q l
⊢ a ↔ q
[PROOFSTEP]
exact ab.trans (H _ h _ hq)
[GOAL]
case intro.tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
⊢ p ↔ a
[PROOFSTEP]
exact (ab.trans (H _ h _ hp)).symm
[GOAL]
case intro.tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
[PROOFSTEP]
exact H _ hp _ hq
[GOAL]
a b : Prop
l : List Prop
⊢ Chain (fun x x_1 => x → x_1) a (b :: l) → (ilast' b l → a) → TFAE (a :: b :: l)
[PROOFSTEP]
induction' l with c l IH generalizing a b
[GOAL]
case nil
a✝ b✝ a b : Prop
⊢ Chain (fun x x_1 => x → x_1) a [b] → (ilast' b [] → a) → TFAE [a, b]
[PROOFSTEP]
simp only [tfae_cons_cons, tfae_singleton, and_true_iff, chain_cons, Chain.nil] at *
[GOAL]
case cons
a✝ b✝ c : Prop
l : List Prop
IH : ∀ {a b : Prop}, Chain (fun x x_1 => x → x_1) a (b :: l) → (ilast' b l → a) → TFAE (a :: b :: l)
a b : Prop
⊢ Chain (fun x x_1 => x → x_1) a (b :: c :: l) → (ilast' b (c :: l) → a) → TFAE (a :: b :: c :: l)
[PROOFSTEP]
simp only [tfae_cons_cons, tfae_singleton, and_true_iff, chain_cons, Chain.nil] at *
[GOAL]
case nil
a✝ b✝ a b : Prop
⊢ (a → b) → (ilast' b [] → a) → (a ↔ b)
[PROOFSTEP]
intro a b
[GOAL]
case nil
a✝¹ b✝¹ a✝ b✝ : Prop
a : a✝ → b✝
b : ilast' b✝ [] → a✝
⊢ a✝ ↔ b✝
[PROOFSTEP]
exact Iff.intro a b
[GOAL]
case cons
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
⊢ (a → b) ∧ (b → c) ∧ Chain (fun x x_1 => x → x_1) c l → (ilast' b (c :: l) → a) → (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
[PROOFSTEP]
rintro ⟨ab, ⟨bc, ch⟩⟩ la
[GOAL]
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
[PROOFSTEP]
have := IH ⟨bc, ch⟩ (ab ∘ la)
[GOAL]
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
this : (b ↔ c) ∧ TFAE (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
[PROOFSTEP]
exact ⟨⟨ab, la ∘ (this.2 c (Mem.head _) _ (ilast'_mem _ _)).1 ∘ bc⟩, this⟩
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ TFAE (map (fun p => ∀ (a : α), p a) l)
[PROOFSTEP]
simp_rw [TFAE, List.forall_mem_map_iff]
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
[PROOFSTEP]
intros p₁ hp₁ p₂ hp₂
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a
[PROOFSTEP]
exact forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁) (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ TFAE (map (fun p => ∃ a, p a) l)
[PROOFSTEP]
simp_rw [TFAE, List.forall_mem_map_iff]
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)
[PROOFSTEP]
intros p₁ hp₁ p₂ hp₂
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a
[PROOFSTEP]
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁) (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)