Integral Model base Change map

theorem integralModel_baseChange_map [IsIntegral 𝒪[k] E] :    integralModel 𝒪[l] (E.baseChange l) =      (integralModel 𝒪[k] E).map (integerMap k l) := by  -- both sides base change to `E.baseChange l`; `𝒪[l] → l` is injective, so `map` is  refine map_injective (f := algebraMap 𝒪[l] l) (IsFractionRing.injective 𝒪[l] l) ?_  change (integralModel 𝒪[l] (E.baseChange l)).map (algebraMap 𝒪[l] l)    = ((integralModel 𝒪[k] E).map (integerMap k l)).map (algebraMap 𝒪[l] l)  have hcomp : (algebraMap 𝒪[l] l).comp (integerMap k l)      = (algebraMap k l).comp (algebraMap 𝒪[k] k) := by    ext x; simpa using algebraMap_integerMap k l x  rw [map_map, hcomp, ← map_map,    show (integralModel 𝒪[k] E).map (algebraMap 𝒪[k] k) = E from baseChange_integralModel_eq 𝒪[k] E]  exact baseChange_integralModel_eq 𝒪[l] (E.baseChange l)