∀ {R : Type u_2} {S : Type u_4} {F : Type u_3} {K : Type u_1} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field F] [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : Algebra R S]
  [inst_6 : Algebra R F] [inst_7 : Algebra S F] [inst_8 : IsScalarTower R S F] [inst_9 : Algebra R K]
  [inst_10 : Algebra S K] [inst_11 : IsScalarTower R S K] (f : F →ₐ[S] K),
  (match 0 with
    | WeierstrassCurve.Affine.Point.zero => 0
    | WeierstrassCurve.Affine.Point.some h => WeierstrassCurve.Affine.Point.some ⋯) =
    match 0 with
    | WeierstrassCurve.Affine.Point.zero => 0
    | WeierstrassCurve.Affine.Point.some h => WeierstrassCurve.Affine.Point.some ⋯