α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : Set.Nontrivial {x}
⊢ False
rw [nontrivial_iff_exists_ne (mem_singleton x)] at H
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
⊢ False
let ⟨y, hy, hya⟩ := H
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False
exact hya (mem_singleton_iff.1 hy)