case h
α : Type u_1
β : Type u_2
γ : Type ?u.40151
ι : Sort ?u.40154
ι' : Sort ?u.40157
f✝ : α → β
s✝ t : Set α
f : α → β
a : α
s : Set α
x✝ : β
⊢ x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.40151
ι : Sort ?u.40154
ι' : Sort ?u.40157
f✝ : α → β
s✝ t : Set α
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.40151
ι : Sort ?u.40154
ι' : Sort ?u.40157
f✝ : α → β
s✝ t : Set α
f : α → β
a : α
s : Set α
x✝ : β
⊢ x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)
simp [and_or_left, exists_or, eq_comm, or_comm, and_comm]