L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(Language.con L a)
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) x = ↑(Language.con L a)
rw [Unique.eq_default x]
no goals
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(Language.con L a)
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _