given infinite type, choose two distinct points

Stream: new members

[Steven Clontz]

np78 : ¬Finite X
⊢ ∃ x y : X, x ≠ y

Any clues on how I might proceed?

[Alex J. Best]

docs#exists_pair_ne using that docs#Infinite is docs#Nontrivial

[Alex J. Best]

Where did np78 come from though, the more canonical way to say that a type is infinite is to write [Infinite X], if you want you should be able to do have : Infinite X := \<np78\> to make the instance inplace instead

[Steven Clontz]

I'm working on https://github.com/leanprover-community/mathlib4/pull/12387 - P78 of https://topology.pi-base.org is Finite, so I'm still learning the "right" way to represent pi-Base properties as Lean objects