α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
unfold extend
no goals
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f✝ f : α → β
g : α → γ
e' : β → γ
b : β
inst✝ : Decidable (∃ a, f a = b)
⊢ (if h : ∃ a, f a = b then g (Classical.choose h) else e' b) =
    if h : ∃ a, f a = b then g (Classical.choose h) else e' b
congr