α : Type u_1
β : Type ?u.159008
s t : Set α
a✝ b x y : α
f : α → β
hs : 1 < ncard s
a : α
hsf : Set.Finite s
⊢ ∃ b, b ∈ s ∧ b ≠ a
α : Type u_1
β : Type ?u.159008
s t : Set α
a✝ b x y : α
f : α → β
hs : 1 < ncard s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
have hsf := (Finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm)
α : Type u_1
β : Type ?u.159008
s t : Set α
a✝ b x y : α
f : α → β
a : α
hsf : Set.Finite s
hs : 1 < Finset.card (Finite.toFinset hsf)
⊢ ∃ b, b ∈ s ∧ b ≠ a
α : Type u_1
β : Type ?u.159008
s t : Set α
a✝ b x y : α
f : α → β
hs : 1 < ncard s
a : α
hsf : Set.Finite s
⊢ ∃ b, b ∈ s ∧ b ≠ a
rw [ncard_eq_toFinset_card _ hsf] at hs
no goals
α : Type u_1
β : Type ?u.159008
s t : Set α
a✝ b x y : α
f : α → β
a : α
hsf : Set.Finite s
hs : 1 < Finset.card (Finite.toFinset hsf)
⊢ ∃ b, b ∈ s ∧ b ≠ a
simpa only [Finite.mem_toFinset] using Finset.exists_ne_of_one_lt_card hs a