∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {S : Type s} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {A : Type v} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [IsScalarTower R S A] {B : Type w} [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B]
  [IsScalarTower R S B] (ψ : A →ₐ[S] B),
  WeierstrassCurve.VariableChange.map (↑ψ) (WeierstrassCurve.VariableChange.baseChange A C) =
    WeierstrassCurve.VariableChange.baseChange B C