case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
⊢ ↑3 ≤ (#α)

α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y
have : ↑(3 : ℕ) ≤ (#α)
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
⊢ ↑3 ≤ (#α)

α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
simpa using h
case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ↑2 < (#α)

α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝ : ↑3 ≤ (#α)
this : ↑2 < (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
have : ↑(2 : ℕ) < (#α)
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝ : ↑3 ≤ (#α)
this : ↑2 < (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
case this
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this : ↑3 ≤ (#α)
⊢ ↑2 < (#α)

α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝ : ↑3 ≤ (#α)
this : ↑2 < (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
rwa [← succ_le_iff, ← Cardinal.nat_succ]
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝¹ : ↑3 ≤ (#α)
this✝ : ↑2 < (#α)
this : ∃ z, ¬z ∈ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝ : ↑3 ≤ (#α)
this : ↑2 < (#α)
⊢ ∃ z, z ≠ x ∧ z ≠ y
have := exists_not_mem_of_length_lt [x, y] this
no goals
α✝ β : Type u
α : Type u_1
h : 3 ≤ (#α)
x y : α
this✝¹ : ↑3 ≤ (#α)
this✝ : ↑2 < (#α)
this : ∃ z, ¬z ∈ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y
simpa [not_or] using this