rfl
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝² : IsIntegrallyClosed S
inst✝¹ : IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
T : Type u_3
inst✝ : CommRing T
f : R →+* T
⊢ span ((fun x => f ((Algebra.intNorm R S) x)) '' ↑I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)
no goals