import Definitions.Def_WeierstrassCurve_TorsionIntegral

set_option autoImplicit false

open IsLocalRing

namespace ValuationSubring

variable {L : Type*} [Field L] (A : ValuationSubring L)

theorem div_mem_of_mem_of_notMem_nonunits {a b : L} (ha : a ∈ A) (hb : b ∉ A.nonunits) :
    a / b ∈ A := by
  rw [div_eq_mul_inv]
  exact A.toSubring.mul_mem ha (A.inv_mem_of_notMem_nonunits hb)

theorem residue_ne_zero_of_notMem_nonunits {b : L} (hb : b ∈ A) (hb' : b ∉ A.nonunits) :
    residue A ⟨b, hb⟩ ≠ 0 := fun h =>
  hb' ((A.coe_mem_nonunits_iff_residue_eq_zero ⟨b, hb⟩).mpr h)

theorem residue_eq_of_coe_eq {a : L} (ha : a ∈ A) {v : A} (hav : a = (v : L)) :
    residue A ⟨a, ha⟩ = residue A v :=
  congrArg (residue A) (Subtype.ext hav)

theorem residue_div {a b : L} (ha : a ∈ A) (hb : b ∈ A) (hb' : b ∉ A.nonunits)
    (hq : a / b ∈ A) :
    residue A ⟨a / b, hq⟩ = residue A ⟨a, ha⟩ / residue A ⟨b, hb⟩ := by
  have hb0 : b ≠ 0 := A.ne_zero_of_notMem_nonunits hb'
  have hbres : residue A ⟨b, hb⟩ ≠ 0 := A.residue_ne_zero_of_notMem_nonunits hb hb'
  rw [eq_div_iff hbres, ← map_mul]
  refine congrArg (residue A) (Subtype.ext ?_)
  push_cast
  exact div_mul_cancel₀ a hb0

theorem residue_eq_div_of_eq_div {a c d : L} (ha : a ∈ A) (hc : c ∈ A) (hd : d ∈ A)
    (hd' : d ∉ A.nonunits) (hacd : a = c / d) :
    residue A ⟨a, ha⟩ = residue A ⟨c, hc⟩ / residue A ⟨d, hd⟩ := by
  rw [A.residue_eq_of_coe_eq ha
    (v := ⟨c / d, A.div_mem_of_mem_of_notMem_nonunits hc hd'⟩) hacd]
  exact A.residue_div hc hd hd' _

theorem residue_eq_residue_iff_sub_mem_nonunits {a b : L} (ha : a ∈ A) (hb : b ∈ A) :
    residue A ⟨a, ha⟩ = residue A ⟨b, hb⟩ ↔ a - b ∈ A.nonunits := by
  constructor
  · intro h
    have h0 : residue A (⟨a, ha⟩ - ⟨b, hb⟩) = 0 := by rw [map_sub, h, sub_self]
    have := (A.coe_mem_nonunits_iff_residue_eq_zero _).mpr h0
    simpa using this
  · intro h
    have h0 : residue A (⟨a, ha⟩ - ⟨b, hb⟩) = 0 :=
      (A.coe_mem_nonunits_iff_residue_eq_zero _).mp (by simpa using h)
    rw [map_sub, sub_eq_zero] at h0
    exact h0

end ValuationSubring

namespace WeierstrassCurve

variable {L : Type*} [Field L] {A : ValuationSubring L} (W : WeierstrassCurve A)

private lemma some_congr' {R : Type*} [CommRing R] {V : Affine R} {x₁ x₂ y₁ y₂ : R}
    (hx : x₁ = x₂) (hy : y₁ = y₂) (h₁ : V.Nonsingular x₁ y₁) (h₂ : V.Nonsingular x₂ y₂) :
    Affine.Point.some x₁ y₁ h₁ = Affine.Point.some x₂ y₂ h₂ := by
  subst hx; subst hy; rfl

section Coercion

variable {W}

lemma coe_negY {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    ((W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩ : A) : L) = (W.map A.subtype).toAffine.negY x y :=
  (Affine.map_negY A.subtype (⟨x, hx⟩ : A) (⟨y, hy⟩ : A)).symm

lemma negY_mem {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    (W.map A.subtype).toAffine.negY x y ∈ A := by
  rw [← coe_negY hx hy]
  exact SetLike.coe_mem _

lemma residue_negY {x y : L} (hx : x ∈ A) (hy : y ∈ A) :
    residue A (W.toAffine.negY ⟨x, hx⟩ ⟨y, hy⟩) =
      (W.map (residue A)).toAffine.negY (residue A ⟨x, hx⟩) (residue A ⟨y, hy⟩) :=
  (Affine.map_negY (residue A) (⟨x, hx⟩ : A) (⟨y, hy⟩ : A)).symm

lemma residue_sub_negY {x₂ y₁ y₂ : L} (hy₁ : y₁ ∈ A) (hx₂ : x₂ ∈ A) (hy₂ : y₂ ∈ A)
    (hmem : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A) :
    residue A ⟨y₁ - (W.map A.subtype).toAffine.negY x₂ y₂, hmem⟩ =
      residue A ⟨y₁, hy₁⟩ -
        (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
  rw [A.residue_eq_of_coe_eq hmem (v := ⟨y₁, hy₁⟩ - W.toAffine.negY ⟨x₂, hx₂⟩ ⟨y₂, hy₂⟩)
    (by push_cast; rw [coe_negY hx₂ hy₂]), map_sub, residue_negY hx₂ hy₂]

lemma residue_inverse_iff {x₁ y₁ x₂ y₂ : L} (hx₁ : x₁ ∈ A) (hy₁ : y₁ ∈ A) (hx₂ : x₂ ∈ A)
    (hy₂ : y₂ ∈ A) :
    (residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ ∧
        residue A ⟨y₁, hy₁⟩ =
          (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩)) ↔
      (x₁ - x₂ ∈ A.nonunits ∧
        y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits) := by
  have hnegA : (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A := negY_mem hx₂ hy₂
  have h1 := A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂
  have h2 := A.residue_eq_residue_iff_sub_mem_nonunits hy₁ hnegA
  have h3 : residue A ⟨(W.map A.subtype).toAffine.negY x₂ y₂, hnegA⟩ =
      (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
    rw [A.residue_eq_of_coe_eq hnegA (v := W.toAffine.negY ⟨x₂, hx₂⟩ ⟨y₂, hy₂⟩)
      (coe_negY hx₂ hy₂).symm]
    exact residue_negY hx₂ hy₂
  rw [← h3]
  exact and_congr h1 h2

end Coercion

section Slope

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W}

theorem slope_mem_residue_of_not_inverse
    {x₁ y₁ x₂ y₂ : L} (h₁ : (W.map A.subtype).toAffine.Equation x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Equation x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A)
    (hred : ¬(x₁ - x₂ ∈ A.nonunits ∧
      y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits)) :
    ∃ hs : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A,
      residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hs⟩ =
        (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
          (residue A ⟨y₁, Affine.Y_mem_of_X_mem W h₁ hx₁⟩)
          (residue A ⟨y₂, Affine.Y_mem_of_X_mem W h₂ hx₂⟩) := by
  have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁ hx₁
  have hy₂ : y₂ ∈ A := Affine.Y_mem_of_X_mem W h₂ hx₂
  have ha₁ : (W.map A.subtype).toAffine.a₁ ∈ A := SetLike.coe_mem W.a₁
  have ha₂ : (W.map A.subtype).toAffine.a₂ ∈ A := SetLike.coe_mem W.a₂
  have ha₄ : (W.map A.subtype).toAffine.a₄ ∈ A := SetLike.coe_mem W.a₄

  have hk₁ : (W.map (residue A)).toAffine.Equation (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩) :=
    Affine.equation_residue W (x := ⟨x₁, hx₁⟩) (y := ⟨y₁, hy₁⟩) h₁
  have hk₂ : (W.map (residue A)).toAffine.Equation (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) :=
    Affine.equation_residue W (x := ⟨x₂, hx₂⟩) (y := ⟨y₂, hy₂⟩) h₂

  have ha₁k : (W.map (residue A)).toAffine.a₁ = residue A W.a₁ := rfl
  have ha₂k : (W.map (residue A)).toAffine.a₂ = residue A W.a₂ := rfl
  have ha₄k : (W.map (residue A)).toAffine.a₄ = residue A W.a₄ := rfl
  by_cases hxx : x₁ - x₂ ∈ A.nonunits
  ·

    have hyy : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∉ A.nonunits := fun h => hred ⟨hxx, h⟩
    have hyyA : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A :=
      A.toSubring.sub_mem hy₁ (negY_mem hx₂ hy₂)
    have hyy0 : y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ≠ 0 :=
      A.ne_zero_of_notMem_nonunits hyy

    have hxk : residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ :=
      (A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂).mpr hxx
    have hyk : residue A ⟨y₁, hy₁⟩ ≠
        (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩) := by
      intro h
      exact hyy (((residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mp ⟨hxk, h⟩).2)

    have hyk' : residue A ⟨y₁, hy₁⟩ = residue A ⟨y₂, hy₂⟩ :=
      Affine.Y_eq_of_Y_ne hk₁ hk₂ hxk hyk
    have hslope_k : (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩)
        (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) =
        (3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
            residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
            (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩) /
          (residue A ⟨y₁, hy₁⟩ -
            (W.map (residue A)).toAffine.negY (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩)) :=
      Affine.slope_of_Y_ne hxk hyk

    have hden_res : residue A ⟨y₁ - (W.map A.subtype).toAffine.negY x₂ y₂, hyyA⟩ =
        residue A ⟨y₁, hy₁⟩ -
          (W.map (residue A)).toAffine.negY (residue A ⟨x₁, hx₁⟩) (residue A ⟨y₁, hy₁⟩) := by
      rw [residue_sub_negY hy₁ hx₂ hy₂ hyyA, hxk, hyk']

    have hnum_mem : 3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
        (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ ∈ A := by
      refine A.toSubring.sub_mem (A.toSubring.add_mem (A.toSubring.add_mem ?_ ?_) ha₄)
        (A.toSubring.mul_mem ha₁ hy₁)
      · exact A.toSubring.mul_mem (by norm_num : (3 : L) ∈ A) (pow_mem hx₁ 2)
      · exact A.toSubring.mul_mem (A.toSubring.mul_mem (by norm_num : (2 : L) ∈ A) ha₂) hx₁
    have hnum_res : residue A ⟨3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
        (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁, hnum_mem⟩ =
        3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
          residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
          (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩ := by
      rw [A.residue_eq_of_coe_eq hnum_mem
        (v := 3 * ⟨x₁, hx₁⟩ ^ 2 + 2 * W.a₂ * ⟨x₁, hx₁⟩ + W.a₄ - W.a₁ * ⟨y₁, hy₁⟩)
        (by push_cast; rfl)]
      simp only [map_sub, map_add, map_mul, map_pow, map_ofNat]
      rw [ha₁k, ha₂k, ha₄k]
    by_cases hx : x₁ = x₂
    ·
      have hyL : y₁ ≠ (W.map A.subtype).toAffine.negY x₂ y₂ := fun h => hyy0 (by rw [h, sub_self])
      have hyL' : y₁ = y₂ := Affine.Y_eq_of_Y_ne h₁ h₂ hx hyL
      have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₁ y₁) :=
        Affine.slope_of_Y_ne hx hyL
      have hden_eq : y₁ - (W.map A.subtype).toAffine.negY x₁ y₁ =
          y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ := by
        rw [hx, hyL']
      have hslope_L' : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (3 * x₁ ^ 2 + 2 * (W.map A.subtype).toAffine.a₂ * x₁ +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by
        rw [hslope_L, hden_eq]
      have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
        rw [hslope_L']
        exact A.div_mem_of_mem_of_notMem_nonunits hnum_mem hyy
      refine ⟨hsmem, ?_⟩
      rw [A.residue_eq_div_of_eq_div hsmem hnum_mem hyyA hyy hslope_L', hslope_k, hnum_res,
        hden_res]
    ·

      have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂) :=
        Affine.slope_of_X_ne hx
      have hN_mem : x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) +
          (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁ ∈ A := by
        refine A.toSubring.sub_mem (A.toSubring.add_mem (A.toSubring.add_mem (A.toSubring.add_mem
          (A.toSubring.add_mem (pow_mem hx₁ 2) (A.toSubring.mul_mem hx₁ hx₂)) (pow_mem hx₂ 2))
          (A.toSubring.mul_mem ha₂ (A.toSubring.add_mem hx₁ hx₂))) ha₄)
          (A.toSubring.mul_mem ha₁ hy₁)

      have hslope_N : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ =
          (x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 + (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) +
              (W.map A.subtype).toAffine.a₄ - (W.map A.subtype).toAffine.a₁ * y₁) /
            (y₁ - (W.map A.subtype).toAffine.negY x₂ y₂) := by
        rw [hslope_L, div_eq_div_iff (sub_ne_zero.mpr hx) hyy0]
        linear_combination Affine.sub_mul_sub_negY h₁ h₂
      have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
        rw [hslope_N]
        exact A.div_mem_of_mem_of_notMem_nonunits hN_mem hyy
      refine ⟨hsmem, ?_⟩

      have hN_res : residue A ⟨x₁ ^ 2 + x₁ * x₂ + x₂ ^ 2 +
          (W.map A.subtype).toAffine.a₂ * (x₁ + x₂) + (W.map A.subtype).toAffine.a₄ -
          (W.map A.subtype).toAffine.a₁ * y₁, hN_mem⟩ =
          3 * residue A ⟨x₁, hx₁⟩ ^ 2 + 2 * (W.map (residue A)).toAffine.a₂ *
            residue A ⟨x₁, hx₁⟩ + (W.map (residue A)).toAffine.a₄ -
            (W.map (residue A)).toAffine.a₁ * residue A ⟨y₁, hy₁⟩ := by
        rw [A.residue_eq_of_coe_eq hN_mem
          (v := ⟨x₁, hx₁⟩ ^ 2 + ⟨x₁, hx₁⟩ * ⟨x₂, hx₂⟩ + ⟨x₂, hx₂⟩ ^ 2 +
            W.a₂ * (⟨x₁, hx₁⟩ + ⟨x₂, hx₂⟩) + W.a₄ - W.a₁ * ⟨y₁, hy₁⟩)
          (by push_cast; rfl)]
        simp only [map_sub, map_add, map_mul, map_pow]
        rw [ha₁k, ha₂k, ha₄k, ← hxk]
        ring
      rw [A.residue_eq_div_of_eq_div hsmem hN_mem hyyA hyy hslope_N, hslope_k, hN_res, hden_res]
  ·
    have hxL : x₁ ≠ x₂ := fun h => hxx (by rw [h, sub_self]; exact A.nonunits.zero_mem)
    have hxxA : x₁ - x₂ ∈ A := A.toSubring.sub_mem hx₁ hx₂
    have hslope_L : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂) :=
      Affine.slope_of_X_ne hxL
    have hyyA : y₁ - y₂ ∈ A := A.toSubring.sub_mem hy₁ hy₂
    have hsmem : (W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂ ∈ A := by
      rw [hslope_L]
      exact A.div_mem_of_mem_of_notMem_nonunits hyyA hxx
    refine ⟨hsmem, ?_⟩

    have hxk : residue A ⟨x₁, hx₁⟩ ≠ residue A ⟨x₂, hx₂⟩ := fun h =>
      hxx ((A.residue_eq_residue_iff_sub_mem_nonunits hx₁ hx₂).mp h)
    have hslope_k : (W.map (residue A)).toAffine.slope (residue A ⟨x₁, hx₁⟩)
        (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₁, hy₁⟩) (residue A ⟨y₂, hy₂⟩) =
        (residue A ⟨y₁, hy₁⟩ - residue A ⟨y₂, hy₂⟩) /
          (residue A ⟨x₁, hx₁⟩ - residue A ⟨x₂, hx₂⟩) := Affine.slope_of_X_ne hxk
    have hnum_eq : residue A ⟨y₁ - y₂, hyyA⟩ = residue A ⟨y₁, hy₁⟩ - residue A ⟨y₂, hy₂⟩ := by
      rw [A.residue_eq_of_coe_eq hyyA (v := ⟨y₁, hy₁⟩ - ⟨y₂, hy₂⟩) (by push_cast; ring), map_sub]
    have hden_eq : residue A ⟨x₁ - x₂, hxxA⟩ = residue A ⟨x₁, hx₁⟩ - residue A ⟨x₂, hx₂⟩ := by
      rw [A.residue_eq_of_coe_eq hxxA (v := ⟨x₁, hx₁⟩ - ⟨x₂, hx₂⟩) (by push_cast; ring), map_sub]
    rw [A.residue_eq_div_of_eq_div hsmem hyyA hxxA hxx hslope_L, hslope_k, hnum_eq, hden_eq]

end Slope

section IntegralCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

set_option maxHeartbeats 1600000 in

theorem reducePoint_add_of_mem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∈ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by
  have hy₁ : y₁ ∈ A := Affine.Y_mem_of_X_mem W h₁.1 hx₁
  have hy₂ : y₂ ∈ A := Affine.Y_mem_of_X_mem W h₂.1 hx₂

  rw [reducePoint_some_of_mem _ _ hx₁, reducePoint_some_of_mem _ _ hx₂]
  by_cases hred : x₁ - x₂ ∈ A.nonunits ∧
      y₁ - (W.map A.subtype).toAffine.negY x₂ y₂ ∈ A.nonunits
  ·
    obtain ⟨hredx, hredy⟩ := (residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mpr hred
    rw [Affine.Point.add_of_Y_eq hredx hredy]
    by_cases hPQ : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂
    ·
      rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2, reducePoint_zero]
    ·

      rw [Affine.Point.add_some hPQ]
      exact reducePoint_some_of_notMem _ _
        (Affine.addX_notMem_of_sub_mem_nonunits W hΔ h₁.1 h₂.1 hx₁ hx₂ hPQ hred.1 hred.2)
  ·

    obtain ⟨hsmem, hsres⟩ := slope_mem_residue_of_not_inverse h₁.1 h₂.1 hx₁ hx₂ hred

    have hPQ : ¬(x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂) := by
      rintro ⟨hxe, hye⟩
      exact hred ⟨by rw [hxe, sub_self]; exact A.nonunits.zero_mem,
        by rw [hye, sub_self]; exact A.nonunits.zero_mem⟩

    have hredk : ¬(residue A ⟨x₁, hx₁⟩ = residue A ⟨x₂, hx₂⟩ ∧
        residue A ⟨y₁, hy₁⟩ =
          (W.map (residue A)).toAffine.negY (residue A ⟨x₂, hx₂⟩) (residue A ⟨y₂, hy₂⟩)) :=
      fun h => hred ((residue_inverse_iff hx₁ hy₁ hx₂ hy₂).mp h)
    rw [Affine.Point.add_some hPQ, Affine.Point.add_some hredk]

    have hX_coe : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) =
        ((W.toAffine.addX ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩
          ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ : A) : L) :=
      Affine.map_addX (W' := W) A.subtype (⟨x₁, hx₁⟩ : A) (⟨x₂, hx₂⟩ : A)
        ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩
    have hY_coe : (W.map A.subtype).toAffine.addY x₁ x₂ y₁
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) =
        ((W.toAffine.addY ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩ ⟨y₁, hy₁⟩
          ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩ : A) : L) :=
      Affine.map_addY (W' := W) A.subtype (⟨x₁, hx₁⟩ : A) (⟨y₁, hy₁⟩ : A) (⟨x₂, hx₂⟩ : A)
        ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩
    have hX_mem : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∈ A := by
      rw [hX_coe]; exact SetLike.coe_mem _
    rw [reducePoint_some_of_mem _ _ hX_mem]
    refine some_congr' ?_ ?_ _ _
    ·
      calc residue A ⟨(W.map A.subtype).toAffine.addX x₁ x₂
              ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂), hX_mem⟩
          = residue A (W.toAffine.addX ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            A.residue_eq_of_coe_eq hX_mem hX_coe
        _ = (W.map (residue A)).toAffine.addX (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
              (residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            (Affine.map_addX (W' := W) (residue A) (⟨x₁, hx₁⟩ : A) (⟨x₂, hx₂⟩ : A)
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩).symm
        _ = _ := by rw [hsres]
    ·
      calc residue A ⟨(W.map A.subtype).toAffine.addY x₁ x₂ y₁
              ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂),
              Affine.Y_mem_of_X_mem W (Affine.nonsingular_add h₁ h₂ hPQ).1 hX_mem⟩
          = residue A (W.toAffine.addY ⟨x₁, hx₁⟩ ⟨x₂, hx₂⟩ ⟨y₁, hy₁⟩
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            A.residue_eq_of_coe_eq _ hY_coe
        _ = (W.map (residue A)).toAffine.addY (residue A ⟨x₁, hx₁⟩) (residue A ⟨x₂, hx₂⟩)
              (residue A ⟨y₁, hy₁⟩)
              (residue A ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩) :=
            (Affine.map_addY (W' := W) (residue A) (⟨x₁, hx₁⟩ : A) (⟨y₁, hy₁⟩ : A)
              (⟨x₂, hx₂⟩ : A)
              ⟨(W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂, hsmem⟩).symm
        _ = _ := by rw [hsres]

end IntegralCase

section KernelCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_of_notMem_of_notMem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∉ A) (hx₂ : x₂ ∉ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by

  rw [reducePoint_some_of_notMem _ _ hx₁, reducePoint_some_of_notMem _ _ hx₂, add_zero]
  by_cases hPQ : x₁ = x₂ ∧ y₁ = (W.map A.subtype).toAffine.negY x₂ y₂
  · rw [Affine.Point.add_of_Y_eq hPQ.1 hPQ.2, reducePoint_zero]
  ·

    have hy₁0 : y₁ ≠ 0 := Affine.Y_ne_zero_of_X_notMem W h₁.1 hx₁
    have hy₂0 : y₂ ≠ 0 := Affine.Y_ne_zero_of_X_notMem W h₂.1 hx₂
    have hx₁0 : x₁ ≠ 0 := fun h => hx₁ (h ▸ A.zero_mem)
    have hx₂0 : x₂ ≠ 0 := fun h => hx₂ (h ▸ A.zero_mem)
    have ht₁m : x₁ / y₁ ∈ A.nonunits := Affine.X_div_Y_mem_nonunits W h₁.1 hx₁
    have ht₂m : x₂ / y₂ ∈ A.nonunits := Affine.X_div_Y_mem_nonunits W h₂.1 hx₂
    have ht₁0 : x₁ / y₁ ≠ 0 := div_ne_zero hx₁0 hy₁0
    have ht₂0 : x₂ / y₂ ≠ 0 := div_ne_zero hx₂0 hy₂0
    have haddX : (W.map A.subtype).toAffine.addX x₁ x₂
        ((W.map A.subtype).toAffine.slope x₁ x₂ y₁ y₂) ∉ A := by
      rcases A.mem_or_inv_mem ((x₁ / y₁) / (x₂ / y₂)) with hcase | hcase
      ·
        refine (Affine.add_formal_param_estimate h₁.1 h₂.1 hx₁ hx₂ hPQ ht₂m ht₂0 hcase ?_).1
        rw [div_self ht₂0]
        exact A.one_mem
      ·
        rw [show ((x₁ / y₁) / (x₂ / y₂))⁻¹ = (x₂ / y₂) / (x₁ / y₁) by rw [inv_div]] at hcase
        refine (Affine.add_formal_param_estimate h₁.1 h₂.1 hx₁ hx₂ hPQ ht₁m ht₁0 ?_ hcase).1
        rw [div_self ht₁0]
        exact A.one_mem
    rw [Affine.Point.add_some hPQ]
    exact reducePoint_some_of_notMem _ _ haddX

end KernelCase

section MixedCase

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_of_mem_of_notMem {x₁ y₁ x₂ y₂ : L}
    (h₁ : (W.map A.subtype).toAffine.Nonsingular x₁ y₁)
    (h₂ : (W.map A.subtype).toAffine.Nonsingular x₂ y₂) (hx₁ : x₁ ∈ A) (hx₂ : x₂ ∉ A) :
    reducePoint hΔ (.some x₁ y₁ h₁ + .some x₂ y₂ h₂) =
      reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (.some x₂ y₂ h₂) := by

  rw [reducePoint_some_of_notMem _ _ hx₂, add_zero]

  have hPn : (W.map A.subtype).toAffine.Nonsingular x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) :=
    (Affine.nonsingular_neg _ _).mpr h₁
  have hQn : (W.map A.subtype).toAffine.Nonsingular x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) :=
    (Affine.nonsingular_neg _ _).mpr h₂
  have hPneg : (.some x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) hPn :
      (W.map A.subtype).toAffine.Point) = -(.some x₁ y₁ h₁) := (Affine.Point.neg_some h₁).symm
  have hQneg : (.some x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) hQn :
      (W.map A.subtype).toAffine.Point) = -(.some x₂ y₂ h₂) := (Affine.Point.neg_some h₂).symm

  cases hadd : (.some x₁ y₁ h₁ + .some x₂ y₂ h₂ : (W.map A.subtype).toAffine.Point) with
  | zero =>

    exfalso
    have hP : (.some x₁ y₁ h₁ : (W.map A.subtype).toAffine.Point) = -(.some x₂ y₂ h₂) :=
      eq_neg_of_add_eq_zero_left hadd
    rw [← hQneg] at hP
    simp only [Affine.Point.some.injEq] at hP
    exact hx₂ (hP.1 ▸ hx₁)
  | some X₃ Y₃ h₃ =>
    by_cases hX₃ : X₃ ∈ A
    ·
      have hint := reducePoint_add_of_mem hΔ h₃ hPn hX₃ hx₁
      have hSnegP : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) +
          .some x₁ ((W.map A.subtype).toAffine.negY x₁ y₁) hPn = .some x₂ y₂ h₂ := by
        rw [hPneg, ← hadd]; abel
      rw [hSnegP, reducePoint_some_of_notMem _ _ hx₂, hPneg, reducePoint_neg,
        ← sub_eq_add_neg] at hint
      exact (sub_eq_zero.mp hint.symm)
    ·
      exfalso
      have hker := reducePoint_add_of_notMem_of_notMem hΔ h₃ hQn hX₃ hx₂
      have hSnegQ : (.some X₃ Y₃ h₃ : (W.map A.subtype).toAffine.Point) +
          .some x₂ ((W.map A.subtype).toAffine.negY x₂ y₂) hQn = .some x₁ y₁ h₁ := by
        rw [hQneg, ← hadd]; abel
      rw [hSnegQ, reducePoint_some_of_mem _ _ hx₁, reducePoint_some_of_notMem _ _ hX₃,
        reducePoint_some_of_notMem _ _ hx₂, add_zero] at hker
      injection hker

end MixedCase

section Homomorphism

variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable {W} (hΔ : (W.map (residue A)).Δ ≠ 0)

theorem reducePoint_add_def (P Q : (W.map A.subtype).toAffine.Point) :
    reducePoint hΔ (P + Q) = reducePoint hΔ P + reducePoint hΔ Q := by
  cases P with
  | zero =>
    show reducePoint hΔ ((0 : (W.map A.subtype).toAffine.Point) + Q) =
      reducePoint hΔ (0 : (W.map A.subtype).toAffine.Point) + reducePoint hΔ Q
    rw [zero_add, reducePoint_zero, zero_add]
  | some x₁ y₁ h₁ =>
    cases Q with
    | zero =>
      show reducePoint hΔ (.some x₁ y₁ h₁ + (0 : (W.map A.subtype).toAffine.Point)) =
        reducePoint hΔ (.some x₁ y₁ h₁) + reducePoint hΔ (0 : (W.map A.subtype).toAffine.Point)
      rw [add_zero, reducePoint_zero, add_zero]
    | some x₂ y₂ h₂ =>
      by_cases hx₁ : x₁ ∈ A <;> by_cases hx₂ : x₂ ∈ A
      · exact reducePoint_add_of_mem hΔ h₁ h₂ hx₁ hx₂
      · exact reducePoint_add_of_mem_of_notMem hΔ h₁ h₂ hx₁ hx₂
      · rw [add_comm, add_comm (reducePoint hΔ (.some x₁ y₁ h₁))]
        exact reducePoint_add_of_mem_of_notMem hΔ h₂ h₁ hx₂ hx₁
      · exact reducePoint_add_of_notMem_of_notMem hΔ h₁ h₂ hx₁ hx₂

noncomputable def reduceHom :
    (W.map A.subtype).toAffine.Point →+ (W.map (residue A)).toAffine.Point where
  toFun := reducePoint hΔ
  map_zero' := reducePoint_zero hΔ
  map_add' := reducePoint_add_def hΔ

end Homomorphism

end WeierstrassCurve