case h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝⁴ : Structure L M
inst✝³ : Structure L N
P : Type ?u.148304
inst✝² : Structure L P
Q : Type ?u.148312
inst✝¹ : Structure L Q
inst✝ : IsAlgebraic L
f : M →[L] N
hf : Function.Injective ↑f
x✝ : M
⊢ ↑(toHom (ofInjective hf)) x✝ = ↑f x✝
L : Language
L' : Language
M : Type w
N : Type w'
inst✝⁴ : Structure L M
inst✝³ : Structure L N
P : Type ?u.148304
inst✝² : Structure L P
Q : Type ?u.148312
inst✝¹ : Structure L Q
inst✝ : IsAlgebraic L
f : M →[L] N
hf : Function.Injective ↑f
⊢ toHom (ofInjective hf) = f
ext
no goals
case h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝⁴ : Structure L M
inst✝³ : Structure L N
P : Type ?u.148304
inst✝² : Structure L P
Q : Type ?u.148312
inst✝¹ : Structure L Q
inst✝ : IsAlgebraic L
f : M →[L] N
hf : Function.Injective ↑f
x✝ : M
⊢ ↑(toHom (ofInjective hf)) x✝ = ↑f x✝
simp