case intro.intro
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x
rcases exists_pair_ne α with ⟨y, y', h⟩
case pos
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

case neg
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
case intro.intro
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x
by_cases hx:x = y
case pos
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
case pos
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
rw [← hx] at h
no goals
case pos
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
exact ⟨y', h.symm⟩
no goals
case neg
α : Type u_1
β : Type ?u.142
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
exact ⟨y, Ne.symm hx⟩