no goals
α : Type u_2
β : Type ?u.2550
ι : Type ?u.2553
M : Type u_1
N : Type ?u.2559
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1
rw [@eq_comm _ (f a)]