import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.nat
import Goppadecoding.zero
import Goppadecoding.sq
import Goppadecoding.poly
import Goppadecoding.shiftpoly
import Goppadecoding.vanishing
import Goppadecoding.goppa_binary
import Goppadecoding.goppa_parity

open Polynomial BigOperators Finset

namespace Goppadecoding

section goppa_closer

variable {U: Type _} [DecidableEq U]
variable {k: Type _} [Field k] [CharP k 2] [DecidableEq k]

theorem goppa_checking_2_lemma_coeff
  {α r d: U → k} {S: Finset U} {g f: k[X]} {t: ℕ}
  (fdeg: f.degree < ((2*t:ℕ):WithBot ℕ))
: coeff (f*∑ s in S, ∑ j in range (2*t), C ((r s / (g^2).eval (α s)) * (d s)^j) * X^(2*t-1-j)) (2*t-1) = ∑ s in S, (r s / (g^2).eval (α s)) * f.eval (d s) :=
by
  rw[coeff_mul_sum_sum_geom fdeg]

theorem goppa_checking_2_lemma_WfEhb
  {α: U → k} (z: U) {b E F W h f: k[X]} {t21: ℕ}
  {bar: k[X] → k[X]}
  (bardef: bar = shiftpoly k (α z))
  (Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]))
: coeff W t21 = coeff (f*E:k[X]) t21 - (h*b:k[X]).eval (α z) :=
by calc
  _ = coeff ((f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X])) t21 := by rw[Wdef]
  _ = coeff (f*E:k[X]) t21 - coeff ((X:k[X])^t21*bar (h*b:k[X]):k[X]) t21 - coeff ((X:k[X])^(t21+1)*(F*f):k[X]) t21 := by repeat rw[coeff_sub]
  _ = coeff (f*E:k[X]) t21 - (bar (h*b:k[X])).eval (0:k) - 0 := by rw[coeff_X_pow_eq_eval_zero,coeff_X_pow_add_one_eq_zero]
  _ = coeff (f*E:k[X]) t21 - (h*b:k[X]).eval (0 + α z) - 0 := by rw[bardef,shiftpoly_eval]
  _ = coeff (f*E:k[X]) t21 - (h*b:k[X]).eval (α z) := by group

theorem goppa_checking_2_lemma_hbfE
  {α: U → k} (z: U) {b E F W h f: k[X]} {t21: ℕ}
  {bar: k[X] → k[X]}
  (bardef: bar = shiftpoly k (α z))
  (Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]))
  (Wdeg: W.degree < (t21:WithBot ℕ))
: (h*b:k[X]).eval (α z) = coeff (f*E:k[X]) t21 :=
by
  have W0: coeff W t21 = 0 := coeff_eq_zero_of_degree_lt Wdeg
  rw[goppa_checking_2_lemma_WfEhb z bardef Wdef] at W0
  exact (eq_if_sub_zero W0).symm

theorem goppa_checking_2_lemma_hbsum
  {α r d: U → k} {S: Finset U} (z: U) {A b D E F W h f q: k[X]} {t t21: ℕ}
  (Adef: A = monic_vanishing_at α S)
  {bar: k[X] → k[X]}
  (t2t1: 2*t-1 = t21)
  (bardef: bar = shiftpoly k (α z))
  (ddef: ∀ s, d s = α s - α z)
  (Ddef: D = bar A)
  (fdef: f = bar (h*q:k[X]))
  (fdeg: f.degree < ((2*t:ℕ):WithBot ℕ))
  (Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ))
  (Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]))
  (DWdeg: (D*W).degree < (t21:WithBot ℕ) + (S.card:WithBot ℕ))
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  have bar_degree (p: k[X]): (bar p:k[X]).degree = p.degree := by
    repeat rw[bardef]; apply shiftpoly_degree
  have dsaz s: d s + α z = α s := by rw[ddef]; group
  have Ddeg: D.degree = S.card := by calc
    _ = (monic_vanishing_at α S).degree := by rw[Ddef,bar_degree,Adef]
    _ = _ := degree_monic_vanishing_at α S
  have DWdeg2: W.degree + S.card < (t21:WithBot ℕ) + S.card := by calc
    _ = W.degree + D.degree := by rw[Ddeg]
    _ = (W*D).degree := by rw[degree_mul]
    _ = (D*W).degree := by rw[mul_comm]
    _ < _ := DWdeg
  have Wdeg: W.degree < (t21:WithBot ℕ) := lt_of_add_lt_add_right DWdeg2
  rw[goppa_checking_2_lemma_hbfE z bardef Wdef Wdeg]
  rw[← t2t1,Edef,goppa_checking_2_lemma_coeff fdeg]
  rw[fdef,bardef]
  simp only [shiftpoly_eval,dsaz]

theorem goppa_checking_2_lemma_DWdeg
  {α: U → k} {S: Finset U} (z: U) {A B a b D R Q E F W h f q: k[X]} {t t21: ℕ}
  {bar: k[X] → k[X]}
  (tt1: ((t-1)+t:ℕ) = t21)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (bardef: bar = shiftpoly k (α z))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (Ddef: D = bar A)
  (XRQ: (X:k[X])^(t21+1)*R - Q = (D*E:k[X]))
  (RBDF: R - bar B = (D*F:k[X]))
  (fdef: f = bar (h*q:k[X]))
  (Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]))
  (hdeg: h.degree ≤ (t:WithBot ℕ))
  (Qdeg: Q.degree < (S.card:WithBot ℕ))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
: (D*W).degree < (t21:WithBot ℕ) + (S.card:WithBot ℕ) :=
by
  have bar_sub (p q: k[X]): bar (p-q:k[X]) = bar p - bar q := by
    repeat rw[bardef]; apply shiftpoly_sub
  have bar_mul (p q: k[X]): bar (p*q:k[X]) = bar p * bar q := by
    repeat rw[bardef]; apply shiftpoly_mul
  have bar_X_sub_C (c: k): bar ((X:k[X]) - C c:k[X]) = (X:k[X]) - C (c - α z) := by
    repeat rw[bardef]; apply shiftpoly_X_sub_C
  have bar_degree (p: k[X]): (bar p:k[X]).degree = p.degree := by
    repeat rw[bardef]; apply shiftpoly_degree
  have Xt21: ((X:k[X])^t21*(X:k[X]):k[X]) = ((X:k[X])^(t21+1):k[X]) := by calc
    _ = ((X:k[X])^t21*(X:k[X])^1:k[X]) := by rw[pow_one]
    _ = ((X:k[X])^(t21+1):k[X]) := by rw[pow_add]
  have aBbAdeg2: ((t:WithBot ℕ) + ((a*B:k[X])-(b*A:k[X]):k[X]).degree) + (t:WithBot ℕ) < (S.card:WithBot ℕ) + (t:WithBot ℕ) := by calc
    _ = 2*(t:WithBot ℕ) + ((a*B:k[X])-(b*A:k[X]):k[X]).degree := by group
    _ < (S.card:WithBot ℕ) + a.degree := aBbAdeg
    _ ≤ (S.card:WithBot ℕ) + (t:WithBot ℕ) := add_le_add_left adeg S.card
  have aBbAdeg3: (t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) := lt_of_add_lt_add_right aBbAdeg2
  have haBbAdeg: (h*(a*B-b*A:k[X]):k[X]).degree < (S.card:WithBot ℕ) := by calc
    _ = h.degree + (a*B-b*A:k[X]).degree := degree_mul
    _ ≤ (t:WithBot ℕ) + (a*B-b*A:k[X]).degree := add_le_add_right hdeg (a*B-b*A:k[X]).degree
    _ < (S.card:WithBot ℕ) := aBbAdeg3
  have shifthaBbAdeg: (bar (h*(a*B-b*A:k[X])):k[X]).degree < (S.card:WithBot ℕ) := by calc
    _ = (h*(a*B-b*A:k[X]):k[X]).degree := bar_degree (h*(a*B-b*A:k[X]))
    _ < (S.card:WithBot ℕ) := haBbAdeg
  have shifthaBbAdeg2: (bar ((X:k[X]) - C (α z)) * bar B * bar (h*q) - D * bar (h*b):k[X]).degree < (S.card:WithBot ℕ) := by calc
    _ = (bar ((X:k[X]) - C (α z):k[X]) * bar B * bar (h*q) - bar A * bar (h*b:k[X]):k[X]).degree := by rw[Ddef]
    _ = (bar (((X:k[X]) - C (α z):k[X]) * B * (h*q:k[X]):k[X]) - bar (A*(h*b:k[X])):k[X]).degree := by repeat rw[bar_mul]
    _ = (bar ((((X:k[X]) - C (α z):k[X]) * B * (h*q:k[X]):k[X]) - (A*(h*b:k[X]):k[X]):k[X]):k[X]).degree := by repeat rw[bar_sub]
    _ = (bar (h * ((q*((X:k[X]) - C (α z):k[X])*B:k[X]) - (b*A:k[X]))):k[X]).degree := by ring_nf
    _ = (bar (h * (a*B - b*A:k[X]):k[X]):k[X]).degree := by rw[aq]
    _ < (S.card:WithBot ℕ) := shifthaBbAdeg
  have shifthaBbAdeg3: (X^(t21) * (bar ((X:k[X]) - C (α z):k[X]) * bar B * bar (h*q:k[X]) - D * bar (h*b:k[X])):k[X]).degree < (t21 + S.card:WithBot ℕ) := by calc
    _ = (X^(t21):k[X]).degree + (bar ((X:k[X]) - C (α z):k[X]) * bar B * bar (h*q:k[X]) - D * bar (h*b:k[X]):k[X]).degree := degree_mul
    _ = (t21) + (bar ((X:k[X]) - C (α z):k[X]) * bar B * bar (h*q:k[X]) - D * bar (h*b:k[X]):k[X]).degree := by rw[degree_X_pow]
    _ < (t21:WithBot ℕ) + (S.card:WithBot ℕ) := add_left_nat_lt_if_lt t21 shifthaBbAdeg2
  have Qfdeg: (Q*bar (h*q):k[X]).degree < (t21:WithBot ℕ) + (S.card:WithBot ℕ) := by calc
    _ = Q.degree + (bar (h*q:k[X]):k[X]).degree := degree_mul
    _ = Q.degree + (h*q:k[X]).degree := by rw[bar_degree]
    _ = Q.degree + (h.degree + q.degree:WithBot ℕ) := by rw[degree_mul]
    _ = h.degree + (q.degree + Q.degree:WithBot ℕ) := by group
    _ ≤ (t:WithBot ℕ) + (q.degree + Q.degree:WithBot ℕ) := add_le_add_right hdeg (q.degree + Q.degree)
    _ = q.degree + (Q.degree + (t:WithBot ℕ)) := by group
    _ ≤ ((t-1:ℕ):WithBot ℕ) + (Q.degree + (t:WithBot ℕ)) := add_le_add_right qdeg (Q.degree + (t:WithBot ℕ))
    _ = (((t-1:ℕ):WithBot ℕ) + t:WithBot ℕ) + Q.degree := by group
    _ = (((t-1:ℕ) + t:ℕ):WithBot ℕ) + Q.degree := by norm_cast
    _ = (t21:WithBot ℕ) + Q.degree := by rw[tt1]
    _ < (t21:WithBot ℕ) + (S.card:WithBot ℕ) := add_left_nat_lt_if_lt t21 Qdeg
  calc
    _ = (D*((f*E:k[X]) - ((X:k[X])^(t21)*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]):k[X]):k[X]).degree := by rw[Wdef]
    _ = ((D*E:k[X])*f - ((X:k[X])^(t21)*D*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(D*F)*f:k[X]):k[X]).degree := by ring_nf
    _ = (((X:k[X])^t21*(X:k[X])*R-Q:k[X])*bar (h*q:k[X]) - ((X:k[X])^(t21)*D*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21)*(X:k[X]) * (R-bar B) * bar (h*q):k[X]):k[X]).degree := by rw[← RBDF,← XRQ,Xt21,fdef]
    _ = ((X:k[X])^(t21) * ((((X:k[X]) - (C (α z) - C (α z)):k[X]) * bar B * bar (h*q:k[X]):k[X]) - (D * bar (h*b:k[X]):k[X]):k[X]) - Q*bar (h*q:k[X]):k[X]).degree := by ring_nf
    _ = ((X:k[X])^(t21) * (((X:k[X]) - (C (α z - α z))) * bar B * bar (h*q:k[X]) - (D * bar (h*b:k[X]):k[X]):k[X]) - Q*bar (h*q:k[X]):k[X]).degree := by rw[C_sub]
    _ = ((X:k[X])^(t21) * (bar ((X:k[X]) - C (α z)) * bar B * bar (h*q:k[X]) - (D * bar (h*b:k[X]):k[X]):k[X]) - Q*bar (h*q:k[X]):k[X]).degree := by rw[bar_X_sub_C]
    _ ≤ max ((X:k[X])^(t21) * (bar ((X:k[X]) - C (α z):k[X]) * bar B * bar (h*q:k[X]) - D * bar (h*b:k[X])):k[X]).degree (Q*bar (h*q:k[X]):k[X]).degree := degree_sub_le (X^(t21) * (bar (X - C (α z):k[X]) * bar B * bar (h*q:k[X]) - D * bar (h*b:k[X]):k[X])) (Q*bar (h*q:k[X]))
    _ < (t21:WithBot ℕ) + (S.card:WithBot ℕ) := max_lt shifthaBbAdeg3 Qfdeg

theorem goppa_checking_2_lemma_hbsum2
  {α r d: U → k} {S: Finset U} (z: U) {A B a b D R Q E F W h f q: k[X]} {t t21: ℕ}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (Adef: A = monic_vanishing_at α S)
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  {bar: k[X] → k[X]}
  (bardef: bar = shiftpoly k (α z))
  (ddef: ∀ s, d s = α s - α z)
  (Ddef: D = bar A)
  (fdef: f = bar (h*q:k[X]))
  (fdeg: f.degree < ((2*t:ℕ):WithBot ℕ))
  (Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ))
  (XRQ: (X:k[X])^(t21+1)*R - Q = (D*E:k[X]))
  (RBDF: R - bar B = (D*F:k[X]))
  (Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]))
  (hdeg: h.degree ≤ (t:WithBot ℕ))
  (Qdeg: Q.degree < (S.card:WithBot ℕ))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  have DWdeg: (D*W).degree < (t21:WithBot ℕ) + (S.card:WithBot ℕ) :=
    goppa_checking_2_lemma_DWdeg z tt1 adeg bardef aBbAdeg aq Ddef XRQ RBDF fdef Wdef hdeg Qdeg qdeg
  exact goppa_checking_2_lemma_hbsum z Adef t2t1 bardef ddef Ddef fdef fdeg Edef Wdef DWdeg

theorem goppa_checking_2_lemma_hbsum3
  {α r d: U → k} {S: Finset U} (z: U) {A B a b g D R Q E F h q: k[X]} {t t21: ℕ}
  {bar: k[X] → k[X]}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t1t: t-1 < t)
  (Adef: A = monic_vanishing_at α S)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (bardef: bar = shiftpoly k (α z))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (ddef: ∀ s, d s = α s - α z)
  (Ddef: D = bar A)
  (Qdeg: Q.degree < (S.card:WithBot ℕ))
  (Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ))
  (XRQ: (X^(t21+1:ℕ)*R - Q:k[X]) = (D*E:k[X]))
  (RBDF: (R - bar B:k[X]) = (D*F:k[X]))
  (hdeg: h.degree ≤ t)
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  let f := bar (h*q:k[X])
  let W := (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X])
  have fdef: f = bar (h*q:k[X]) := rfl
  have Wdef: W = (f*E:k[X]) - ((X:k[X])^t21*bar (h*b:k[X]):k[X]) - ((X:k[X])^(t21+1)*(F*f):k[X]) := rfl
  have qdegt: q.degree < t := by calc
    _ ≤ ((t-1:ℕ):WithBot ℕ) := qdeg
    _ < t := by norm_cast
  have fdeg: f.degree < (2*t:ℕ) := by calc
    _ = (shiftpoly k (α z) (h*q)).degree := by rw[fdef,bardef]
    _ = (h*q).degree := by rw[shiftpoly_degree]
    _ = h.degree + q.degree := degree_mul
    _ ≤ t + q.degree := add_le_add_right hdeg q.degree
    _ < ((t + t):WithBot ℕ) := add_left_nat_lt_if_lt t qdegt
    _ = ((t + t:ℕ):WithBot ℕ) := by norm_cast
    _ = ((2*t:ℕ):WithBot ℕ) := by norm_cast; exact (Nat.two_mul t).symm
  exact goppa_checking_2_lemma_hbsum2 z tt1 t2t1 Adef aBbAdeg adeg aq bardef ddef Ddef fdef fdeg Edef XRQ RBDF Wdef hdeg Qdeg qdeg

theorem goppa_checking_2_lemma_RBD
  {α r d: U → k} {S: Finset U} (z: U) {A B g D R: k[X]}
  {bar: k[X] → k[X]}
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (ddef: ∀ s, d s = α s - α z)
  (dinjective: Set.InjOn d S)
  (bardef: bar = shiftpoly k (α z))
  (Ddef: D = bar A)
  (Dmv: D = monic_vanishing_at d S)
  (Rdef: R = ∑ s in S, C (r s / (g^2:k[X]).eval (α s)) * monic_vanishing_at_except d S s)
: D ∣ R - bar B :=
by
  have dsaz s: d s + α z = α s := by rw[ddef]; group
  have bar_eval (c: k) (p: k[X]): (bar p).eval c = p.eval (c + α z) := by
    repeat rw[bardef]; apply shiftpoly_eval
  have bar_diff (p: k[X]): (bar p).diff = bar p.diff := by
    repeat rw[bardef]; apply shiftpoly_diff
  have Ddiffeval s: D.diff.eval (d s) = A.diff.eval (α s) := by calc
    _ = D.diff.eval (d s) := rfl
    _ = (bar A.diff).eval (d s) := by rw[Ddef,bar_diff]
    _ = A.diff.eval (d s + α z) := by rw[bar_eval]
    _ = A.diff.eval (α s) := by rw[dsaz s]
  have Rinterp: R = interpolator d S (fun s ↦ r s / (g^2).eval (α s) * D.diff.eval (d s)) := by
    rw[Rdef]
    exact sum_C_mul_monic_vanishing_at_except_eq_interpolator (fun s ↦ r s / (g^2).eval (α s)) dinjective Dmv
  have Reval s (sinS: s ∈ S): R.eval (d s) = B.eval (α s) := by calc
    _ = (interpolator d S (fun s ↦ r s / (g^2).eval (α s) * D.diff.eval (d s))).eval (d s) := by rw[Rinterp]
    _ = r s / (g^2).eval (α s) * D.diff.eval (d s) := by rw[interpolator_eval dinjective sinS]
    _ = r s / (g^2).eval (α s) * A.diff.eval (α s) := by rw[Ddiffeval s]
    _ = ((g^2 * B).eval (α s) / A.diff.eval (α s)) / (g^2).eval (α s) * A.diff.eval (α s) := by rw[rdef s sinS]
    _ = ((g^2).eval (α s) * B.eval (α s) / A.diff.eval (α s)) / (g^2).eval (α s) * A.diff.eval (α s) := by rw[eval_mul]
    _ = B.eval (α s) * ((g^2).eval (α s) / (g^2).eval (α s)) * (A.diff.eval (α s) / A.diff.eval (α s)) := by group
    _ = B.eval (α s) * 1 * 1 := by rw[div_self (Aprimeevalnonzero s sinS),div_self (g2nonzero s sinS)]
    _ = B.eval (α s) := by repeat rw[mul_one]
  have RBbareval s (sinS: s ∈ S): (R - bar B).eval (d s) = 0 := by calc
    _ = R.eval (d s) - (bar B).eval (d s) := by rw[eval_sub]
    _ = R.eval (d s) - B.eval (d s + α z) := by rw[bar_eval]
    _ = R.eval (d s) - B.eval (α s) := by rw[dsaz s]
    _ = B.eval (α s) - B.eval (α s) := by rw[Reval s sinS]
    _ = 0 := by rw[sub_self]
  rw[Dmv]
  exact monic_vanishing_at_divides S (R - bar B) dinjective RBbareval

theorem goppa_checking_2_lemma_hbsum4
  {α r d: U → k} {S: Finset U} (z: U) {A B a b g D R h q: k[X]} {t t21: ℕ}
  {bar: k[X] → k[X]}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (ddef: ∀ s, d s = α s - α z)
  (dinjective: Set.InjOn d S)
  (bardef: bar = shiftpoly k (α z))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (Ddef: D = bar A)
  (Dmv: D = monic_vanishing_at d S)
  (hdeg: h.degree ≤ t)
  (Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ))
  (Rdef: R = ∑ s in S, C (r s / (g^2).eval (α s)) * monic_vanishing_at_except d S s)
  (Qdef: Q = ∑ s in S, C ((r s / (g^2).eval (α s)) * (d s)^(2*t)) * monic_vanishing_at_except d S s)
  (Qdeg: Q.degree < (S.card:WithBot ℕ))
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  have RBD: D ∣ R - bar B := goppa_checking_2_lemma_RBD z Aprimeevalnonzero g2nonzero rdef ddef dinjective bardef Ddef Dmv Rdef
  cases RBD with | intro F RBDF =>
  have XRQ: (X^(t21+1:ℕ)*R - Q:k[X]) = (D*E:k[X]) := by
    rw[t211,Rdef,Qdef,Edef,Dmv]
    exact goppa_parity_lemma d (fun s ↦ r s / (g^2).eval (α s)) S (2*t)
  exact goppa_checking_2_lemma_hbsum3 z tt1 t2t1 t1t Adef adeg aBbAdeg bardef qdeg aq ddef Ddef Qdeg Edef XRQ RBDF hdeg

theorem goppa_checking_2_lemma_hbsum5
  {α r d: U → k} {S: Finset U} (z: U) {A B a b g D R h q: k[X]} {t t21: ℕ}
  {bar: k[X] → k[X]}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (ddef: ∀ s, d s = α s - α z)
  (dinjective: Set.InjOn d S)
  (bardef: bar = shiftpoly k (α z))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (Ddef: D = bar A)
  (Dmv: D = monic_vanishing_at d S)
  (hdeg: h.degree ≤ t)
  (Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ))
  (Rdef: R = ∑ s in S, C (r s / (g^2).eval (α s)) * monic_vanishing_at_except d S s)
  (Qdef: Q = ∑ s in S, C ((r s / (g^2).eval (α s)) * (d s)^(2*t)) * monic_vanishing_at_except d S s)
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  have Qinterp: Q = interpolator d S (fun (s:U) ↦ (((r s / (g^2).eval (α s)) * (d s)^(2*t) * D.diff.eval (d s)):k)) := by
    rw[Qdef]
    exact sum_C_mul_monic_vanishing_at_except_eq_interpolator (fun (s:U) ↦ (((r s / (g^2).eval (α s)) * (d s)^(2*t)):k)) dinjective Dmv
  have Qdeg: Q.degree < S.card := by
    rw[Qinterp]
    apply degree_interpolator_lt
  exact goppa_checking_2_lemma_hbsum4 z tt1 t2t1 t211 t1t Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg ddef dinjective bardef qdeg aq Ddef Dmv hdeg Edef Rdef Qdef Qdeg

theorem goppa_checking_2_lemma_hbsum6
  {α r d: U → k} {S: Finset U} (z: U) {A B a b g D h q: k[X]} {t t21: ℕ}
  {bar: k[X] → k[X]}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (ddef: ∀ s, d s = α s - α z)
  (dinjective: Set.InjOn d S)
  (bardef: bar = shiftpoly k (α z))
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (Ddef: D = bar A)
  (Dmv: D = monic_vanishing_at d S)
  (hdeg: h.degree ≤ t)
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  let E := ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ)
  have Edef: E = ∑ s in S, ∑ j in range (2*t), C ((r s / (g^2:k[X]).eval (α s)) * (d s)^j) * (X:k[X])^(2*t-1-j:ℕ) := rfl
  let R := ∑ s in S, C (r s / (g^2).eval (α s)) * monic_vanishing_at_except d S s
  have Rdef: R = ∑ s in S, C (r s / (g^2).eval (α s)) * monic_vanishing_at_except d S s := rfl
  let Q := ∑ s in S, C ((r s / (g^2).eval (α s)) * (d s)^(2*t)) * monic_vanishing_at_except d S s
  have Qdef: Q = ∑ s in S, C ((r s / (g^2).eval (α s)) * (d s)^(2*t)) * monic_vanishing_at_except d S s := rfl
  exact goppa_checking_2_lemma_hbsum5 z tt1 t2t1 t211 t1t Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg ddef dinjective bardef qdeg aq Ddef Dmv hdeg Edef Rdef Qdef

theorem goppa_checking_2_lemma_hbsum7
  {α r d: U → k} {S: Finset U} (z: U) {A B a b g h q: k[X]} {t t21: ℕ}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (ddef: ∀ s, d s = α s - α z)
  (dinjective: Set.InjOn d S)
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (hdeg: h.degree ≤ t)
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  let bar := shiftpoly k (α z)
  have bardef: bar = shiftpoly k (α z) := rfl
  have bar_X_sub_C (c: k): bar ((X:k[X]) - C c:k[X]) = (X:k[X]) - C (c - α z) := by
    repeat rw[bardef]; apply shiftpoly_X_sub_C
  have bar_prod {p: U → k[X]}: bar (∏ s in S, p s) = ∏ s in S, bar (p s) := by
    repeat rw[bardef]; apply shiftpoly_prod
  let D := bar A
  have Ddef: D = bar A := rfl
  have Dmv: D = monic_vanishing_at d S := by calc
    _ = bar A := rfl
    _ = bar (monic_vanishing_at α S) := by rw[Adef]
    _ = bar (∏ s in S, (X - C (α s))) := by rw[monic_vanishing_at]
    _ = ∏ s in S, bar (X - C (α s)) := by rw[bar_prod]
    _ = ∏ s in S, (X - C (d s)) := by
          apply prod_congr; simp only
          intro s _
          rw[bar_X_sub_C,ddef s]
    _ = monic_vanishing_at d S := by rw[monic_vanishing_at]
  exact goppa_checking_2_lemma_hbsum6 z tt1 t2t1 t211 t1t Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg ddef dinjective bardef qdeg aq Ddef Dmv hdeg

theorem goppa_checking_2_lemma_hbsum8
  {α r: U → k} {S: Finset U} (z: U) {A B a b g h q: k[X]} {t t21: ℕ}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef : ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (hdeg: h.degree ≤ t)
: (h*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (h*q).eval (α s) :=
by
  let d := fun s ↦ α s - α z
  have ddef s: d s = α s - α z := rfl
  have dinjective: Set.InjOn d S := by
    rw[Set.InjOn]
    intro x xinS y yinS dxdy
    have axay: α x = α y := by calc
      α x = (α x - α z) + α z := eq_add_of_sub_eq rfl
      _ = (α y - α z) + α z := by rw[← ddef x,← ddef y,dxdy]
      _ = α y := (eq_add_of_sub_eq rfl).symm
    exact injective xinS yinS axay
  exact goppa_checking_2_lemma_hbsum7 z tt1 t2t1 t211 t1t Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg ddef dinjective qdeg aq hdeg

theorem goppa_checking_2_lemma_gb2qb
  {α r: U → k} {S: Finset U} (z: U) {A B a b g q: k[X]} {t t21: ℕ}
  (tt1: ((t-1)+t:ℕ) = t21)
  (t2t1: 2*t-1 = t21)
  (t211: t21+1 = 2*t)
  (t1t: t-1 < t)
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ))
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (gdeg: g.degree ≤ t)
: ((g*b).eval (α z))^2 = (q*b).eval (α z) :=
by
  have qdegt: q.degree ≤ t := by calc
    _ ≤ ((t-1:ℕ):WithBot ℕ) := qdeg
    _ ≤ t := by norm_cast; exact Nat.sub_le t 1
  have gb: (g*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (g*q).eval (α s) :=
    goppa_checking_2_lemma_hbsum8 z tt1 t2t1 t211 t1t injective Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg qdeg aq gdeg
  have qb: (q*b).eval (α z) = ∑ s in S, r s / (g^2:k[X]).eval (α s) * (q*q).eval (α s) :=
    goppa_checking_2_lemma_hbsum8 z tt1 t2t1 t211 t1t injective Adef Aprimeevalnonzero g2nonzero rdef adeg aBbAdeg qdeg aq qdegt
  have rg2gq s: r s / (g^2:k[X]).eval (α s) * (g*q).eval (α s) = r s / g.eval (α s) * q.eval (α s) := by
    rw[eval_pow,eval_mul]
    rw[div_sq_mul_mul (r s) (g.eval (α s)) (q.eval (α s))]
  have sumrg2gq: ∑ s in S, r s / (g^2:k[X]).eval (α s) * (g*q).eval (α s) = ∑ s in S, r s / g.eval (α s) * q.eval (α s) := by
    apply sum_congr; rfl; intro s _; rw[rg2gq s]
  calc
    _ = (∑ s in S, r s / (g^2:k[X]).eval (α s) * (g*q).eval (α s))^2 := by rw[gb]
    _ = (∑ s in S, r s / g.eval (α s) * q.eval (α s))^2 := by rw[sumrg2gq]
    _ = ∑ s in S, (r s / g.eval (α s) * q.eval (α s))^2 := by rw[CharTwo.sum_sq]
    _ = ∑ s in S, (r s / g.eval (α s))^2 * (q.eval (α s))^2 := by simp[mul_sq]
    _ = ∑ s in S, (r s)^2 / (g.eval (α s))^2 * (q.eval (α s))^2 := by simp[div_sq]
    _ = ∑ s in S, r s / (g.eval (α s))^2 * (q.eval (α s))^2 := by simp[rsq]
    _ = ∑ s in S, r s / ((g^2:k[X]).eval (α s)) * (q^2).eval (α s) := by simp[eval_pow]
    _ = ∑ s in S, r s / ((g^2:k[X]).eval (α s)) * (q*q).eval (α s) := by rw[← sq]
    _ = (q*b).eval (α z) := by rw[qb]

theorem goppa_checking_2_lemma_gb2qb2
  {α r: U → k} {S: Finset U} (z: U) {A B a b g q: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (aA : a ∣ A)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (gdeg: g.degree ≤ t)
: ((g*b).eval (α z))^2 = (q*b).eval (α z) :=
by
  have Anonzero: A ≠ 0 := by rw[Adef]; exact monic_vanishing_at_nonzero α S
  have anonzero: a ≠ 0 := nonzero_if_divides_nonzero aA Anonzero
  have qnonzero: q ≠ 0 := by
    by_cases q0: q = 0
    . rw[q0,zero_mul,← not_ne_iff] at aq
      rw[q0]
      simp only [ne_eq, not_true]
      exact aq anonzero
    simp[q0]
  have qdegnat: 0 ≤ q.degree := zero_le_degree_iff.mpr qnonzero
  have adegqdeg: a.degree = q.degree + 1 := by calc
    _ = (q*((X:k[X]) - C (α z):k[X])).degree := by rw[aq]
    _ = q.degree + (X - C (α z)).degree := degree_mul
    _ = q.degree + 1 := by simp
  have qdeg1: q.degree + 1 ≤ t := by rw[← adegqdeg]; exact adeg
  have t1withbot: 1 ≤ (t:WithBot ℕ) := by calc
    _ = (0 + 1:WithBot ℕ) := by rw[zero_add]
    _ ≤ q.degree + 1 := add_le_add_right qdegnat 1
    _ = a.degree := by rw[adegqdeg]
    _ ≤ t := adeg
  have t1: 1 ≤ t := WithBot.coe_le_coe.mp t1withbot
  let t21 := 2*t-1
  have t2t1: 2*t-1 = t21 := rfl
  have t1t: t-1 < t := sub_one_lt_if_one_le t1
  have tt1: ((t-1)+t:ℕ) = t21 := by rw[← t2t1]; exact sub_one_add_eq_dbl_sub_one
  have t211: t21+1 = 2*t := by rw[← t2t1]; exact dbl_sub_one_add_one_eq_dbl_if_one_le t1
  have qdeg: q.degree ≤ ((t-1:ℕ):WithBot ℕ) := le_sub_one_if_one_le_and_add_one_le t1 qdeg1
  exact goppa_checking_2_lemma_gb2qb z tt1 t2t1 t211 t1t injective Adef Aprimeevalnonzero g2nonzero rdef rsq adeg aBbAdeg qdeg aq gdeg

theorem goppa_checking_2_lemma_gb2qb3
  {α r: U → k} {S: Finset U} (z: U) {A B a b g q: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (ab: IsCoprime a b)
  (aA : a ∣ A)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (zroot: a.eval (α z) = 0)
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (gdeg: g.degree ≤ t)
: (g^2*b - q).eval (α z) = 0 :=
by
  have h: ((g*b).eval (α z))^2 = (q*b).eval (α z) :=
    goppa_checking_2_lemma_gb2qb2 z injective Adef Aprimeevalnonzero g2nonzero rdef rsq aA adeg aBbAdeg aq gdeg
  have h2: (g^2*b - q).eval (α z) * b.eval (α z) = 0 := by calc
    _ = ((g^2*b - q)*b).eval (α z) := by rw[eval_mul]
    _ = ((g*b)^2 - q*b).eval (α z) := by ring_nf
    _ = ((g*b)^2).eval (α z) - (q*b).eval (α z) := by rw[eval_sub]
    _ = (g*b).eval (α z)^2 - (q*b).eval (α z) := by rw[eval_pow]
    _ = (q*b).eval (α z) - (q*b).eval (α z) := by rw[h]
    _ = 0 := by group
  have beval: b.eval (α z) ≠ 0 := no_shared_root_if_coprime ab zroot
  exact zero_if_mul_right_zero beval h2

theorem goppa_checking_2_lemma_gb2qb4
  {α r: U → k} {S: Finset U} (z: U) {A B a b g q: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (ab: IsCoprime a b)
  (aA : a ∣ A)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (zroot: a.eval (α z) = 0)
  (aq: a = q*((X:k[X]) - C (α z):k[X]))
  (gdeg: g.degree ≤ t)
: (g^2*b - a.diff).eval (α z) = 0 :=
by
  have adiffq: a.diff = q.diff*(X - C (α z)) + q := by
    rw[aq,diff,AddHom.toFun_eq_coe,LinearMap.coe_toAddHom]
    simp only [derivative_mul, map_sub, derivative_X, derivative_C, sub_zero, mul_one]
  have adiffeval: a.diff.eval (α z) = q.eval (α z) := by calc
    _ = (q.diff*(X - C (α z)) + q).eval (α z) := by rw[adiffq]
    _ = (q.diff*(X - C (α z))).eval (α z) + q.eval (α z) := by simp only [eval_add]
    _ = q.diff.eval (α z) * (X - C (α z)).eval (α z) + q.eval (α z) := by simp only [eval_mul]
    _ = q.diff.eval (α z) * 0 + q.eval (α z) := by simp only [eval_sub,eval_X,eval_C,sub_self]
    _ = q.eval (α z) := by rw[mul_zero,zero_add]
  calc
    _ = (g^2*b).eval (α z) - a.diff.eval (α z) := by rw[eval_sub]
    _ = (g^2*b).eval (α z) - q.eval (α z) := by rw[adiffeval]
    _ = (g^2*b-q).eval (α z) := by rw[eval_sub]
    _ = 0 := goppa_checking_2_lemma_gb2qb3 z injective Adef Aprimeevalnonzero g2nonzero rdef rsq ab aA adeg aBbAdeg zroot aq gdeg

theorem goppa_checking_2_lemma_gb2qb5
  {α r: U → k} {S: Finset U} (z: U) {A B a b g: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (ab: IsCoprime a b)
  (aA : a ∣ A)
  (adeg: a.degree ≤ (t:WithBot ℕ))
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
  (zinSfilter: z ∈ S.filter (fun s ↦ a.eval (α s) = 0))
  (gdeg: g.degree ≤ t)
: (g^2*b - a.diff).eval (α z) = 0 :=
by
  let q := C (leadingCoeff a) * monic_vanishing_at_except α (S.filter (fun s ↦ a.eval (α s) = 0)) z
  have qdef: q = C (leadingCoeff a) * monic_vanishing_at_except α (S.filter (fun s ↦ a.eval (α s) = 0)) z := rfl
  have amv: a ∣ monic_vanishing_at α S := by rw[← Adef]; exact aA
  have acm: a = C a.leadingCoeff * monic_vanishing_at α (S.filter (fun s ↦ a.eval (α s) = 0)) := lead_mul_monic_vanishing_at_roots_if_dvd_monic_vanishing_at injective amv
  have aq: a = q*((X:k[X]) - C (α z):k[X]) := by rw[acm,qdef,mul_assoc,monic_vanishing_at_except_filter α (S.filter (fun s ↦ a.eval (α s) = 0)) z zinSfilter]
  rw[mem_filter] at zinSfilter
  have zroot: a.eval (α z) = 0 := by simp[zinSfilter]
  exact goppa_checking_2_lemma_gb2qb4 z injective Adef Aprimeevalnonzero g2nonzero rdef rsq ab aA adeg aBbAdeg zroot aq gdeg

theorem goppa_checking_2_lemma_adiv
  {α r: U → k} {S: Finset U} {A B a b g: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Aprimeevalnonzero : ∀ s, s ∈ S → eval (α s) (diff A) ≠ 0)
  (g2nonzero : ∀ s, s ∈ S → eval (α s) (g^2) ≠ 0)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (gdeg: g.degree ≤ t)
  (ab: IsCoprime a b)
  (aA: a ∣ A)
  (adeg: a.degree ≤ t)
  (aBbAdeg: 2*(t:WithBot ℕ) + (a*B-b*A:k[X]).degree < (S.card:WithBot ℕ) + a.degree)
: a ∣ g^2*b - a.diff :=
by
  have amv: a ∣ monic_vanishing_at α S := by rw[← Adef]; exact aA
  have acm: a = C a.leadingCoeff * monic_vanishing_at α (S.filter (fun s ↦ a.eval (α s) = 0)) := lead_mul_monic_vanishing_at_roots_if_dvd_monic_vanishing_at injective amv
  have leadnonzero: a.leadingCoeff ≠ 0 := lead_nonzero_if_dvd_monic_vanishing_at amv
  apply dvd_if_mul_C_nonzero_and_dvd acm leadnonzero
  apply monic_vanishing_at_divides
  . apply injon_filter _ _ _ injective
  intro z zinSfilter
  exact goppa_checking_2_lemma_gb2qb5 z injective Adef Aprimeevalnonzero g2nonzero rdef rsq ab aA adeg aBbAdeg zinSfilter gdeg

theorem goppa_checking_2
  {α e r: U → k} {S: Finset U} {A B a b g: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (gdeg: g.degree = t)
  (gA: IsCoprime g A)
  (ab: IsCoprime a b)
  (adeg: a.degree ≤ t)
  (aA: a ∣ A)
  (aBbAdeg: 2*t + (a*B-b*A).degree < S.card + a.degree)
  (rdef: ∀ s, s ∈ S → r s = (g^2*B).eval (α s) / A.diff.eval (α s))
  (rsq: ∀ s, (r s)^2 = r s)
  (ea: (∀ s, s ∈ S → e s = if a.eval (α s) = 0 then 1 else 0))
: (a ∣ g^2*b - a.diff ∧
   hamming_weight e S = a.degree ∧
   g^2 ∣ ∑ s in S, C (((g^2 * B).eval (α s) / A.diff.eval (α s) - e s)) * monic_vanishing_at_except α S s
  ) :=
by
  have gdegle: g.degree ≤ t := by rw[gdeg]
  have Aprimeevalnonzero s (sinS: s ∈ S): A.diff.eval (α s) ≠ 0 := by
    rw[Adef]
    exact derivative_monic_vanishing_at_eval_nonzero α injective sinS
  have g2nonzero s (sinS: s ∈ S): (g^2).eval (α s) ≠ 0 := by
    have Ag: IsCoprime A g := isCoprime_comm.mpr gA
    have Aeval: A.eval (α s) = 0 := by
      rw[Adef]
      exact monic_vanishing_at_vanishes α S sinS                                                                                     
    have gnonzero: g.eval (α s) ≠ 0 := no_shared_root_if_coprime Ag Aeval
    calc
      _ = (g.eval (α s))^2 := by rw[eval_pow]
      _ ≠ 0 := pow_ne_zero 2 gnonzero
  have g2ba: a ∣ g^2*b - a.diff := goppa_checking_2_lemma_adiv injective Adef Aprimeevalnonzero g2nonzero rdef rsq gdegle ab aA adeg aBbAdeg
  constructor
  . exact g2ba
  let G := g^2
  have g2G: g^2 = G := rfl
  rw[g2G]
  have Gba: a ∣ G*b - a.diff := g2ba
  have Gdeg: G.degree = 2*t := by calc
    G.degree = (g^2).degree := rfl
    _ = 2*g.degree := by simp only [degree_pow, nsmul_eq_mul, Nat.cast_ofNat]
    _ = 2*t := by rw[gdeg]
  exact goppa_checking injective Adef Gdeg aA aBbAdeg Gba ea

end goppa_closer