α : Type u_1
β : Type ?u.349
inst✝ : Nontrivial α
x : α
this : DecidableEq α := Classical.decEq α
⊢ ∃ y, y ≠ x
α : Type u_1
β : Type ?u.349
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x
letI := Classical.decEq α
no goals
α : Type u_1
β : Type ?u.349
inst✝ : Nontrivial α
x : α
this : DecidableEq α := Classical.decEq α
⊢ ∃ y, y ≠ x
exact Decidable.exists_ne x