simpa
case h.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
⊢ x ∈ update f x b ⁻¹' s ↔ x ∈ insert x (f ⁻¹' s)

case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)
case h.inr
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b : β
f : α → β
s : Set β
hbs : b ∈ s
x : α
hxa : x ≠ a
⊢ x ∈ update f a b ⁻¹' s ↔ x ∈ insert a (f ⁻¹' s)