case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ j ∈ ↑(single a b) i ↔ j ∈ ↑(PEquiv.refl α) i
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b : α
⊢ single a b = PEquiv.refl α
ext (i j)
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ (j ∈ if i = a then some b else none) ↔ j ∈ some i
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ j ∈ ↑(single a b) i ↔ j ∈ ↑(PEquiv.refl α) i
dsimp [single]
no goals
case h.a
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : Subsingleton α
a b i j : α
⊢ (j ∈ if i = a then some b else none) ↔ j ∈ some i
rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]