-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Pairwise.lean
theorem pwFilter_map [DecidableRel (α := α) R] (f : β → α) :
    ∀ l : List β, pwFilter R (map f l) = map f (pwFilter (fun x y => R (f x) (f y)) l)
  | [] => rfl
  | x :: xs => by
    if h : ∀ b ∈ pwFilter R (map f xs), R (f x) b then
      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)
      rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]
    else
      rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg ?_, pwFilter_map f xs]
      refine fun hh => h fun a ha => ?_
      rw [pwFilter_map f xs, mem_map] at ha
      let ⟨b, hb₀, hb₁⟩ := ha; exact hb₁ ▸ hh _ hb₀

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
⊢ pwFilter R (map f (x :: xs)) = map f (pwFilter (fun x y => R (f x) (f y)) (x :: xs))

Tactic:
if h : ∀ b ∈ pwFilter R (map f xs), R (f x) b then
  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)
  rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]
else
  rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg ?_, pwFilter_map f xs]
  refine fun hh => h fun a ha => ?_
  rw [pwFilter_map f xs, mem_map] at ha
  let ⟨b, hb₀, hb₁⟩ := ha; exact hb₁ ▸ hh _ hb₀

Result:
no goals

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

Tactic:
apply mem_map_of_mem _ hb

Result:
no goals

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

Tactic:
rw [map, pwFilter_cons_of_neg h, pwFilter_cons_of_neg ?_, pwFilter_map f xs]

Result:
α : Type u_1
R : α → α → Prop
β : Type u_2
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
⊢ ¬∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)

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

Tactic:
rw [pwFilter_map f xs, mem_map] at ha

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

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
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
b : β
hb₀ : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
hb₁ : f b = a
⊢ R (f x) a

Tactic:
exact hb₁ ▸ hh _ hb₀

Result:
no goals

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

Tactic:
let ⟨b, hb₀, hb₁⟩ := ha

Result:
α : Type u_1
R : α → α → Prop
β : Type u_2
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
b : β
hb₀ : b ∈ pwFilter (fun x y => R (f x) (f y)) xs
hb₁ : f b = a
⊢ R (f x) a

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

Tactic:
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)

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

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

Tactic:
rw [pwFilter_map f xs]

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

Proof state:
α : Type u_1
R : α → α → Prop
β : Type u_2
inst✝ : DecidableRel R
f : β → α
x : β
xs : List β
h : ¬∀ (b : α), b ∈ pwFilter R (map f xs) → R (f x) b
⊢ ¬∀ (b : β), b ∈ pwFilter (fun x y => R (f x) (f y)) xs → R (f x) (f b)

Tactic:
refine fun hh => h fun a ha => ?_

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

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

Tactic:
rw [map, pwFilter_cons_of_pos h, pwFilter_cons_of_pos h', pwFilter_map f xs, map]

Result:
no goals