Definitions/Def_EllipticCurve_FunctionFieldPullback.lean

import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗
import Mathlib.RingTheory.DedekindDomain.Dvr ↗
import Mathlib.RingTheory.DedekindDomain.AdicValuation ↗
import Mathlib.RingTheory.DiscreteValuationRing.TFAE ↗
import Mathlib.FieldTheory.IsAlgClosed.Basic ↗
import Mathlib.RingTheory.Ideal.GoingUp ↗
import Mathlib.RingTheory.Localization.FractionRing ↗
import Mathlib.Tactic.FieldSimp ↗

open Polynomial
open scoped Polynomial.Bivariate

namespace WeierstrassCurve.Affine.CoordinateRing

variable {K : Type*} [Field K] {W : Affine K}

instance moduleFinite : Module.Finite K[X] W.CoordinateRing :=
  Module.Finite.of_basis (CoordinateRing.basis W)

instance isIntegral : Algebra.IsIntegral K[X] W.CoordinateRing :=
  Algebra.IsIntegral.of_finite K[X] W.CoordinateRing

theorem algebraMap_eq_mk_C (p : K[X]) : algebraMap K[X] W.CoordinateRing p = mk W (C p) := rfl

theorem isMaximal_of_isPrime {P : Ideal W.CoordinateRing} (hP : P ≠ ⊥) [P.IsPrime] :
    P.IsMaximal := by
  have hc : (P.comap (algebraMap K[X] W.CoordinateRing)) ≠ ⊥ := fun h =>
    hP (Ideal.eq_bot_of_comap_eq_bot h)
  haveI : (P.comap (algebraMap K[X] W.CoordinateRing)).IsMaximal :=
    IsPrime.to_maximal_ideal hc
  exact Ideal.isMaximal_of_isIntegral_of_isMaximal_comap (R := K[X]) P inferInstance

theorem exists_comap_eq_span [IsAlgClosed K] {P : Ideal W.CoordinateRing} (hP : P ≠ ⊥)
    [P.IsPrime] :
    ∃ a : K, P.comap (algebraMap K[X] W.CoordinateRing) = Ideal.span {X - C a} := by
  set p := P.comap (algebraMap K[X] W.CoordinateRing) with hp
  have hp0 : p ≠ ⊥ := fun h => hP (Ideal.eq_bot_of_comap_eq_bot h)
  haveI : p.IsPrime := Ideal.comap_isPrime _ P
  haveI hpmax : p.IsMaximal := IsPrime.to_maximal_ideal hp0
  set g := Submodule.IsPrincipal.generator p with hg
  have hgp : Ideal.span {g} = p := Ideal.span_singleton_generator p
  have hgprime : Prime g := Submodule.IsPrincipal.prime_generator_of_isPrime p hp0
  have hdeg : g.degree = 1 := IsAlgClosed.degree_eq_one_of_irreducible K hgprime.irreducible
  obtain ⟨a, ha⟩ := Polynomial.exists_root_of_degree_eq_one hdeg
  refine ⟨a, ?_⟩
  have hle : p ≤ Ideal.span {X - C a} := by
    rw [← hgp, Ideal.span_singleton_le_span_singleton]
    exact ⟨g /ₘ (X - C a), (Polynomial.mul_divByMonic_eq_iff_isRoot.mpr ha).symm⟩
  exact (hpmax.eq_of_le (Ideal.span_singleton_ne_top (Polynomial.not_isUnit_X_sub_C a)) hle).symm
    |>.symm

theorem XClass_mem_of_comap_eq {P : Ideal W.CoordinateRing} {a : K}
    (h : P.comap (algebraMap K[X] W.CoordinateRing) = Ideal.span {X - C a}) : XClass W a ∈ P := by
  have : X - C a ∈ P.comap (algebraMap K[X] W.CoordinateRing) := by
    rw [h]; exact Ideal.mem_span_singleton_self _
  exact this

theorem mk_C_mem_iff {P : Ideal W.CoordinateRing} {a : K}
    (h : P.comap (algebraMap K[X] W.CoordinateRing) = Ideal.span {X - C a}) (q : K[X]) :
    mk W (C q) ∈ P ↔ q.IsRoot a := by
  change q ∈ P.comap (algebraMap K[X] W.CoordinateRing) ↔ _
  rw [h, Ideal.mem_span_singleton, Polynomial.dvd_iff_isRoot]

theorem XYIdeal_isMaximal {a b : K} (h : W.Equation a b) : (XYIdeal W a (C b)).IsMaximal := by
  apply Ideal.Quotient.maximal_of_isField
  exact MulEquiv.isField (Field.toIsField K)
    (quotientXYIdealEquiv (W' := W) (x := a) (y := C b) h).toMulEquiv

theorem algebraMap_quot_apply (P : Ideal W.CoordinateRing) (c : K) :
    algebraMap K (W.CoordinateRing ⧸ P) c = Ideal.Quotient.mk P (mk W (C (C c))) := rfl

theorem algebraMap_quot_eq_comp_eval {P : Ideal W.CoordinateRing} {a : K}
    (h : P.comap (algebraMap K[X] W.CoordinateRing) = Ideal.span {X - C a}) :
    algebraMap K[X] (W.CoordinateRing ⧸ P) =
      (algebraMap K (W.CoordinateRing ⧸ P)).comp (evalRingHom a) := by
  apply Polynomial.ringHom_ext
  · intro c
    simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_C]
    rfl
  · simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_X]
    rw [algebraMap_quot_apply, IsScalarTower.algebraMap_apply K[X] W.CoordinateRing (W.CoordinateRing ⧸ P),
      Ideal.Quotient.algebraMap_eq, eq_comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
    have : mk W (C (C a)) - algebraMap K[X] W.CoordinateRing X = -XClass W a := by
      simp only [algebraMap_eq_mk_C, XClass, map_sub]; abel
    rw [this]
    exact P.neg_mem (XClass_mem_of_comap_eq h)

theorem exists_eq_XYIdeal [IsAlgClosed K] {P : Ideal W.CoordinateRing} (hP : P ≠ ⊥) [P.IsPrime] :
    ∃ a b : K, W.Equation a b ∧ P = XYIdeal W a (C b) := by
  obtain ⟨a, ha⟩ := exists_comap_eq_span hP
  haveI hPmax : P.IsMaximal := isMaximal_of_isPrime hP
  set L := W.CoordinateRing ⧸ P
  set π := Ideal.Quotient.mk P
  have hθ := algebraMap_quot_eq_comp_eval ha

  haveI : Algebra.IsIntegral K L := ⟨fun z => by
    obtain ⟨m, hm, hm0⟩ := Algebra.IsIntegral.isIntegral (R := K[X]) z
    refine ⟨m.map (evalRingHom a), hm.map _, ?_⟩
    rw [eval₂_map, ← hθ]
    exact hm0⟩

  obtain ⟨b, hb⟩ := (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := K) (K := L)).2 (π (mk W Y))
  have hYmem : YClass W (C b) ∈ P := by
    rw [YClass, map_sub, ← Ideal.Quotient.mk_eq_mk_iff_sub_mem]
    exact hb.symm

  have heq : W.Equation a b := by
    have hψ : π.comp (mk W) = (algebraMap K L).comp (evalEvalRingHom a b) := by
      apply Polynomial.ringHom_ext
      · intro q
        change algebraMap K[X] L q = _
        rw [hθ]
        simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_C]
        rfl
      · simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_X, eval_C]
        exact hb.symm
    have h0 : (π.comp (mk W)) W.polynomial = 0 := by
      rw [RingHom.comp_apply, AdjoinRoot.mk_self, map_zero]
    rw [hψ, RingHom.comp_apply, coe_evalEvalRingHom, map_eq_zero] at h0
    exact h0
  refine ⟨a, b, heq, ?_⟩

  have hle : XYIdeal W a (C b) ≤ P := by
    rw [XYIdeal, Ideal.span_le]
    rintro z (rfl | rfl)
    · exact XClass_mem_of_comap_eq ha
    · exact hYmem
  exact ((XYIdeal_isMaximal heq).eq_of_le hPmax.ne_top hle).symm

end WeierstrassCurve.Affine.CoordinateRing

namespace WeierstrassCurve.Affine

namespace Point

variable {S : Type*} [CommRing S] {V : Affine S}

def xc : V.Point → S
  | 0 => 0
  | some x _ _ => x

def yc : V.Point → S
  | 0 => 0
  | some _ y _ => y

@[simp] lemma xc_some {x y : S} (h : V.Nonsingular x y) : (some x y h).xc = x := rfl
@[simp] lemma yc_some {x y : S} (h : V.Nonsingular x y) : (some x y h).yc = y := rfl

lemma nonsingular_xc_yc {P : V.Point} (hP : P ≠ 0) : V.Nonsingular P.xc P.yc := by
  rcases P with _ | ⟨x, y, h⟩
  · exact absurd rfl hP
  · exact h

lemma eq_some_xc_yc {P : V.Point} (hP : P ≠ 0) : P = some P.xc P.yc (nonsingular_xc_yc hP) := by
  rcases P with _ | ⟨x, y, h⟩
  · exact absurd rfl hP
  · rfl

end Point

section Generic

variable {R : Type*} [Field R] (W : WeierstrassCurve R) (K : Type*) [Field K] [Algebra R K]

noncomputable instance instDecidableEqFunctionField : DecidableEq (W⁄K).FunctionField :=
  Classical.decEq _

noncomputable def genericX : (W⁄K).FunctionField :=
  algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField (CoordinateRing.mk (W⁄K) (C X))

noncomputable def genericY : (W⁄K).FunctionField :=
  algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField (CoordinateRing.mk (W⁄K) Y)

theorem evalEval_baseChange_polynomial (x y : (W⁄K).FunctionField) :
    (W⁄(W⁄K).FunctionField).polynomial.evalEval x y =
      (W⁄K).polynomial.eval₂ (aeval (R := K) x).toRingHom y := by
  rw [baseChange_polynomial W (Algebra.ofId K (W⁄K).FunctionField), evalEval, eval_map]
  have h := hom_eval₂ (W⁄K).polynomial (mapRingHom (Algebra.ofId K (W⁄K).FunctionField : K →+* _))
    (evalRingHom x) (C y)
  simp only [coe_evalRingHom, eval_C] at h
  rw [h]
  congr 1
  apply Polynomial.ringHom_ext
  · intro c
    simp only [RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, map_C, coe_evalRingHom,
      eval_C, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_C]
    rfl
  · simp only [RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, map_X, coe_evalRingHom,
      eval_X, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_X]

theorem algebraMap_comp_of :
    (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField).comp (AdjoinRoot.of (W⁄K).polynomial) =
      (aeval (R := K) (genericX W K)).toRingHom := by
  apply Polynomial.ringHom_ext
  · intro c
    simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      aeval_C]
    rw [← AdjoinRoot.algebraMap_eq, ← IsScalarTower.algebraMap_apply]
    change (algebraMap K[X] (W⁄K).FunctionField) (algebraMap K K[X] c) = _
    exact (IsScalarTower.algebraMap_apply K K[X] (W⁄K).FunctionField c).symm
  · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      aeval_X]
    rfl

theorem generic_equation :
    (W⁄(W⁄K).FunctionField).Equation (genericX W K) (genericY W K) := by
  rw [Equation, evalEval_baseChange_polynomial, ← algebraMap_comp_of]
  have h0 := congrArg (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField)
    (AdjoinRoot.eval₂_root (W⁄K).polynomial)
  rw [map_zero, hom_eval₂] at h0
  exact h0

theorem generic_nonsingular [W.IsElliptic] :
    (W⁄(W⁄K).FunctionField).Nonsingular (genericX W K) (genericY W K) := by
  haveI : (W⁄(W⁄K).FunctionField).IsElliptic := by
    dsimp only [Affine.baseChange, WeierstrassCurve.baseChange]; infer_instance
  exact (equation_iff_nonsingular (W := W⁄(W⁄K).FunctionField)).mp (generic_equation W K)

noncomputable def genericPoint [W.IsElliptic] : (W⁄(W⁄K).FunctionField).Point :=
  .some _ _ (generic_nonsingular W K)

end Generic

section PointHom

variable {R : Type*} [Field R] {W : WeierstrassCurve R} {K : Type*} [Field K] [Algebra R K]

theorem eval₂_polynomial_of_point (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) :
    (W⁄K).polynomial.eval₂ (aeval (R := K) Q.xc).toRingHom Q.yc = 0 := by
  rw [← evalEval_baseChange_polynomial]
  exact (Point.nonsingular_xc_yc hQ).left

noncomputable def pointHom (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) :
    (W⁄K).CoordinateRing →ₐ[K] (W⁄K).FunctionField :=
  { AdjoinRoot.lift (aeval (R := K) Q.xc).toRingHom Q.yc (eval₂_polynomial_of_point Q hQ) with
    commutes' := fun c => by
      simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
        MonoidHom.coe_coe]
      rw [IsScalarTower.algebraMap_apply K (Polynomial K) (W⁄K).CoordinateRing,
        AdjoinRoot.algebraMap_eq, AdjoinRoot.lift_of, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
        Polynomial.algebraMap_apply, aeval_C, Algebra.algebraMap_self, RingHom.id_apply] }

theorem pointHom_mk (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) (g : (Polynomial K)[X]) :
    pointHom Q hQ (CoordinateRing.mk (W⁄K) g) = g.eval₂ (aeval (R := K) Q.xc).toRingHom Q.yc :=
  AdjoinRoot.lift_mk (eval₂_polynomial_of_point Q hQ) g

@[simp] theorem pointHom_mk_C_C (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) (c : K) :
    pointHom Q hQ (CoordinateRing.mk (W⁄K) (C (C c))) = algebraMap K _ c :=
  (pointHom Q hQ).commutes c

@[simp] theorem pointHom_mk_C_X (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) :
    pointHom Q hQ (CoordinateRing.mk (W⁄K) (C X)) = Q.xc := by
  rw [pointHom_mk, eval₂_C, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_X]

@[simp] theorem pointHom_mk_Y (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) :
    pointHom Q hQ (CoordinateRing.mk (W⁄K) Y) = Q.yc := by
  rw [pointHom_mk, eval₂_X]

theorem CoordinateRing.algHom_ext' {A : Type*} [Semiring A] [Algebra K A]
    {f g : (W⁄K).CoordinateRing →ₐ[K] A}
    (hX : f (CoordinateRing.mk (W⁄K) (C X)) = g (CoordinateRing.mk (W⁄K) (C X)))
    (hY : f (CoordinateRing.mk (W⁄K) Y) = g (CoordinateRing.mk (W⁄K) Y)) : f = g := by
  apply AlgHom.coe_ringHom_injective
  apply Ideal.Quotient.ringHom_ext
  apply Polynomial.ringHom_ext
  · intro q
    change f (CoordinateRing.mk (W⁄K) (C q)) = g (CoordinateRing.mk (W⁄K) (C q))
    have hf : (f : (W⁄K).CoordinateRing →+* A).comp ((CoordinateRing.mk (W⁄K)).comp C) =
        (g : (W⁄K).CoordinateRing →+* A).comp ((CoordinateRing.mk (W⁄K)).comp C) := by
      apply Polynomial.ringHom_ext
      · intro c
        change f (algebraMap K _ c) = g (algebraMap K _ c)
        rw [AlgHom.commutes, AlgHom.commutes]
      · exact hX
    exact RingHom.congr_fun hf q
  · exact hY

theorem pointHom_genericPoint [W.IsElliptic] :
    pointHom (genericPoint W K) (Point.some_ne_zero _) =
      IsScalarTower.toAlgHom K (W⁄K).CoordinateRing (W⁄K).FunctionField := by
  apply CoordinateRing.algHom_ext'
  · rw [pointHom_mk_C_X, IsScalarTower.coe_toAlgHom', genericPoint, Point.xc_some]; rfl
  · rw [pointHom_mk_Y, IsScalarTower.coe_toAlgHom', genericPoint, Point.yc_some]; rfl

theorem Point.xc_map {F' L' : Type*} [Field F'] [Field L'] [Algebra R F'] [Algebra K F']
    [IsScalarTower R K F'] [Algebra R L'] [Algebra K L'] [IsScalarTower R K L']
    [DecidableEq F'] [DecidableEq L'] (f : F' →ₐ[K] L') (P : (W⁄F').Point) :
    (Point.map (W' := W) f P).xc = f P.xc := by
  cases P with
  | zero => exact (_root_.map_zero f).symm
  | some x y h => rfl

theorem Point.yc_map {F' L' : Type*} [Field F'] [Field L'] [Algebra R F'] [Algebra K F']
    [IsScalarTower R K F'] [Algebra R L'] [Algebra K L'] [IsScalarTower R K L']
    [DecidableEq F'] [DecidableEq L'] (f : F' →ₐ[K] L') (P : (W⁄F').Point) :
    (Point.map (W' := W) f P).yc = f P.yc := by
  cases P with
  | zero => exact (_root_.map_zero f).symm
  | some x y h => rfl

theorem pointHom_injective_of_ne_baseChange [DecidableEq K] [IsAlgClosed K] [W.IsElliptic]
    (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hQK : ∀ P : (W⁄K).Point, Q ≠ Point.baseChange K (W⁄K).FunctionField P) :
    Function.Injective (pointHom Q hQ) := by
  rw [injective_iff_map_eq_zero]
  by_contra hcon
  push Not at hcon
  have hker : RingHom.ker (pointHom Q hQ) ≠ ⊥ := by
    obtain ⟨a, ha, ha0⟩ := hcon
    intro h
    have hm : a ∈ RingHom.ker (pointHom Q hQ) := (RingHom.mem_ker).mpr ha
    rw [h, Ideal.mem_bot] at hm
    exact ha0 hm
  haveI : (RingHom.ker (pointHom Q hQ)).IsPrime := RingHom.ker_isPrime _
  obtain ⟨a, b, hab, hker'⟩ := CoordinateRing.exists_eq_XYIdeal hker
  haveI : (W⁄K).IsElliptic := by
    dsimp only [Affine.baseChange, WeierstrassCurve.baseChange]; infer_instance
  have hns : (W⁄K).Nonsingular a b := (equation_iff_nonsingular (W := W⁄K)).mp hab
  have hx : Q.xc = algebraMap K _ a := by
    have : CoordinateRing.XClass (W⁄K) a ∈ RingHom.ker (pointHom Q hQ) := by
      rw [hker']; exact Ideal.subset_span (Set.mem_insert _ _)
    rw [RingHom.mem_ker, CoordinateRing.XClass, map_sub, map_sub, map_sub, pointHom_mk_C_X,
      pointHom_mk_C_C, sub_eq_zero] at this
    exact this
  have hy : Q.yc = algebraMap K _ b := by
    have : CoordinateRing.YClass (W⁄K) (C b) ∈ RingHom.ker (pointHom Q hQ) := by
      rw [hker']; exact Ideal.subset_span (Set.mem_insert_of_mem _ rfl)
    rw [RingHom.mem_ker, CoordinateRing.YClass, map_sub, map_sub, pointHom_mk_Y, pointHom_mk_C_C,
      sub_eq_zero] at this
    exact this
  apply hQK (.some a b hns)
  rw [Point.eq_some_xc_yc hQ, Point.baseChange, Point.map_some]
  congr 1

noncomputable def pointPull (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) :
    (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField :=
  IsFractionRing.liftAlgHom hinj

@[simp] theorem pointPull_algebraMap (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) (h : (W⁄K).CoordinateRing) :
    pointPull Q hQ hinj (algebraMap _ _ h) = pointHom Q hQ h := by
  rw [pointPull, IsFractionRing.liftAlgHom_apply]
  exact IsFractionRing.lift_algebraMap hinj h

theorem map_pointPull_genericPoint [W.IsElliptic] (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) :
    Point.map (pointPull Q hQ hinj) (genericPoint W K) = Q := by
  conv_rhs => rw [Point.eq_some_xc_yc hQ]
  rw [genericPoint, Point.map_some]
  congr 1
  · rw [genericX, pointPull_algebraMap, pointHom_mk_C_X]
  · rw [genericY, pointPull_algebraMap, pointHom_mk_Y]

theorem pointPull_comp_pointHom (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) (P : (W⁄(W⁄K).FunctionField).Point) (hP : P ≠ 0)
    (hP' : Point.map (pointPull Q hQ hinj) P ≠ 0) :
    (pointPull Q hQ hinj).comp (pointHom P hP) = pointHom (Point.map (pointPull Q hQ hinj) P) hP' := by
  apply CoordinateRing.algHom_ext'
  · rw [AlgHom.comp_apply, pointHom_mk_C_X, pointHom_mk_C_X, Point.xc_map]
  · rw [AlgHom.comp_apply, pointHom_mk_Y, pointHom_mk_Y, Point.yc_map]

theorem pointHom_congr {Q Q' : (W⁄(W⁄K).FunctionField).Point} (h : Q = Q') (hQ : Q ≠ 0) (hQ' : Q' ≠ 0) :
    pointHom Q hQ = pointHom Q' hQ' := by subst h; rfl

theorem pointPull_comp_algebraMap (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) :
    (pointPull Q hQ hinj : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
      (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField) = pointHom Q hQ :=
  RingHom.ext fun h => pointPull_algebraMap Q hQ hinj h

theorem FunctionField.algHom_ext {φ ψ : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField}
    (h : (φ : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
        (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField) =
      (ψ : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
        (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField)) : φ = ψ :=
  AlgHom.coe_ringHom_injective
    (IsLocalization.ringHom_ext (nonZeroDivisors (W⁄K).CoordinateRing) h)

theorem exists_eq_baseChange_of_isIntegral_xc [DecidableEq K] [IsAlgClosed K] [W.IsElliptic]
    (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) (hx : _root_.IsIntegral K Q.xc) :
    ∃ P : (W⁄K).Point, Q = Point.baseChange K (W⁄K).FunctionField P := by
  haveI : (W⁄K).IsElliptic := by
    dsimp only [Affine.baseChange, WeierstrassCurve.baseChange]; infer_instance

  have hdx : (minpoly K Q.xc).degree = 1 :=
    IsAlgClosed.degree_eq_one_of_irreducible K (minpoly.irreducible hx)
  obtain ⟨a, ha⟩ : Q.xc ∈ (algebraMap K (W⁄K).FunctionField).range := minpoly.mem_range_of_degree_eq_one K _ hdx

  have heq := (Point.nonsingular_xc_yc hQ).left
  rw [equation_iff] at heq
  have hy : _root_.IsIntegral K Q.yc := by
    refine ⟨X ^ 2 + C ((W⁄K).a₁ * a + (W⁄K).a₃) * X - C (a ^ 3 + (W⁄K).a₂ * a ^ 2 + (W⁄K).a₄ * a + (W⁄K).a₆),
      ?_, ?_⟩
    · have hlt : (C ((W⁄K).a₁ * a + (W⁄K).a₃) * X -
          C (a ^ 3 + (W⁄K).a₂ * a ^ 2 + (W⁄K).a₄ * a + (W⁄K).a₆) : K[X]).degree < ((X : K[X]) ^ 2).degree := by
        rw [degree_X_pow]
        refine (degree_sub_le _ _).trans_lt (max_lt ((degree_C_mul_X_le _).trans_lt ?_)
          (degree_C_le.trans_lt ?_))
        · exact WithBot.coe_lt_coe.mpr (by norm_num)
        · exact WithBot.coe_lt_coe.mpr (by norm_num)
      rw [add_sub_assoc]
      exact (monic_X_pow 2).add_of_left hlt
    · simp only [eval₂_add, eval₂_sub, eval₂_pow, eval₂_X, eval₂_mul, eval₂_C, map_add, map_mul, map_pow]
      rw [ha]
      have e1 : (algebraMap K (W⁄K).FunctionField) (W⁄K).a₁ = (W⁄(W⁄K).FunctionField).a₁ :=
        (IsScalarTower.algebraMap_apply R K (W⁄K).FunctionField W.a₁).symm
      have e2 : (algebraMap K (W⁄K).FunctionField) (W⁄K).a₂ = (W⁄(W⁄K).FunctionField).a₂ :=
        (IsScalarTower.algebraMap_apply R K (W⁄K).FunctionField W.a₂).symm
      have e3 : (algebraMap K (W⁄K).FunctionField) (W⁄K).a₃ = (W⁄(W⁄K).FunctionField).a₃ :=
        (IsScalarTower.algebraMap_apply R K (W⁄K).FunctionField W.a₃).symm
      have e4 : (algebraMap K (W⁄K).FunctionField) (W⁄K).a₄ = (W⁄(W⁄K).FunctionField).a₄ :=
        (IsScalarTower.algebraMap_apply R K (W⁄K).FunctionField W.a₄).symm
      have e6 : (algebraMap K (W⁄K).FunctionField) (W⁄K).a₆ = (W⁄(W⁄K).FunctionField).a₆ :=
        (IsScalarTower.algebraMap_apply R K (W⁄K).FunctionField W.a₆).symm
      rw [e1, e2, e3, e4, e6]
      linear_combination heq
  have hdy : (minpoly K Q.yc).degree = 1 :=
    IsAlgClosed.degree_eq_one_of_irreducible K (minpoly.irreducible hy)
  obtain ⟨b, hb⟩ : Q.yc ∈ (algebraMap K (W⁄K).FunctionField).range := minpoly.mem_range_of_degree_eq_one K _ hdy
  have hab : (W⁄K).Equation a b := by
    rw [← baseChange_equation W (Algebra.ofId K (W⁄K).FunctionField).injective a b]
    change (W⁄(W⁄K).FunctionField).Equation (algebraMap K _ a) (algebraMap K _ b)
    rw [ha, hb]
    exact (Point.nonsingular_xc_yc hQ).left
  have hns : (W⁄K).Nonsingular a b := (equation_iff_nonsingular (W := W⁄K)).mp hab
  refine ⟨.some a b hns, ?_⟩
  rw [Point.eq_some_xc_yc hQ, Point.baseChange, Point.map_some]
  congr 1 <;> [exact ha.symm; exact hb.symm]

theorem not_isIntegral_xc_of_ne_baseChange [DecidableEq K] [IsAlgClosed K] [W.IsElliptic]
    (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hQK : ∀ P : (W⁄K).Point, Q ≠ Point.baseChange K (W⁄K).FunctionField P) :
    ¬ _root_.IsIntegral K Q.xc :=
  fun hx => by obtain ⟨P, hP⟩ := exists_eq_baseChange_of_isIntegral_xc Q hQ hx; exact hQK P hP

end PointHom

section TransMul

variable {R : Type*} [Field R] (W : WeierstrassCurve R) (K : Type*) [Field K] [Algebra R K]
  [DecidableEq K] [IsAlgClosed K] [W.IsElliptic]

omit [IsAlgClosed K] in

theorem genericPoint_ne_baseChange (P : (W⁄K).Point) :
    genericPoint W K ≠ Point.baseChange K (W⁄K).FunctionField P := by
  intro h
  cases P with
  | zero => exact Point.some_ne_zero _ (h.trans (map_zero _))
  | some a b hab =>
    rw [genericPoint, Point.baseChange, Point.map_some, Point.some.injEq] at h
    apply CoordinateRing.XClass_ne_zero (W' := W⁄K) a
    apply IsFractionRing.injective (W⁄K).CoordinateRing (W⁄K).FunctionField
    rw [CoordinateRing.XClass, map_sub, map_sub, map_sub, _root_.map_zero]
    have h1 : algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField (CoordinateRing.mk (W⁄K) (C X)) =
        genericX W K := rfl
    have h2 : algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField (CoordinateRing.mk (W⁄K) (C (C a))) =
        algebraMap K (W⁄K).FunctionField a :=
      (IsScalarTower.algebraMap_apply K (W⁄K).CoordinateRing (W⁄K).FunctionField a).symm
    rw [h1, h2, h.1, sub_eq_zero]
    rfl

omit [IsAlgClosed K] in

theorem genericPoint_add_baseChange_ne_zero (S : (W⁄K).Point) :
    genericPoint W K + Point.baseChange K _ S ≠ 0 := by
  intro h
  apply genericPoint_ne_baseChange W K (-S)
  rw [map_neg]
  exact eq_neg_of_add_eq_zero_left h

omit [IsAlgClosed K] in

theorem genericPoint_add_baseChange_ne_baseChange (S P : (W⁄K).Point) :
    genericPoint W K + Point.baseChange K _ S ≠ Point.baseChange K _ P := by
  intro h
  apply genericPoint_ne_baseChange W K (P - S)
  rw [map_sub, ← h, add_sub_cancel_right]

theorem transHom_injective (S : (W⁄K).Point) :
    Function.Injective (pointHom (genericPoint W K + Point.baseChange K _ S)
      (genericPoint_add_baseChange_ne_zero W K S)) :=
  pointHom_injective_of_ne_baseChange _ _ (genericPoint_add_baseChange_ne_baseChange W K S)

noncomputable def transPull (S : (W⁄K).Point) : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField :=
  pointPull _ (genericPoint_add_baseChange_ne_zero W K S) (transHom_injective W K S)

theorem map_transPull_genericPoint (S : (W⁄K).Point) :
    Point.map (transPull W K S) (genericPoint W K) = genericPoint W K + Point.baseChange K _ S :=
  map_pointPull_genericPoint _ _ _

theorem map_transPull_genericPoint_add (S T : (W⁄K).Point) :
    Point.map (transPull W K S) (genericPoint W K + Point.baseChange K _ T) =
      genericPoint W K + Point.baseChange K _ (S + T) := by
  rw [map_add, map_transPull_genericPoint, Point.map_baseChange, add_assoc, ← map_add]

theorem transPull_comp_algebraMap (S : (W⁄K).Point) :
    (transPull W K S : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
      (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField) =
      pointHom (genericPoint W K + Point.baseChange K _ S) (genericPoint_add_baseChange_ne_zero W K S) :=
  pointPull_comp_algebraMap _ (genericPoint_add_baseChange_ne_zero W K S) (transHom_injective W K S)

theorem transPull_comp_pointHom (S : (W⁄K).Point) (P : (W⁄(W⁄K).FunctionField).Point) (hP : P ≠ 0)
    (hP' : Point.map (transPull W K S) P ≠ 0) :
    (transPull W K S).comp (pointHom P hP) = pointHom (Point.map (transPull W K S) P) hP' :=
  pointPull_comp_pointHom _ _ _ P hP hP'

theorem transPull_comp_transHom (S T : (W⁄K).Point) :
    (transPull W K S).comp (pointHom (genericPoint W K + Point.baseChange K _ T)
      (genericPoint_add_baseChange_ne_zero W K T)) =
      pointHom (genericPoint W K + Point.baseChange K _ (S + T))
        (genericPoint_add_baseChange_ne_zero W K (S + T)) := by
  apply CoordinateRing.algHom_ext'
  · rw [AlgHom.comp_apply, pointHom_mk_C_X, pointHom_mk_C_X, ← map_transPull_genericPoint_add,
      Point.xc_map]
  · rw [AlgHom.comp_apply, pointHom_mk_Y, pointHom_mk_Y, ← map_transPull_genericPoint_add,
      Point.yc_map]

theorem transPull_comp (S T : (W⁄K).Point) :
    (transPull W K S).comp (transPull W K T) = transPull W K (S + T) := by
  apply FunctionField.algHom_ext
  rw [AlgHom.comp_toRingHom, RingHom.comp_assoc, transPull_comp_algebraMap W K T,
    transPull_comp_algebraMap W K (S + T), ← AlgHom.comp_toRingHom, transPull_comp_transHom]

theorem transPull_zero : transPull W K 0 = AlgHom.id K _ := by
  apply FunctionField.algHom_ext
  rw [transPull_comp_algebraMap]
  have h0 : genericPoint W K + Point.baseChange K (W⁄K).FunctionField (0 : (W⁄K).Point) =
      genericPoint W K := by
    rw [map_zero, add_zero]
  rw [pointHom_congr h0 _ (Point.some_ne_zero _), pointHom_genericPoint]
  exact RingHom.ext fun x => rfl

noncomputable def transEquiv (S : (W⁄K).Point) : (W⁄K).FunctionField ≃ₐ[K] (W⁄K).FunctionField :=
  AlgEquiv.ofAlgHom (transPull W K S) (transPull W K (-S))
    (by rw [transPull_comp, add_neg_cancel, transPull_zero])
    (by rw [transPull_comp, neg_add_cancel, transPull_zero])

theorem transEquiv_apply (S : (W⁄K).Point) (h : (W⁄K).FunctionField) :
    transEquiv W K S h = transPull W K S h := rfl

theorem coe_transEquiv (S : (W⁄K).Point) :
    (transEquiv W K S : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField) = transPull W K S := rfl

theorem transEquiv_algebraMap (S : (W⁄K).Point) (h : (W⁄K).CoordinateRing) :
    transEquiv W K S (algebraMap _ _ h) =
      pointHom (genericPoint W K + Point.baseChange K _ S) (genericPoint_add_baseChange_ne_zero W K S) h :=
  pointPull_algebraMap _ (genericPoint_add_baseChange_ne_zero W K S) (transHom_injective W K S) h

theorem transEquiv_genericX (S : (W⁄K).Point) :
    transEquiv W K S (genericX W K) = (genericPoint W K + Point.baseChange K _ S).xc := by
  rw [genericX, transEquiv_algebraMap, pointHom_mk_C_X]

theorem transEquiv_genericY (S : (W⁄K).Point) :
    transEquiv W K S (genericY W K) = (genericPoint W K + Point.baseChange K _ S).yc := by
  rw [genericY, transEquiv_algebraMap, pointHom_mk_Y]

theorem map_transEquiv_genericPoint (S : (W⁄K).Point) :
    Point.map (transEquiv W K S : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField) (genericPoint W K) =
      genericPoint W K + Point.baseChange K _ S := by
  rw [coe_transEquiv, map_transPull_genericPoint]

theorem transEquiv_add (S T : (W⁄K).Point) :
    transEquiv W K (S + T) = (transEquiv W K T).trans (transEquiv W K S) := by
  apply AlgEquiv.ext
  intro h
  rw [AlgEquiv.trans_apply, transEquiv_apply, transEquiv_apply, transEquiv_apply,
    ← AlgHom.comp_apply, transPull_comp]

theorem transEquiv_zero : transEquiv W K 0 = AlgEquiv.refl := by
  apply AlgEquiv.ext
  intro h
  rw [transEquiv_apply, transPull_zero]
  rfl

theorem transEquiv_injective : Function.Injective (transEquiv W K) := by
  intro S T h
  have hx := transEquiv_genericX W K S
  have hy := transEquiv_genericY W K S
  rw [h, transEquiv_genericX] at hx
  rw [h, transEquiv_genericY] at hy
  have hpt : genericPoint W K + Point.baseChange K _ T = genericPoint W K + Point.baseChange K _ S := by
    rw [Point.eq_some_xc_yc (genericPoint_add_baseChange_ne_zero W K T),
      Point.eq_some_xc_yc (genericPoint_add_baseChange_ne_zero W K S)]
    congr 1
  exact (Point.map_injective _ (add_left_cancel hpt)).symm

omit [IsAlgClosed K] in
theorem neg_genericPoint_ne_baseChange (P : (W⁄K).Point) :
    -genericPoint W K ≠ Point.baseChange K (W⁄K).FunctionField P := by
  intro h
  apply genericPoint_ne_baseChange W K (-P)
  rw [map_neg, ← h, neg_neg]

theorem negHom_injective :
    Function.Injective (pointHom (-genericPoint W K) (neg_ne_zero.mpr (Point.some_ne_zero _))) :=
  pointHom_injective_of_ne_baseChange _ _ (neg_genericPoint_ne_baseChange W K)

noncomputable def negPull : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField :=
  pointPull _ (neg_ne_zero.mpr (Point.some_ne_zero _)) (negHom_injective W K)

theorem map_negPull_genericPoint : Point.map (negPull W K) (genericPoint W K) = -genericPoint W K :=
  map_pointPull_genericPoint _ _ _

theorem negPull_algebraMap (g : (W⁄K).CoordinateRing) :
    negPull W K (algebraMap _ _ g) = pointHom (-genericPoint W K) (neg_ne_zero.mpr (Point.some_ne_zero _)) g :=
  pointPull_algebraMap _ _ _ g

theorem negPull_comp_algebraMap :
    (negPull W K : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
      (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField) =
      pointHom (-genericPoint W K) (neg_ne_zero.mpr (Point.some_ne_zero _)) :=
  pointPull_comp_algebraMap _ _ _

theorem negPull_comp_pointHom (P : (W⁄(W⁄K).FunctionField).Point) (hP : P ≠ 0)
    (hP' : Point.map (negPull W K) P ≠ 0) :
    (negPull W K).comp (pointHom P hP) = pointHom (Point.map (negPull W K) P) hP' :=
  pointPull_comp_pointHom _ _ _ P hP hP'

theorem negPull_comp_negPull : (negPull W K).comp (negPull W K) = AlgHom.id K _ := by
  apply FunctionField.algHom_ext
  have hP' : Point.map (negPull W K) (-genericPoint W K) = genericPoint W K := by
    rw [map_neg, map_negPull_genericPoint, neg_neg]
  rw [AlgHom.comp_toRingHom, RingHom.comp_assoc, negPull_comp_algebraMap, ← AlgHom.comp_toRingHom,
    negPull_comp_pointHom W K _ _ (by rw [hP']; exact Point.some_ne_zero _),
    pointHom_congr hP' _ (Point.some_ne_zero _), pointHom_genericPoint]
  exact RingHom.ext fun x => rfl

noncomputable def negEquiv : (W⁄K).FunctionField ≃ₐ[K] (W⁄K).FunctionField :=
  AlgEquiv.ofAlgHom (negPull W K) (negPull W K) (negPull_comp_negPull W K) (negPull_comp_negPull W K)

theorem coe_negEquiv : (negEquiv W K : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField) = negPull W K := rfl

theorem negEquiv_apply (h : (W⁄K).FunctionField) : negEquiv W K h = negPull W K h := rfl

theorem map_negEquiv_genericPoint :
    Point.map (negEquiv W K : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField) (genericPoint W K) =
      -genericPoint W K := by
  rw [coe_negEquiv, map_negPull_genericPoint]

theorem negEquiv_genericX : negEquiv W K (genericX W K) = genericX W K := by
  rw [negEquiv_apply, genericX, negPull_algebraMap, pointHom_mk_C_X]
  simp only [genericPoint, Point.neg_some, Point.xc_some]
  rfl

theorem negEquiv_genericY :
    negEquiv W K (genericY W K) = (W⁄(W⁄K).FunctionField).negY (genericX W K) (genericY W K) := by
  rw [negEquiv_apply, genericY, negPull_algebraMap, pointHom_mk_Y]
  simp only [genericPoint, Point.neg_some, Point.yc_some]
  rfl

theorem negEquiv_symm : (negEquiv W K).symm = negEquiv W K := rfl

def MulGood (n : ℤ) : Prop :=
  n • genericPoint W K ≠ 0 ∧
    ∀ P : (W⁄K).Point, n • genericPoint W K ≠ Point.baseChange K (W⁄K).FunctionField P

theorem mulHom_injective {n : ℤ} (h : MulGood W K n) :
    Function.Injective (pointHom (n • genericPoint W K) h.1) :=
  pointHom_injective_of_ne_baseChange _ _ h.2

open Classical in

noncomputable def mulPull (n : ℤ) : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField :=
  if h : MulGood W K n then pointPull (n • genericPoint W K) h.1 (mulHom_injective W K h)
  else AlgHom.id K _

theorem mulPull_eq {n : ℤ} (h : MulGood W K n) :
    mulPull W K n = pointPull (n • genericPoint W K) h.1 (mulHom_injective W K h) := by
  rw [mulPull, dif_pos h]

theorem mulPull_algebraMap {n : ℤ} (h : MulGood W K n) (g : (W⁄K).CoordinateRing) :
    mulPull W K n (algebraMap _ _ g) = pointHom (n • genericPoint W K) h.1 g := by
  rw [mulPull_eq W K h, pointPull_algebraMap]

theorem mulPull_comp_algebraMap {n : ℤ} (h : MulGood W K n) :
    (mulPull W K n : (W⁄K).FunctionField →+* (W⁄K).FunctionField).comp
      (algebraMap (W⁄K).CoordinateRing (W⁄K).FunctionField) = pointHom (n • genericPoint W K) h.1 :=
  RingHom.ext fun g => mulPull_algebraMap W K h g

theorem mulPull_genericX' {n : ℤ} (h : MulGood W K n) :
    mulPull W K n (genericX W K) = (n • genericPoint W K).xc := by
  rw [genericX, mulPull_algebraMap W K h, pointHom_mk_C_X]

theorem mulPull_genericY' {n : ℤ} (h : MulGood W K n) :
    mulPull W K n (genericY W K) = (n • genericPoint W K).yc := by
  rw [genericY, mulPull_algebraMap W K h, pointHom_mk_Y]

theorem map_mulPull_genericPoint' {n : ℤ} (h : MulGood W K n) :
    Point.map (mulPull W K n) (genericPoint W K) = n • genericPoint W K := by
  rw [mulPull_eq W K h, map_pointPull_genericPoint]

theorem mulPull_comp_pointHom {n : ℤ} (h : MulGood W K n) (P : (W⁄(W⁄K).FunctionField).Point)
    (hP : P ≠ 0) (hP' : Point.map (mulPull W K n) P ≠ 0) :
    (mulPull W K n).comp (pointHom P hP) = pointHom (Point.map (mulPull W K n) P) hP' := by
  have hP'' : Point.map (pointPull (n • genericPoint W K) h.1 (mulHom_injective W K h)) P ≠ 0 := by
    rw [← mulPull_eq W K h]; exact hP'
  rw [pointHom_congr (congrArg (fun φ => Point.map φ P) (mulPull_eq W K h)) hP' hP'', mulPull_eq W K h]
  exact pointPull_comp_pointHom _ _ _ P hP hP''

theorem transEquiv_mulPull' {n : ℤ} (h : MulGood W K n) {S : (W⁄K).Point} (hS : n • S = 0)
    (g : (W⁄K).FunctionField) : transEquiv W K S (mulPull W K n g) = mulPull W K n g := by
  rw [transEquiv_apply, ← AlgHom.comp_apply]
  congr 1
  apply FunctionField.algHom_ext
  have hP' : Point.map (transPull W K S) (n • genericPoint W K) = n • genericPoint W K := by
    rw [map_zsmul, map_transPull_genericPoint, smul_add, ← map_zsmul, hS, map_zero, add_zero]
  rw [AlgHom.comp_toRingHom, RingHom.comp_assoc, mulPull_comp_algebraMap W K h, ← AlgHom.comp_toRingHom,
    transPull_comp_pointHom W K S _ _ (by rw [hP']; exact h.1)]
  exact congrArg _ (pointHom_congr hP' _ _)

theorem mulPull_comp' {m n : ℤ} (hm : MulGood W K m) (hn : MulGood W K n) (hnm : MulGood W K (n * m)) :
    (mulPull W K m).comp (mulPull W K n) = mulPull W K (n * m) := by
  apply FunctionField.algHom_ext
  have hP' : Point.map (mulPull W K m) (n • genericPoint W K) = (n * m) • genericPoint W K := by
    rw [map_zsmul, map_mulPull_genericPoint' W K hm, smul_smul]
  rw [AlgHom.comp_toRingHom, RingHom.comp_assoc, mulPull_comp_algebraMap W K hn,
    mulPull_comp_algebraMap W K hnm, ← AlgHom.comp_toRingHom,
    mulPull_comp_pointHom W K hm _ _ (by rw [hP']; exact hnm.1)]
  exact congrArg _ (pointHom_congr hP' _ _)

omit [DecidableEq K] in

theorem exists_point_xc_eq (x : K) : ∃ P : (W⁄K).Point, P ≠ 0 ∧ P.xc = x := by
  haveI : (W⁄K).IsElliptic := by
    dsimp only [Affine.baseChange, WeierstrassCurve.baseChange]; infer_instance
  set c := (W⁄K).a₁ * x + (W⁄K).a₃ with hc
  set d := -(x ^ 3 + (W⁄K).a₂ * x ^ 2 + (W⁄K).a₄ * x + (W⁄K).a₆) with hd
  have hlt : (C c * X + C d : K[X]).degree < ((X : K[X]) ^ 2).degree := by
    rw [degree_X_pow]
    refine (degree_add_le _ _).trans_lt (max_lt ((degree_C_mul_X_le c).trans_lt ?_)
      (degree_C_le.trans_lt ?_))
    · exact WithBot.coe_lt_coe.mpr (by norm_num)
    · exact WithBot.coe_lt_coe.mpr (by norm_num)
  have hdeg : ((X : K[X]) ^ 2 + (C c * X + C d)).degree = 2 := by
    rw [degree_add_eq_left_of_degree_lt hlt, degree_X_pow]; rfl
  obtain ⟨y, hy⟩ := IsAlgClosed.exists_root ((X : K[X]) ^ 2 + (C c * X + C d))
    (by rw [hdeg]; exact two_ne_zero)
  have hroot : y ^ 2 + (c * y + d) = 0 := by
    have := hy.eq_zero
    simpa only [eval_add, eval_pow, eval_X, eval_mul, eval_C] using this
  have heq : (W⁄K).Equation x y := by
    rw [equation_iff]
    rw [hc, hd] at hroot
    linear_combination hroot
  exact ⟨.some x y ((equation_iff_nonsingular (W := W⁄K)).mp heq), Point.some_ne_zero _, rfl⟩

omit [DecidableEq K] in
theorem infinite_point : Infinite (W⁄K).Point := by
  choose f hf0 hfx using exists_point_xc_eq W K
  exact Infinite.of_injective f fun x y h => by rw [← hfx x, ← hfx y, h]

theorem map_negEquiv_zsmul_genericPoint (n : ℤ) :
    Point.map (negEquiv W K : (W⁄K).FunctionField →ₐ[K] (W⁄K).FunctionField) (n • genericPoint W K) =
      -(n • genericPoint W K) := by
  rw [map_zsmul, map_negEquiv_genericPoint, smul_neg]

theorem negEquiv_mulPull_genericX' {n : ℤ} (h : MulGood W K n) :
    negEquiv W K (mulPull W K n (genericX W K)) = (n • genericPoint W K).xc := by
  rw [mulPull_genericX' W K h, ← AlgEquiv.coe_algHom, ← Point.xc_map (W := W) (K := K),
    map_negEquiv_zsmul_genericPoint, Point.eq_some_xc_yc h.1, Point.neg_some, Point.xc_some, Point.xc_some]

theorem negEquiv_mulPull_genericY' {n : ℤ} (h : MulGood W K n) :
    negEquiv W K (mulPull W K n (genericY W K)) =
      (W⁄(W⁄K).FunctionField).negY (n • genericPoint W K).xc (n • genericPoint W K).yc := by
  rw [mulPull_genericY' W K h, ← AlgEquiv.coe_algHom, ← Point.yc_map (W := W) (K := K),
    map_negEquiv_zsmul_genericPoint]
  conv_lhs => rw [Point.eq_some_xc_yc h.1, Point.neg_some, Point.yc_some]

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in
theorem mulPull_injective [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] (n : ℤ) :
    Function.Injective (mulPull W K n) := (mulPull W K n).injective

end TransMul

section Places

variable {R : Type*} [Field R] (W : WeierstrassCurve R) (K : Type*) [Field K] [Algebra R K]
  [DecidableEq K]

noncomputable def placeOf (P : (W⁄K).Point) (hP : P ≠ 0) :
    IsDedekindDomain.HeightOneSpectrum (W⁄K).CoordinateRing where
  asIdeal := CoordinateRing.XYIdeal (W⁄K) P.xc (C P.yc)
  isPrime := (CoordinateRing.XYIdeal_isMaximal (Point.nonsingular_xc_yc hP).left).isPrime
  ne_bot h := CoordinateRing.XClass_ne_zero (W' := W⁄K) P.xc
    (by rw [← Ideal.mem_bot, ← h]; exact Ideal.subset_span (Set.mem_insert _ _))

omit [DecidableEq K] in
@[simp] theorem placeOf_asIdeal (P : (W⁄K).Point) (hP : P ≠ 0) :
    (placeOf W K P hP).asIdeal = CoordinateRing.XYIdeal (W⁄K) P.xc (C P.yc) := rfl

omit [DecidableEq K] in

theorem placeOf_surjective [IsAlgClosed K] [W.IsElliptic]
    (v : IsDedekindDomain.HeightOneSpectrum (W⁄K).CoordinateRing) :
    ∃ (P : (W⁄K).Point) (hP : P ≠ 0), placeOf W K P hP = v := by
  haveI : (W⁄K).IsElliptic := by
    dsimp only [Affine.baseChange, WeierstrassCurve.baseChange]; infer_instance
  haveI := v.isPrime
  obtain ⟨a, b, hab, hv⟩ := CoordinateRing.exists_eq_XYIdeal v.ne_bot
  refine ⟨.some a b ((equation_iff_nonsingular (W := W⁄K)).mp hab), Point.some_ne_zero _, ?_⟩
  exact IsDedekindDomain.HeightOneSpectrum.ext hv.symm

noncomputable def CoordinateRing.evalAt {a b : K} (h : (W⁄K).Equation a b) : (W⁄K).CoordinateRing →+* K :=
  AdjoinRoot.evalEval h

omit [DecidableEq K] in
theorem CoordinateRing.evalAt_mk {a b : K} (h : (W⁄K).Equation a b) (g : K[X][Y]) :
    CoordinateRing.evalAt W K h (CoordinateRing.mk (W⁄K) g) = g.evalEval a b :=
  AdjoinRoot.evalEval_mk h g

omit [DecidableEq K] in
theorem CoordinateRing.evalAt_XYIdeal {a b : K} (h : (W⁄K).Equation a b) :
    ∀ g ∈ CoordinateRing.XYIdeal (W⁄K) a (C b), CoordinateRing.evalAt W K h g = 0 := by
  intro g hg
  rw [← RingHom.mem_ker]
  revert hg g
  rw [← SetLike.le_def, CoordinateRing.XYIdeal, Ideal.span_le]
  rintro g (rfl | rfl)
  · rw [SetLike.mem_coe, RingHom.mem_ker, CoordinateRing.XClass, CoordinateRing.evalAt_mk,
      evalEval_C, eval_sub, eval_X, eval_C, sub_self]
  · rw [SetLike.mem_coe, RingHom.mem_ker, CoordinateRing.YClass, CoordinateRing.evalAt_mk,
      evalEval_sub, evalEval_X, evalEval_C, eval_C, sub_self]

omit [DecidableEq K] in
theorem placeOf_injective {P Q : (W⁄K).Point} (hP : P ≠ 0) (hQ : Q ≠ 0)
    (h : placeOf W K P hP = placeOf W K Q hQ) : P = Q := by
  have hI : CoordinateRing.XYIdeal (W⁄K) P.xc (C P.yc) = CoordinateRing.XYIdeal (W⁄K) Q.xc (C Q.yc) :=
    congrArg IsDedekindDomain.HeightOneSpectrum.asIdeal h
  have hev := CoordinateRing.evalAt_XYIdeal W K (Point.nonsingular_xc_yc hP).left
  rw [hI] at hev
  have hx : P.xc = Q.xc := by
    have := hev _ (Ideal.subset_span (Set.mem_insert _ _))
    rw [CoordinateRing.XClass, CoordinateRing.evalAt_mk, evalEval_C, eval_sub, eval_X, eval_C,
      sub_eq_zero] at this
    exact this
  have hy : P.yc = Q.yc := by
    have := hev _ (Ideal.subset_span (Set.mem_insert_of_mem _ rfl))
    rw [CoordinateRing.YClass, CoordinateRing.evalAt_mk, evalEval_sub, evalEval_X, evalEval_C, eval_C,
      sub_eq_zero] at this
    exact this
  rw [Point.eq_some_xc_yc hP, Point.eq_some_xc_yc hQ]
  congr 1

end Places

end WeierstrassCurve.Affine

open Polynomial

namespace Valuation

variable {L : Type*} [CommRing L] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)

def Cong (a b : L) : Prop := v (a - b) < 1

variable {v}

theorem cong_iff {a b : L} : v.Cong a b ↔ v (a - b) < 1 := Iff.rfl

@[refl] theorem Cong.refl (a : L) : v.Cong a a := by simp [Cong]

theorem Cong.rfl {a : L} : v.Cong a a := Cong.refl a

@[symm] theorem Cong.symm {a b : L} (h : v.Cong a b) : v.Cong b a := by
  rw [Cong, ← Valuation.map_neg, neg_sub]; exact h

theorem Cong.trans {a b c : L} (h₁ : v.Cong a b) (h₂ : v.Cong b c) : v.Cong a c := by
  have : a - c = (a - b) + (b - c) := by ring
  rw [Cong, this]
  exact (v.map_add _ _).trans_lt (max_lt h₁ h₂)

theorem Cong.add {a b a' b' : L} (h₁ : v.Cong a a') (h₂ : v.Cong b b') : v.Cong (a + b) (a' + b') := by
  have : a + b - (a' + b') = (a - a') + (b - b') := by ring
  rw [Cong, this]
  exact (v.map_add _ _).trans_lt (max_lt h₁ h₂)

theorem Cong.neg {a a' : L} (h : v.Cong a a') : v.Cong (-a) (-a') := by
  have : -a - -a' = -(a - a') := by ring
  rw [Cong, this, Valuation.map_neg]; exact h

theorem Cong.sub {a b a' b' : L} (h₁ : v.Cong a a') (h₂ : v.Cong b b') : v.Cong (a - b) (a' - b') := by
  rw [sub_eq_add_neg, sub_eq_add_neg]; exact h₁.add h₂.neg

theorem Cong.le_one {a a' : L} (h : v.Cong a a') (ha' : v a' ≤ 1) : v a ≤ 1 := by
  have : a = (a - a') + a' := by ring
  rw [this]
  exact (v.map_add _ _).trans (max_le h.le ha')

theorem Cong.mul {a b a' b' : L} (h₁ : v.Cong a a') (h₂ : v.Cong b b') (ha' : v a' ≤ 1)
    (hb' : v b' ≤ 1) : v.Cong (a * b) (a' * b') := by
  have ha : v a ≤ 1 := h₁.le_one ha'
  have : a * b - a' * b' = a * (b - b') + (a - a') * b' := by ring
  rw [Cong, this]
  refine (v.map_add _ _).trans_lt (max_lt ?_ ?_)
  · rw [Valuation.map_mul]
    calc v a * v (b - b') ≤ 1 * v (b - b') := mul_le_mul' ha le_rfl
      _ < 1 := by rw [one_mul]; exact h₂
  · rw [Valuation.map_mul]
    calc v (a - a') * v b' ≤ v (a - a') * 1 := mul_le_mul' le_rfl hb'
      _ < 1 := by rw [mul_one]; exact h₁

theorem Cong.pow {a a' : L} (h : v.Cong a a') (ha' : v a' ≤ 1) (n : ℕ) : v.Cong (a ^ n) (a' ^ n) := by
  induction n with
  | zero => simp only [pow_zero]; exact Cong.rfl
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul h (by rw [Valuation.map_pow]; exact pow_le_one' ha' n) ha'

theorem Cong.eq_of_eq_one {a a' : L} (h : v.Cong a a') (ha' : v a' = 1) : v a = 1 := by
  have : a = a' + (a - a') := by ring
  rw [this, Valuation.map_add_eq_of_lt_left]
  · exact ha'
  · rw [ha']; exact h

theorem Cong.lt_one_iff {a a' : L} (h : v.Cong a a') : v a < 1 ↔ v a' < 1 := by
  constructor
  · intro ha
    have : a' = a - (a - a') := by ring
    rw [this]
    exact (v.map_sub _ _).trans_lt (max_lt ha h)
  · intro ha'
    have : a = (a - a') + a' := by ring
    rw [this]
    exact (v.map_add _ _).trans_lt (max_lt h ha')

theorem cong_zero_iff {a : L} : v.Cong a 0 ↔ v a < 1 := by rw [Cong, sub_zero]

section Field

variable {F : Type*} [Field F] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] {w : Valuation F Γ}

theorem Cong.inv {d d' : F} (h : w.Cong d d') (hd' : w d' = 1) : w.Cong d⁻¹ d'⁻¹ := by
  have hd : w d = 1 := h.eq_of_eq_one hd'
  have hd0 : d ≠ 0 := fun h0 => by rw [h0, Valuation.map_zero] at hd; exact zero_ne_one hd
  have hd0' : d' ≠ 0 := fun h0 => by rw [h0, Valuation.map_zero] at hd'; exact zero_ne_one hd'
  have : d⁻¹ - d'⁻¹ = -(d - d') * (d⁻¹ * d'⁻¹) := by
    field_simp
    ring
  rw [Cong, this, Valuation.map_mul, Valuation.map_neg, Valuation.map_mul, map_inv₀, map_inv₀, hd, hd',
    inv_one, mul_one, mul_one]
  exact h

theorem Cong.div {a d a' d' : F} (h₁ : w.Cong a a') (h₂ : w.Cong d d') (ha' : w a' ≤ 1)
    (hd' : w d' = 1) : w.Cong (a / d) (a' / d') := by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact h₁.mul (h₂.inv hd') ha' (by rw [map_inv₀, hd', inv_one])

end Field

section Eval

variable {K : Type*} [CommRing K] (f : K →+* L)

theorem Cong.eval₂ (hf : ∀ c, v (f c) ≤ 1) {a a' : L} (h : v.Cong a a') (ha' : v a' ≤ 1) (p : K[X]) :
    v.Cong (p.eval₂ f a) (p.eval₂ f a') ∧ v (p.eval₂ f a') ≤ 1 := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq =>
    rw [eval₂_add, eval₂_add]
    exact ⟨hp.1.add hq.1, (v.map_add _ _).trans (max_le hp.2 hq.2)⟩
  | monomial n c =>
    rw [eval₂_monomial, eval₂_monomial]
    have hpow : v (a' ^ n) ≤ 1 := by rw [Valuation.map_pow]; exact pow_le_one' ha' n
    exact ⟨(Cong.refl (f c)).mul (h.pow ha' n) (hf c) hpow,
      by rw [Valuation.map_mul]; exact mul_le_one' (hf c) hpow⟩

theorem Cong.eval₂_eval₂ (hf : ∀ c, v (f c) ≤ 1) {a a' b b' : L} (ha : v.Cong a a') (ha' : v a' ≤ 1)
    (hb : v.Cong b b') (hb' : v b' ≤ 1) (p : K[X][X]) :
    v.Cong (p.eval₂ (eval₂RingHom f a) b) (p.eval₂ (eval₂RingHom f a') b') ∧
      v (p.eval₂ (eval₂RingHom f a') b') ≤ 1 := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq =>
    rw [eval₂_add, eval₂_add]
    exact ⟨hp.1.add hq.1, (v.map_add _ _).trans (max_le hp.2 hq.2)⟩
  | monomial n q =>
    rw [eval₂_monomial, eval₂_monomial, coe_eval₂RingHom, coe_eval₂RingHom]
    have hq := Cong.eval₂ f hf ha ha' q
    have hpow : v (b' ^ n) ≤ 1 := by rw [Valuation.map_pow]; exact pow_le_one' hb' n
    exact ⟨hq.1.mul (hb.pow hb' n) hq.2 hpow, by rw [Valuation.map_mul]; exact mul_le_one' hq.2 hpow⟩

end Eval

end Valuation

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum WithZero

namespace IsDedekindDomain.HeightOneSpectrum

variable {R : Type*} [CommRing R] [IsDedekindDomain R] {K : Type*} [Field K] [Algebra R K]
  [IsFractionRing R K] {R' : Type*} [CommRing R'] [IsDedekindDomain R'] {K' : Type*} [Field K']
  [Algebra R' K'] [IsFractionRing R' K']

omit [IsDedekindDomain R] [IsFractionRing R K] in

theorem valuation_map_le_exp_neg_of_mem_pow (ψ : K →+* K') (w : HeightOneSpectrum R)
    (v : HeightOneSpectrum R')
    (h0 : ∀ b : R, v.valuation K' (ψ (algebraMap R K b)) ≤ 1)
    (h1 : ∀ b : R, b ∈ w.asIdeal → v.valuation K' (ψ (algebraMap R K b)) ≤ exp (-1 : ℤ))
    (m : ℕ) : ∀ a ∈ w.asIdeal ^ m, v.valuation K' (ψ (algebraMap R K a)) ≤ exp (-(m : ℤ)) := by
  induction m with
  | zero =>
    intro a _
    rw [Nat.cast_zero, neg_zero, exp_zero]
    exact h0 a
  | succ m ih =>
    intro a ha
    rw [pow_succ'] at ha
    refine Submodule.mul_induction_on ha ?_ ?_
    · intro c hc a' ha'
      rw [map_mul, map_mul, map_mul, Nat.cast_succ, neg_add, add_comm, exp_add]
      exact mul_le_mul' (h1 c hc) (ih a' ha')
    · intro z₁ z₂ hz₁ hz₂
      rw [map_add, map_add]
      exact (Valuation.map_add _ _ _).trans (max_le hz₁ hz₂)

theorem valuation_map_le_of_valuation_le (ψ : K →+* K') (w : HeightOneSpectrum R)
    (v : HeightOneSpectrum R')
    (h1 : ∀ b : R, b ∈ w.asIdeal → v.valuation K' (ψ (algebraMap R K b)) ≤ exp (-1 : ℤ))
    (h2 : ∀ b : R, b ∉ w.asIdeal → v.valuation K' (ψ (algebraMap R K b)) = 1)
    (x : K) (k : ℕ) (hx : w.valuation K x ≤ exp (-(k : ℤ))) :
    v.valuation K' (ψ x) ≤ exp (-(k : ℤ)) := by
  have h0 : ∀ b : R, v.valuation K' (ψ (algebraMap R K b)) ≤ 1 := by
    intro b
    by_cases hb : b ∈ w.asIdeal
    · exact (h1 b hb).trans (by rw [← exp_zero, exp_le_exp]; norm_num)
    · exact (h2 b hb).le
  have hx1 : w.valuation K x ≤ 1 :=
    hx.trans (by rw [← exp_zero, exp_le_exp, neg_nonpos]; exact Nat.cast_nonneg k)
  obtain ⟨n, d, hnd⟩ := exists_primeCompl_mul_eq_of_integer (v := w) x hx1
  have hd : (d : R) ∉ w.asIdeal := d.2

  have hwn : w.valuation K (algebraMap R K n) ≤ exp (-(k : ℤ)) := by
    rw [← hnd, map_mul, (valuation_eq_one_iff_notMem (K := K) w).mpr hd, mul_one]
    exact hx
  rw [valuation_of_algebraMap, intValuation_le_pow_iff_mem] at hwn
  have hψn := valuation_map_le_exp_neg_of_mem_pow ψ w v h0 h1 k n hwn

  have := congrArg (fun t => v.valuation K' (ψ t)) hnd
  simp only [map_mul, h2 d hd, mul_one] at this
  rw [this]
  exact hψn

end IsDedekindDomain.HeightOneSpectrum

namespace WeierstrassCurve.Affine

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum WithZero Polynomial

section Transport

variable {R : Type*} [Field R] (W : WeierstrassCurve R) (K : Type*) [Field K] [Algebra R K]
  [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] [IsDedekindDomain (W⁄K).CoordinateRing]

theorem _root_.WithZero.lt_one_iff_le_exp_neg_one {y : ℤᵐ⁰} : y < 1 ↔ y ≤ exp (-1 : ℤ) := by
  by_cases hy : y = 0
  · subst hy; simp
  · rw [← exp_log hy, ← exp_zero, exp_lt_exp, exp_le_exp]; omega

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in

theorem valuation_algebraMap_le_one (P : (W⁄K).Point) (hP : P ≠ 0) (c : K) :
    (placeOf W K P hP).valuation (W⁄K).FunctionField (algebraMap K (W⁄K).FunctionField c) ≤ 1 := by
  rw [IsScalarTower.algebraMap_apply K (W⁄K).CoordinateRing (W⁄K).FunctionField]
  exact valuation_le_one _ _

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in

theorem valuation_algebraMap_eq_one (P : (W⁄K).Point) (hP : P ≠ 0) {c : K} (hc : c ≠ 0) :
    (placeOf W K P hP).valuation (W⁄K).FunctionField (algebraMap K (W⁄K).FunctionField c) = 1 := by
  apply le_antisymm (valuation_algebraMap_le_one W K P hP c)
  have h := valuation_algebraMap_le_one W K P hP c⁻¹
  rw [map_inv₀, map_inv₀, inv_le_one₀] at h
  · exact h
  · rw [Valuation.pos_iff]
    exact (_root_.map_ne_zero _).mpr hc

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] [IsDedekindDomain (W⁄K).CoordinateRing] in

theorem mem_placeOf_iff (P : (W⁄K).Point) (hP : P ≠ 0) (b : (W⁄K).CoordinateRing) :
    b ∈ (placeOf W K P hP).asIdeal ↔ CoordinateRing.evalAt W K (Point.nonsingular_xc_yc hP).left b = 0 := by
  constructor
  · exact CoordinateRing.evalAt_XYIdeal W K _ b
  · intro hb
    have hker : RingHom.ker (CoordinateRing.evalAt W K (Point.nonsingular_xc_yc hP).left) =
        (placeOf W K P hP).asIdeal := by
      refine ((CoordinateRing.XYIdeal_isMaximal (Point.nonsingular_xc_yc hP).left).eq_of_le
        (RingHom.ker_ne_top _) ?_).symm
      intro g hg
      exact (RingHom.mem_ker).mpr (CoordinateRing.evalAt_XYIdeal W K _ g hg)
    rw [← hker]
    exact (RingHom.mem_ker).mpr hb

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in
theorem cong_genericX (P : (W⁄K).Point) (hP : P ≠ 0) :
    ((placeOf W K P hP).valuation (W⁄K).FunctionField).Cong (genericX W K)
      (algebraMap K (W⁄K).FunctionField P.xc) := by
  rw [Valuation.cong_iff, IsScalarTower.algebraMap_apply K (W⁄K).CoordinateRing (W⁄K).FunctionField, genericX,
    ← map_sub]
  apply (valuation_lt_one_iff_mem _ _).mpr
  rw [placeOf_asIdeal]
  have : CoordinateRing.mk (W⁄K) (C X) - algebraMap K (W⁄K).CoordinateRing P.xc =
      CoordinateRing.XClass (W⁄K) P.xc := by
    rw [CoordinateRing.XClass, map_sub, map_sub]; rfl
  rw [this]
  exact Ideal.subset_span (Set.mem_insert _ _)

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in
theorem cong_genericY (P : (W⁄K).Point) (hP : P ≠ 0) :
    ((placeOf W K P hP).valuation (W⁄K).FunctionField).Cong (genericY W K)
      (algebraMap K (W⁄K).FunctionField P.yc) := by
  rw [Valuation.cong_iff, IsScalarTower.algebraMap_apply K (W⁄K).CoordinateRing (W⁄K).FunctionField, genericY,
    ← map_sub]
  apply (valuation_lt_one_iff_mem _ _).mpr
  rw [placeOf_asIdeal]
  have : CoordinateRing.mk (W⁄K) Y - algebraMap K (W⁄K).CoordinateRing P.yc =
      CoordinateRing.YClass (W⁄K) (C P.yc) := by
    rw [CoordinateRing.YClass, map_sub]; rfl
  rw [this]
  exact Ideal.subset_span (Set.mem_insert_of_mem _ rfl)

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] [IsDedekindDomain (W⁄K).CoordinateRing] in

theorem algebraMap_evalEval (g : K[X][Y]) (a b : K) :
    algebraMap K (W⁄K).FunctionField (g.evalEval a b) =
      g.eval₂ (eval₂RingHom (algebraMap K (W⁄K).FunctionField) (algebraMap K _ a)) (algebraMap K _ b) := by
  have hφ : (algebraMap K (W⁄K).FunctionField).comp (evalEvalRingHom a b) =
      eval₂RingHom (eval₂RingHom (algebraMap K (W⁄K).FunctionField) (algebraMap K _ a)) (algebraMap K _ b) := by
    apply Polynomial.ringHom_ext
    · intro q
      simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_C, coe_eval₂RingHom,
        eval₂_C, eval₂_at_apply]
    · simp only [RingHom.coe_comp, Function.comp_apply, coe_evalRingHom, eval_X, eval_C, coe_eval₂RingHom,
        eval₂_X]
  exact RingHom.congr_fun hφ g

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] [IsDedekindDomain (W⁄K).CoordinateRing] in
theorem pointHom_mk_eq_eval₂ (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0) (g : K[X][Y]) :
    pointHom Q hQ (CoordinateRing.mk (W⁄K) g) =
      g.eval₂ (eval₂RingHom (algebraMap K (W⁄K).FunctionField) Q.xc) Q.yc := by
  rw [pointHom_mk]
  congr 1

omit [DecidableEq K] [IsAlgClosed K] [W.IsElliptic] in

theorem valuation_pointPull_le (Q : (W⁄(W⁄K).FunctionField).Point) (hQ : Q ≠ 0)
    (hinj : Function.Injective (pointHom Q hQ)) {P : (W⁄K).Point} (hP : P ≠ 0) {P' : (W⁄K).Point}
    (hP' : P' ≠ 0)
    (hx : ((placeOf W K P hP).valuation (W⁄K).FunctionField).Cong Q.xc (algebraMap K _ P'.xc))
    (hy : ((placeOf W K P hP).valuation (W⁄K).FunctionField).Cong Q.yc (algebraMap K _ P'.yc))
    (h : (W⁄K).FunctionField) (k : ℕ)
    (hh : (placeOf W K P' hP').valuation (W⁄K).FunctionField h ≤ exp (-(k : ℤ))) :
    (placeOf W K P hP).valuation (W⁄K).FunctionField (pointPull Q hQ hinj h) ≤ exp (-(k : ℤ)) := by
  set v := (placeOf W K P hP).valuation (W⁄K).FunctionField with hv
  have hc : ∀ g : K[X][Y], v.Cong (pointHom Q hQ (CoordinateRing.mk (W⁄K) g))
      (algebraMap K _ (g.evalEval P'.xc P'.yc)) := by
    intro g
    rw [pointHom_mk_eq_eval₂, algebraMap_evalEval]
    exact (Valuation.Cong.eval₂_eval₂ (v := v) (algebraMap K _) (valuation_algebraMap_le_one W K P hP)
      hx (valuation_algebraMap_le_one W K P hP _) hy (valuation_algebraMap_le_one W K P hP _) g).1
  refine valuation_map_le_of_valuation_le (pointPull Q hQ hinj : (W⁄K).FunctionField →+* (W⁄K).FunctionField)
    (placeOf W K P' hP') (placeOf W K P hP) ?_ ?_ h k hh
  · intro b hb
    obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective b
    change v (pointPull Q hQ hinj (algebraMap _ _ (CoordinateRing.mk (W⁄K) g))) ≤ _
    rw [pointPull_algebraMap, ← lt_one_iff_le_exp_neg_one, ← Valuation.cong_zero_iff]
    have h0 : g.evalEval P'.xc P'.yc = 0 := by
      rw [← CoordinateRing.evalAt_mk W K (Point.nonsingular_xc_yc hP').left]
      exact (mem_placeOf_iff W K P' hP' _).mp hb
    simpa only [h0, map_zero] using hc g
  · intro b hb
    obtain ⟨g, rfl⟩ := Ideal.Quotient.mk_surjective b
    change v (pointPull Q hQ hinj (algebraMap _ _ (CoordinateRing.mk (W⁄K) g))) = 1
    rw [pointPull_algebraMap]
    have h0 : g.evalEval P'.xc P'.yc ≠ 0 := by
      rw [← CoordinateRing.evalAt_mk W K (Point.nonsingular_xc_yc hP').left]
      exact fun h => hb ((mem_placeOf_iff W K P' hP' _).mpr h)
    exact (hc g).eq_of_eq_one (valuation_algebraMap_eq_one W K P hP h0)

theorem valuation_mulPull_le {n : ℤ} (hgood : MulGood W K n) (Φ Ψ : K[X]) (ω ψ : K[X][Y])
    (hξ : (n • genericPoint W K).xc =
      Φ.eval₂ (algebraMap K (W⁄K).FunctionField) (genericX W K) /
        Ψ.eval₂ (algebraMap K (W⁄K).FunctionField) (genericX W K))
    (hη : (n • genericPoint W K).yc =
      ω.eval₂ (eval₂RingHom (algebraMap K (W⁄K).FunctionField) (genericX W K)) (genericY W K) /
        ψ.eval₂ (eval₂RingHom (algebraMap K (W⁄K).FunctionField) (genericX W K)) (genericY W K) ^ 3)
    {P : (W⁄K).Point} (hP : P ≠ 0) (hnP : n • P ≠ 0)
    (hxP : (n • P).xc = Φ.eval P.xc / Ψ.eval P.xc) (hΨ : Ψ.eval P.xc ≠ 0)
    (hyP : (n • P).yc = ω.evalEval P.xc P.yc / ψ.evalEval P.xc P.yc ^ 3) (hψ : ψ.evalEval P.xc P.yc ≠ 0)
    (h : (W⁄K).FunctionField) (k : ℕ)
    (hh : (placeOf W K (n • P) hnP).valuation (W⁄K).FunctionField h ≤ exp (-(k : ℤ))) :
    (placeOf W K P hP).valuation (W⁄K).FunctionField (mulPull W K n h) ≤ exp (-(k : ℤ)) := by
  set v := (placeOf W K P hP).valuation (W⁄K).FunctionField with hv
  have hc1 := valuation_algebraMap_le_one W K P hP
  have hX := cong_genericX W K P hP
  have hY := cong_genericY W K P hP

  have hx : v.Cong (n • genericPoint W K).xc (algebraMap K _ (n • P).xc) := by
    rw [hξ, hxP, map_div₀, ← eval₂_at_apply, ← eval₂_at_apply]
    have hΦ := Valuation.Cong.eval₂ (v := v) (algebraMap K _) hc1 hX (hc1 _) Φ
    have hΨc := Valuation.Cong.eval₂ (v := v) (algebraMap K _) hc1 hX (hc1 _) Ψ
    refine hΦ.1.div hΨc.1 hΦ.2 ?_
    rw [eval₂_at_apply]
    exact valuation_algebraMap_eq_one W K P hP hΨ

  have hy : v.Cong (n • genericPoint W K).yc (algebraMap K _ (n • P).yc) := by
    rw [hη, hyP, map_div₀, map_pow, algebraMap_evalEval, algebraMap_evalEval]
    have hω := Valuation.Cong.eval₂_eval₂ (v := v) (algebraMap K _) hc1 hX (hc1 _) hY (hc1 _) ω
    have hψc := Valuation.Cong.eval₂_eval₂ (v := v) (algebraMap K _) hc1 hX (hc1 _) hY (hc1 _) ψ
    refine hω.1.div (hψc.1.pow hψc.2 3) hω.2 ?_
    rw [← algebraMap_evalEval, ← map_pow]
    exact valuation_algebraMap_eq_one W K P hP (pow_ne_zero 3 hψ)
  rw [mulPull_eq W K hgood]
  exact valuation_pointPull_le W K _ _ _ hP hnP hx hy h k hh

end Transport

end WeierstrassCurve.Affine