α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hs : Set.Nontrivial {x}
H : s = {x}
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hs : Set.Nontrivial s
H : s = {x}
⊢ False
rw [H] at hs
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hs : Set.Nontrivial {x}
H : s = {x}
⊢ False
exact not_nontrivial_singleton hs