α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (fun i => if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j)
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
simp [piecewise]
case h
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (fun i => if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j)
ext i
case pos
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i

case neg
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
case h
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
by_cases h : i = j
case pos
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (fun i => if i ∈ s then f i else g i) j (f j) j
case pos
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
rw [h]
no goals
case pos
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (fun i => if i ∈ s then f i else g i) j (f j) j
simp
no goals
case neg
α : Type u_1
β : Type ?u.73354
γ : Type ?u.73357
ι : Sort ?u.73360
π : α → Type ?u.73365
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i => if i ∈ s then f i else g i) j (f j) i
by_cases h' : i ∈ s <;> simp [h, h']