case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∆ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs ∆ Finite.toFinset ht
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∆ t)
⊢ Finite.toFinset h = Finite.toFinset hs ∆ Finite.toFinset ht
ext
no goals
case a
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
a : α
hs✝ : Set.Finite s
ht✝ : Set.Finite t
inst✝ : DecidableEq α
hs : Set.Finite s
ht : Set.Finite t
h : Set.Finite (s ∆ t)
a✝ : α
⊢ a✝ ∈ Finite.toFinset h ↔ a✝ ∈ Finite.toFinset hs ∆ Finite.toFinset ht
simp [mem_symmDiff, Finset.mem_symmDiff]