α : Type u_1
β : Type u_2
γ : Type ?u.96342
ι : Sort ?u.96345
π : α → Type ?u.96350
δ : α → Sort ?u.96355
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g (sᶜ) ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → piecewise s f g x ≠ piecewise s f g y) ↔
    InjOn f s ∧ InjOn g (sᶜ) ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
α : Type u_1
β : Type u_2
γ : Type ?u.96342
ι : Sort ?u.96345
π : α → Type ?u.96350
δ : α → Sort ?u.96355
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (piecewise s f g) ↔ InjOn f s ∧ InjOn g (sᶜ) ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
rw [injective_iff_injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
  (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]
α : Type u_1
β : Type u_2
γ : Type ?u.96342
ι : Sort ?u.96345
π : α → Type ?u.96350
δ : α → Sort ?u.96355
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ piecewise s f g x ≠ piecewise s f g y ↔ f x ≠ g y
α : Type u_1
β : Type u_2
γ : Type ?u.96342
ι : Sort ?u.96345
π : α → Type ?u.96350
δ : α → Sort ?u.96355
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g (sᶜ) ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → piecewise s f g x ≠ piecewise s f g y) ↔
    InjOn f s ∧ InjOn g (sᶜ) ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y
refine' and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => _)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.96342
ι : Sort ?u.96345
π : α → Type ?u.96350
δ : α → Sort ?u.96355
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ piecewise s f g x ≠ piecewise s f g y ↔ f x ≠ g y
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_not_mem s f g hy]