refine ⟨fun h ↦ ⟨fun x hx y hy hxy ↦  h hx.1 hy.1 ?_, ?_⟩, fun h x hx y hy hxy ↦ ?_⟩
α✝ : 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 α
a : α
b : β
⊢ InjOn (update f a b) s ↔ InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
case refine_1
α✝ : 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 α
a : α
b : β
h : InjOn (update f a b) s
x : α
hx : x ∈ s \ {a}
y : α
hy : y ∈ s \ {a}
hxy : f x = f y
⊢ update f a b x = update f a b y

case refine_2
α✝ : 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 α
a : α
b : β
h : InjOn (update f a b) s
⊢ a ∈ s → ∀ x ∈ s, f x = b → x = a

case refine_3
α✝ : 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 α
a : α
b : β
h : InjOn f (s \ {a}) ∧ (a ∈ s → ∀ x ∈ s, f x = b → x = a)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : update f a b x = update f a b y
⊢ x = y