no goals
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.13935
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)
simp
no goals
α : Type u
α' : Type w
β : Type v
β' : Type x
γ : Type u_1
δ : Type ?u.13935
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1
simp (config := { contextual := true })