case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f x = Function.const α (f default) x
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
⊢ f = Function.const α (f default)
ext x
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f default = Function.const α (f default) default
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f x = Function.const α (f default) x
rw [Subsingleton.elim x default]
no goals
case h
α : Sort u_1
β : Sort u_2
inst✝ : Unique α
f : α → β
x : α
⊢ f default = Function.const α (f default) default
rfl