case intro.intro.intro.intro
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b, b ∈ s ∧ b ≠ a
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp hs
case pos
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a

case neg
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b, b ∈ s ∧ b ≠ a
by_cases ha : y = a
no goals
case pos
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
exact ⟨x, hx, ne_of_ne_of_eq hxy ha⟩
no goals
case neg
α : Type u_1
β : Type ?u.58840
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
exact ⟨y, hy, ha⟩