case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Subsingleton ↑s → Set.Subsingleton s

case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Set.Subsingleton s → Subsingleton ↑s
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Subsingleton ↑s ↔ Set.Subsingleton s
constructor
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b✝ : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Subsingleton ↑s → Set.Subsingleton s
refine' fun h => fun a ha b hb => _
no goals
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b✝ : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
no goals
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Set.Subsingleton s → Subsingleton ↑s
exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)