α : Type u_2
β : Type u_1
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))
α : Type u_2
β : Type u_1
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))
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)
no goals
α : Type u_2
β : Type u_1
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))
rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]
α : Type u_2
β : Type u_1
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)
α : Type u_2
β : Type u_1
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)
rw [pwFilter_map f xs]
no goals
α : Type u_2
β : Type u_1
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)
apply mem_map_of_mem _ hb
α : Type u_2
β : Type u_1
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))
α : Type u_2
β : Type u_1
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))
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₀
no goals
α : Type u_2
β : Type u_1
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))
rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg h', pwFilter_map f xs]
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
rw [pwFilter_map f xs, mem_map] at ha
case intro.intro
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
rcases ha with ⟨b, hb₀, hb₁⟩
case intro.intro
α : Type u_2
β : Type u_1
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)
case intro.intro
α : Type u_2
β : Type u_1
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
subst a
no goals
case intro.intro
α : Type u_2
β : Type u_1
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)
exact hh _ hb₀