case h
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ piecewise {x} f g y = update g x (f x) y
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ piecewise {x} f g = update g x (f x)
ext y
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ piecewise {x} f g y = update g x (f x) y

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ piecewise {x} f g y = update g x (f x) y
case h
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ piecewise {x} f g y = update g x (f x) y
by_cases hy : y = x
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ piecewise {x} f g x = update g x (f x) x
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ piecewise {x} f g y = update g x (f x) y
subst y
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ piecewise {x} f g x = update g x (f x) x
simp
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.78565
ι : Sort ?u.78568
π : α → Type ?u.78573
δ : α → Sort ?u.78578
s : Set α
f✝ g✝ : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ piecewise {x} f g y = update g x (f x) y
simp [hy]