case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
case refine_2
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ dedup l ↔ a ∈ l

case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
simpa only [dedup, forall_mem_ne, not_not] using this
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
intros x y z xz
no goals
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz