no goals
K : Type u
L : Type v
M : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field M
g : L →+* M
f : K →+* L
⊢ Subfield.map g (fieldRange f) = fieldRange (comp g f)
simpa only [fieldRange_eq_map] using (⊤ : Subfield K).map_map g f