You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inline in Init.Core
Array in Init.Prelude
Bool in Init.Prelude
Fin in Init.Prelude
Nat in Init.Prelude
Option in Init.Prelude
Semiring in Mathlib.Algebra.Ring.Defs
Polynomial in Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFn in Mathlib.Algebra.Polynomial.OfFn
BEq in Init.Prelude
Ring in Mathlib.Algebra.Ring.Defs
LawfulBEq in Init.Core
Subtype in Init.Prelude
Subtype.val in Init.Prelude
Polynomial.C in Mathlib.Algebra.Polynomial.Basic
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
Array.foldl in Init.Data.Array.Basic
Array.zipIdx in Init.Data.Array.Basic
Eq in Init.Prelude
pos in ToMathlib.Control.Comonad.Instances
Array.zipWith in Init.Data.Array.Basic
Array.rightpad in Init.Data.Array.Basic
Array.size in Init.Prelude
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

def findIdxRev? (cond : α → Bool) (as : Array α) : Option (Fin as.size) :=
  find ⟨ as.size, Nat.lt_succ_self _ ⟩
where
  find : Fin (as.size + 1) → Option (Fin as.size)
    | 0 => none
    | ⟨ i+1, h ⟩ =>
      if (cond as[i]) then
        some ⟨ i, Nat.lt_of_succ_lt_succ h ⟩
      else
        find ⟨ i, Nat.lt_of_succ_lt h ⟩

def coeff.{u} {F : Type u} [Semiring F] (f : F[X][Y]) (i j : ℕ) : F := (f.coeff j).coeff i

@[reducible]
def matchSize (a b : Array α) (unit : α) : Array α × Array α :=
  (a.rightpad (b.size) unit, b.rightpad (a.size) unit)

def findIdxRev?_maximal {cond} {as : Array α} {k : Fin as.size} :
  findIdxRev? cond as = some k → ∀ j : Fin as.size, j > k → ¬ cond as[j] :=

def findIdxRev?_def {cond} {as : Array α} {k : Fin as.size} :
  findIdxRev? cond as = some k → cond as[k] :=

def getLast (a : Array α) (h : a.size > 0) : α := a[a.size - 1]

instance instOneConcreteBTField (k : ℕ) : One (ConcreteBTField k) where
  one := one

Id.run in Init.Control.Id

noncomputable def changeOfBasisMatrix (ℓ : Nat) (h_ℓ : ℓ ≤ r) : Matrix (Fin (2^ℓ)) (Fin (2^ℓ)) L :=
    fun j i => (toCoeffsVec (L := L) (ℓ := ℓ) (
      basisVectors 𝔽q β ℓ h_ℓ j)) i

lift_knowledgeSound : ∀ outerStmtIn outerWitOut innerWitIn,
    compatWit outerWitOut innerWitIn →
    (lens.stmt.proj outerStmtIn, innerWitIn) ∈ innerRelIn →
    (outerStmtIn, lens.wit.lift (outerStmtIn, outerWitOut) innerWitIn) ∈ outerRelIn

def β (R : F[X][X][Y]) (t : ℕ) : 𝒪 H :=
  (β_regular R H (Nat.le_refl _) t).choose

structure Commit where
  commit : Data → Randomness → OracleComp oSpec Commitment

noncomputable def qMap_total_fiber
    
      (i : Fin r) (steps : ℕ) (h_i_add_steps : i.val + steps < ℓ + 𝓡)
        (y : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i.val + steps, by admit /- proof elided -/
        ⟩)) :
    Fin (2 ^ steps) → sDomain 𝔽q β h_ℓ_add_R_rate i :=
  if h_steps : steps = 0 then by
    
    subst h_steps
    simp only [add_zero, Fin.eta] at y
    exact fun _ => y
  else by
    
    let basis_y := sDomain_basis 𝔽q β h_ℓ_add_R_rate (i := ⟨i+steps,by admit /- proof elided -/
    ⟩) (by admit /- proof elided -/
    )
    let y_coeffs : Fin (ℓ + 𝓡 - (↑i + steps)) →₀ 𝔽q := basis_y.repr y

@[reducible, simp] def StmtIn := Unit

def powAlgHom :
  MvPolynomial (Fin m) F →ₐ[F] Polynomial F :=
   aeval fun j => Polynomial.X ^ (2 ^ (j : ℕ))

def queryCodeword (k : ℕ) (s : Fin (k + 1) → ℕ+) {i : Fin (k + 1)}
      (w : evalDomain D x (∑ j' ∈ (List.take i.1 (List.finRange (k + 1))).toFinset, (s j').1)) :
    OracleComp [FinalOracleStatement D x s]ₒ F :=
      OracleComp.lift <| by
        simpa using
          OracleSpec.query
            (spec := [FinalOracleStatement D x s]ₒ)
            ⟨i.1, Nat.lt_succ_of_lt i.2⟩
            (by admit /- proof elided -/
            )

def StateRestoration (oSpec : OracleSpec ι)
    (StmtIn WitIn WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) :=
  StmtIn → 
  WitOut → 
  pSpec.FullTranscript → 
  QueryLog (oSpec ++ₒ (srChallengeOracle StmtIn pSpec)) → 
  QueryLog oSpec → 
  OracleComp oSpec WitIn

@[inline, specialize, simp]
def verifier : Verifier oSpec Statement Statement !p[] := Verifier.id

instance instCharP2 {k : ℕ} : CharP (ConcreteBTField k) 2 :=
  charP_eq_2_of_add_self_eq_zero (F:=(ConcreteBTField k)) (sumZeroIffEq:=add_eq_zero_iff_eq)

instance : ∀ i, SelectableType (Challenge !p[] i) :=
  fun ⟨i, h⟩ =>
    (Fin.elim0 i : (h' : !p[].dir i = .V_to_P) → SelectableType (!p[].Challenge ⟨i, h'⟩)) h

HSMul.hSMul in Init.Prelude

def somePairs : HList' (fun x => x × x) someTypes :=
  HList'.cons (1, 1) (HList'.cons ("good", "bad") (HList'.cons (5, 3) HList'.nil))

def DVec {m : Type v} (α : m → Type u) : Type (max u v) := ∀ i, α i

noncomputable def finalFoldProver :
  OracleProver []ₒ
    (Statement F (Fin.last k)) (OracleStatement D x s (Fin.last k))
      (Witness F s d (Fin.last k).castSucc)
    (FinalStatement F k) (FinalOracleStatement D x s)
      (Witness F s d (Fin.last (k + 1)))
    (pSpec F) where
  PrvState
  | 0 =>
    (Statement F (Fin.last k) × ((j : Fin (k + 1)) → OracleStatement D x s (Fin.last k) j)) ×
      Witness F s d (Fin.last k).castSucc
  | _ =>
    (FinalStatement F k × ((j : Fin (k + 1)) → OracleStatement D x s (Fin.last k) j)) ×
      Witness F s d (Fin.last (k + 1))

PFunctor in Mathlib.Data.PFunctor.Univariate.Basic

def toNat (f : ValidChurchNat) : ℕ :=
  ChurchNat.toNat f.1

@[inline]
def seqCompose {m : ℕ} (Stmt : Fin (m + 1) → Type)
    {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    (V : (i : Fin m) → Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i)) :
    Verifier oSpec (Stmt 0) (Stmt (Fin.last m)) (seqCompose pSpec) := match m with
  | 0 => Verifier.id
  | _ + 1 => append (V 0) (seqCompose (Stmt ∘ Fin.succ) (fun i => V (Fin.succ i)))

let f_bar_i := uniqueClosestCodeword 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
      (i := ⟨i, by admit /- proof elided -/
      ⟩) (h_i := by admit /- proof elided -/
      ) f_i
      h_dist_curr_lt
    let folded_f_i := iterated_fold 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
      (steps := ⟨steps, by admit /- proof elided -/
      ⟩) (i := ⟨i, by admit /- proof elided -/
      ⟩)
      (h_i_add_steps := by admit /- proof elided -/
      ) f_i challenges
    let folded_f_bar_i := iterated_fold 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
      (steps := ⟨steps, by admit /- proof elided -/
      ⟩) (i := ⟨i, by admit /- proof elided -/
      ⟩)
      (h_i_add_steps := by admit /- proof elided -/
      ) f_bar_i challenges

def runWithOracle (f : spec.FunctionType) : OracleComp spec α → Option α :=
  OracleComp.construct' (spec := spec) (C := fun _ => Option α)
    
    (fun x => some x)
    
    (fun i q _ g => g (f i q))
    
    (none)

Subsingleton in Init.Core

def erase_even (s : Finset ℕ) : Finset ℕ := s.filter Odd

instance : _root_.Field Field := ZMod.instField fieldSize

def domainEnum (i : Fin (n + 1)) : Fin (2 ^ (n - i)) ↪ evalDomain D i :=
  ⟨domain D n i.1, domain_injective D i.1 (by admit /- proof elided -/
  )⟩

Fintype.ofFinite in Mathlib.Data.Fintype.EquivFin

def idxOf' [BEq α] (a : α) (l : List α) : ℕ := findIdx' (· == a) l

def join {k : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) : ConcreteBTField k :=

iSup in Mathlib.Order.SetNotation

IsLinearMap in Mathlib.Algebra.Module.LinearMap.Defs

abbrev Field := ZMod fieldSize

def shift_left (s : Finset ℕ) : Finset ℕ :=
  s.filterMap
    (fun n => match n with
      | 0 => .none
      | n + 1 => .some n
      )
    (by admit /- proof elided -/
    )

hEq := sorry

protected def Reduction.id : Reduction oSpec Statement Witness Statement Witness !p[] where
  prover := Prover.id
  verifier := Verifier.id

noncomputable def H_tilde' (H : F[X][Y]) : F[X][Y] :=
  let hᵢ (i : ℕ) := H.coeff i
  let d := H.natDegree
  let W := hᵢ d
  Polynomial.X ^ d +
    ∑ i ∈ (List.range d).toFinset,
      Polynomial.X^(d - 1 - i) *
      Polynomial.C (hᵢ (i + 1) * W ^ i)

def SkeletonNodeIndex.path {s : Skeleton} (idx : SkeletonNodeIndex s) :
    List (SkeletonNodeIndex s) := sorry

Fin.insertNth in Mathlib.Data.Fin.Tuple.Basic

Polynomial.aeval in Mathlib.Algebra.Polynomial.AlgebraMap

repr in Init.Data.Repr

List.Vector.get in Mathlib.Data.Vector.Defs

def divSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j, n j)) : Fin m :=
  (divSum? n k).get (divSum?_is_some_iff_lt_sum.mpr k.isLt)

DivisionRing in Mathlib.Algebra.Field.Defs

@[inline] def toT [Zero T] (c : Cayley T) : T := c.toFun 0

MvPolynomial.X in Mathlib.Algebra.MvPolynomial.Basic

let st1 : Vector KoalaBear.Field params.width :=
    Fin.foldl params.halfNumFullRounds (fun st_acc rc_idx =>
      let rc_chunk := (rcs.extract rc_idx (rc_idx + params.width)).cast (by admit /- proof elided -/
      )
      let st_new := fullRound params st_acc rc_chunk
      st_new) st0

Subtype.fintype in Mathlib.Data.Fintype.Sets

noncomputable def errorBound (δ : ℝ≥0) (deg : ℕ) (domain : ι ↪ F) : ℝ≥0 :=
  letI ρ : ℝ≥0 := ρ (ReedSolomon.code domain deg)
  if δ ∈ Set.Ioc 0 ((1 - ρ)/2)
  then Fintype.card ι / Fintype.card F
  else if δ ∈ Set.Ioo ((1 - ρ)/2) (1 - ρ.sqrt)
       then letI m := min (1 - ρ.sqrt - δ) (ρ.sqrt / 20)
            ⟨(deg ^ 2 : ℝ≥0) / ((2 * m) ^ 7 * (Fintype.card F : ℝ)), by admit /- proof elided -/
            ⟩
       else 0

Lagrange.basis in Mathlib.LinearAlgebra.Lagrange

Function.Surjective in Init.Data.Function

instance [Zero T] [ToNat T] : ToNat (Cayley T) where
  toNat := ToNat.toNat ∘ toT

def implGroupExpOracle : QueryImpl (GroupExpOracle ι p) (StateT (GroupValTable ι G) Option) where
  impl | query _ ⟨i, a, j⟩ => fun table =>
    match table i with
    | some g => some ((), table.update j (some (g ^ a.val)))
    | none => none

Module.Basis.span in Mathlib.LinearAlgebra.Basis.Basic

alias E_prp := collisionPerm

sendMessage
  | ⟨0, h⟩ => nomatch h

noncomputable def vanishingPoly (S : Finset F) : Polynomial F :=
  ∏ s ∈ S, (Polynomial.X - Polynomial.C s)

def Verifier.StateFunction.liftContext
    {σ : Type} {init : ProbComp σ} {impl : QueryImpl oSpec (StateT σ ProbComp)}
    (lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
    (V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
    (outerLangIn : Set OuterStmtIn) (outerLangOut : Set OuterStmtOut)
    (innerLangIn : Set InnerStmtIn) (innerLangOut : Set InnerStmtOut)
    [lensSound : lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut
      (V.compatStatement lens)]
    (stF : V.StateFunction init impl innerLangIn innerLangOut) :
      (V.liftContext lens).StateFunction init impl outerLangIn outerLangOut
where
  toFun := fun m outerStmtIn transcript =>
    stF m (lens.proj outerStmtIn) transcript
  toFun_empty := fun stmt => by admit /- proof elided -/

instance [Zero T] [ToNat T] : Mul (Cayley T) where
  mul := mul

def CEmbedding : R ↪ MvPolynomial σ R := ⟨C, C_injective σ R⟩

(Vector.flatten chunksAfterDiffusion).cast (params.widthDiv4_mul_4_eq_width)

def foldingBadEvent (i : Fin ℓ) (steps : ℕ) [NeZero steps] (h_i_add_steps : i + steps ≤ ℓ)
  (f_i : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by admit /- proof elided -/
  ⟩)
  (challenges : Fin steps → L) : Prop :=
  let d_i_plus_steps := BBF_CodeDistance ℓ 𝓡 ⟨i + steps, by admit /- proof elided -/
  ⟩
  if h_is_close : 2 * fiberwiseDistance 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (i := i)
      steps h_i_add_steps f_i < (d_i_plus_steps : ℕ∞) then
    
    
    
    let h_dist_curr_lt := fiberwise_dist_lt_imp_dist_lt_unique_decoding_radius 𝔽q β
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (i := i) (steps := steps) h_i_add_steps f_i h_is_close

eval₂_X {S : Type w} [CommSemiring S] (f : R →+* S) (x : S) : eval₂ f x X = x

@[ext]
structure ProverState (n : ℕ) where
  PrvState : Fin (n + 1) → Type

String in Init.Prelude

def Option.doubleBind_v2 {α β γ : Type} (f : α → β → Option γ)
    (x : Option α) (y : Option β) : Option γ := do
  let a ← x
  let b ← y
  f a b

WeierstrassCurve in Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

def BBF_SumcheckMultiplierParam : SumcheckMultiplierParam L ℓ (SumcheckBaseContext L ℓ) :=
  { multpoly := fun ctx => BBF_eq_multiplier ctx.t_eval_point }

def toNat (n : ChurchNat ℕ) : ℕ := n Nat.succ 0

@[simps!]
def MessageIdx.sumEquiv :
    MessageIdx pSpec₁ ⊕ MessageIdx pSpec₂ ≃ MessageIdx (pSpec₁ ++ₚ pSpec₂) where
  toFun := Sum.elim (MessageIdx.inl) (MessageIdx.inr)
  invFun := fun ⟨i, h⟩ => by admit /- proof elided -/

fun i => by admit /- proof elided -/

Mathlib.Meta.NormNum.IsNat in Mathlib.Tactic.NormNum.Result

instance [inst : ∀ i, DecidableEq (pSpec.Message i)] {k : Fin (n + 1)} :
    DecidableEq (MessagesUpTo k pSpec) :=
  @Fintype.decidablePiFintype _ _ (fun i => inst ⟨i.1.castLE (by admit /- proof elided -/
  ), i.property⟩) _

embed := sorry

match m with
  | ⟨0, _⟩ => 
    masterKStateProp (mp := mp) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑 := 𝓑)
      (stmtIdx := i.succ) (oracleIdx := i.castSucc)
      (h_le := by admit /- proof elided -/
      )
      (stmt := stmtIn) (wit := witMid) (oStmt := oStmtIn)
      (localChecks := True)
  | ⟨1, _⟩ => 
    let ⟨_, stmtOut, oStmtOut, witOut⟩ := getCommitProverFinalOutput 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i ⟨stmtIn, oStmtIn, witMid⟩
    masterKStateProp (mp := mp) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑 := 𝓑)
      (stmtIdx := i.succ) (oracleIdx := i.succ)
      (h_le := le_refl _)
      (stmt := stmtOut) (wit := witOut) (oStmt := oStmtOut)
      (localChecks := True)

input := fun ctxIn => by admit /- proof elided -/

instance : AlgebraTower (BTField) where
  algebraMap := towerAlgebraMap
  commutes' := by admit /- proof elided -/

@[reducible]
def empty : ProtocolSpec 0 := ⟨!v[], !v[]⟩

return none

structure DomainSeparator (U : Type) [SpongeUnit U] (H : Type*) [DuplexSpongeInterface U H] where
   
  io : String
deriving Repr

def leftpad (m₂ n₂ : ℕ) (a : α) {m₁ n₁ : ℕ} (M : Matrix (Fin m₁) (Fin n₁) α) :
    Matrix (Fin m₂) (Fin n₂) α :=
  Fin.leftpad m₂ (fun _ => a) (Fin.leftpad n₂ a ∘ M)

PFunctor.Lens in ToMathlib.PFunctor.Basic

def MLEEquivFin {n : ℕ} : R⦃≤ 1⦄[X (Fin n)] ≃ (Fin (2 ^ n) → R) :=
  Equiv.trans MLEEquiv (Equiv.piCongr finFunctionFinEquiv (fun _ => Equiv.refl _))

let sumcheck_check := h_i.val.eval 0 + h_i.val.eval 1 = stmtIn.sumcheck_target
    unless sumcheck_check do
      
      let dummyStmt : Statement (L := L) Context i.succ := {
        ctx := stmtIn.ctx,
        sumcheck_target := 0,
        challenges := Fin.snoc stmtIn.challenges 0
      }
      return dummyStmt

structure FSProverState (U : Type) [SpongeUnit U] (H : Type*) [DuplexSpongeInterface U H]
    (R : Type*) extends FSVerifierState U H where
   
  rng : ProverPrivateRng R
deriving Repr

def finalSumcheckKnowledgeError (m : pSpecFinalSumcheckStep (L := L).ChallengeIdx) :
  ℝ≥0 :=
  match m with
  | ⟨0, h0⟩ => nomatch h0

@[inline] def gt [Zero T] [ToNat T] (a b : Cayley T) : Prop :=
  (↑a : Nat) > (↑b : Nat)

noncomputable instance {R : Type u} [CommSemiring R] : PolynomialLike R R[X] where
  X := Polynomial.X
  eval₂ := Polynomial.eval₂RingHom
  eval₂_C := Polynomial.eval₂_C
  eval₂_X := Polynomial.eval₂_X
  eval₂_eq f := by admit /- proof elided -/

eval₂_eq {S : Type y} [CommSemiring S] {F : Type z} [FunEquiv F σ S] (h : P →+* S) :
    h = eval₂ (h.comp (Algebra.ofId R P)) (fun s => h (X s) : F)

def BacktrackSequence.Index (trace : QueryLog (duplexSpongeChallengeOracle StmtIn U))
    (state : CanonicalSpongeState U) (seq : BacktrackSequence trace state) :
    Fin trace.length × (Fin seq.inputState.length → Fin trace.length) :=
  
  
  
  (⟨trace.findIdx sorry, sorry⟩, sorry)

private def k [Zero F] (B : Finset (Fin n → F)) : ℚ :=
  (1 : ℚ) / n * ∑ i, K B i 0

def forwardRange (n : ℕ) (r : Fin (n)) (l : Fin (r.val + 1)) : List (Fin n) :=
  let len := r.val - l.val + 1
  List.ofFn (fun (k : Fin len) =>
    let val := l.val + k.val
    have h_bound : val < n := by admit /- proof elided -/
  )

class ProverFirst (pSpec : ProtocolSpec n) [NeZero n] where
  prover_first' : pSpec.dir 0 = .P_to_V

noncomputable def hasMutualCorrAgreement
  (Gen : ProximityGenerator ι F) [Fintype Gen.parℓ]
  (BStar : ℝ) (errStar : ℝ → ENNReal) :=
    haveI := Gen.Gen_nonempty
    ∀ (f : Gen.parℓ → ι → F) (δ : ℝ≥0) (_hδ : 0 < δ ∧ δ < 1 - BStar),
    Pr_{let r ←$ᵖ Gen.Gen}[ proximityCondition f δ r Gen.C ] ≤ errStar δ

protected def Prover.id : Prover oSpec Statement Witness Statement Witness !p[] where
  PrvState := fun _ => Statement × Witness
  input := _root_.id
  sendMessage := fun i => Fin.elim0 i
  receiveChallenge := fun i => Fin.elim0 i
  output := pure

def MlPoly.mk {R : Type*} (n : ℕ) (v : Vector R (2 ^ n)) : MlPoly R n := v

output := fun ⟨⟨chals, o⟩, p⟩ => pure <|
    ⟨
      ⟨
        chals,
        fun j =>
          if h : j.1 < i.1
          then by admit /- proof elided -/
      ⟩,
      p
    ⟩

@[inline, specialize]
def eval (x : R) (p : UniPoly R) : R :=
  p.eval₂ (RingHom.id R) x

Algebra.TensorProduct.instAlgebra in Mathlib.RingTheory.TensorProduct.Basic

def monomialXY (n m : ℕ) : F →ₗ[F] F[X][Y] where
  toFun t := ⟨Finsupp.single m ⟨(Finsupp.single n t)⟩⟩
  map_add' x y := by admit /- proof elided -/

@[simp]
abbrev Witness.AfterLinearCombination : Type := Unit

structure ParamConditions (P : Params ι F) where
  m : ℕ 
  h_m : m = P.varCount 0
  h_sumkLt : ∑ i : Fin (M + 1), P.foldingParam i ≤ m
  h_varCount_i : ∀ i : Fin (M + 1),
    P.varCount i = m - ∑ j : Fin i, P.foldingParam (Fin.castLT j (Nat.lt_trans j.isLt i.isLt))
  h_smooth : ∀ i : Fin (M + 1), Smooth (P.φ i)
  h_repeatPLt : ∀ i : Fin (M + 1), P.repeatParam i ≤ Fintype.card (ι i)

@[inline, reducible]
def toContext :
    Context.Lens (OuterStmtIn × (∀ i, OuterOStmtIn i)) (OuterStmtOut × (∀ i, OuterOStmtOut i))
                (InnerStmtIn × (∀ i, InnerOStmtIn i)) (InnerStmtOut × (∀ i, InnerOStmtOut i))
                OuterWitIn OuterWitOut InnerWitIn InnerWitOut :=
  ⟨lens.stmt, lens.wit⟩

def Transcript.removeSalt {k : Fin (n + 1)} (transcript : (pSpec.addSalt Salt).Transcript k) :
    pSpec.Transcript k :=

instance (k : ℕ) : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype

Set.offDiag in Mathlib.Data.Set.Operations

Nat.boddDiv2 in Mathlib.Data.Nat.Bits

IsField in Mathlib.Algebra.Field.IsField

def bitsToU (i : Fin r) (k : Fin (2 ^ i.val)) :
    AdditiveNTT.U (L := L) (𝔽q := 𝔽q) (β := β) i :=
  let val := (Finset.univ : Finset (Fin i)).sum fun j =>
    if (Nat.getBit (n := k.val) (k := j.val) == 1) then
      β ⟨j, by admit /- proof elided -/
      ⟩
    else 0

noncomputable def foldProver :
  OracleProver []ₒ
    (Statement F i.castSucc) (OracleStatement D x s i.castSucc) (Witness F s d i.castSucc.castSucc)
    (Statement F i.succ) (OracleStatement D x s i.succ) (Witness F s d i.castSucc.succ)
    (pSpec D x s i) where
  PrvState
  | 0 =>
    (Statement F i.castSucc × ((j : Fin (↑i.castSucc + 1)) → OracleStatement D x s i.castSucc j)) ×
      Witness F s d i.castSucc.castSucc
  | _ =>
    (Statement F i.succ × ((j : Fin (↑i.castSucc + 1)) → OracleStatement D x s i.castSucc j)) ×
      Witness F s d i.castSucc.succ

instance : Sub (UniPoly R) := ⟨UniPoly.sub⟩

def getPutativeRoot_with_hash {s} (idx : BinaryTree.SkeletonLeafIndex s)
    (leafValue : α) (proof : List α) (hashFn : α → α → α) : α :=
  match proof with
  | [] => leafValue 
  | siblingBelowRootHash :: restProof =>
    match idx with
    | BinaryTree.SkeletonLeafIndex.ofLeaf =>
      
      
      
      leafValue
    | BinaryTree.SkeletonLeafIndex.ofLeft idxLeft =>
      
      hashFn (getPutativeRoot_with_hash idxLeft leafValue restProof hashFn) siblingBelowRootHash
    | BinaryTree.SkeletonLeafIndex.ofRight idxRight =>
      
      hashFn siblingBelowRootHash (getPutativeRoot_with_hash idxRight leafValue restProof hashFn)

noncomputable def batchOracleReduction :
  OracleReduction []ₒ
    Unit (OracleStatement D x m) (Witness F s d m)
    ((Fin m → F) × Fri.Spec.Statement F (0 : Fin (k + 1)))
    (OracleStatement D x m)
    (Fri.Spec.Witness F s d (0 : Fin (k + 2)))
    (batchSpec F m) where
  prover := batchProver D x s d m
  verifier := batchVerifier (k := k) D x m

OracleComp.SelectableType in VCVio.OracleComp.Constructions.UniformSelect

sendMessage 
  | ⟨0, _⟩ => fun inputPrvState => by admit /- proof elided -/
  | ⟨0, h⟩ => nomatch h

instance {k : ℕ} : IntCast (ConcreteBTField k) where
  intCast n:= intCast n

def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) (t : ℕ) : 𝕃 H :=
  α x₀ R _ (φ := ⟨H_irreducible⟩) t

def rtake {n : ℕ} {α : Fin n → Sort*} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
    (i : Fin m) → α (Fin.cast (Nat.sub_add_cancel h) (natAdd (n - m) i)) :=
  fun i => v (Fin.cast (Nat.sub_add_cancel h) (natAdd (n - m) i))

instance [Zero T] [ToNat T] : DecidableRel (@LE.le (Cayley T) _) := fun a b =>
  Nat.decLe (↑a) (↑b)

instance instSelectableTypeChallengePSpec [SelectableType R] :
    ∀ i, SelectableType ((pSpec R deg).Challenge i) :=
  instSelectableTypeChallengeAppend

def localized_fold_eval (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i + steps ≤ ℓ)
    (f : (sDomain 𝔽q β h_ℓ_add_R_rate)
      ⟨i, by exact Nat.lt_of_le_of_lt (n := i) (k := r) (m := ℓ) (h₁ := by
        exact Fin.is_le') (by exact lt_of_add_right_lt h_ℓ_add_R_rate)⟩ → L)
    (r_challenges : Fin steps → L)
    (y : (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨↑i + steps, by omega⟩) : L :=

class IsKnowledgeSound (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut))
    (verifier : Verifier oSpec StmtIn StmtOut pSpec) where
  knowledgeError : ℝ≥0
  is_knowledge_sound : knowledgeSoundness init impl relIn relOut verifier knowledgeError

def OracleReduction.append (R₁ : OracleReduction oSpec Stmt₁ OStmt₁ Wit₁ Stmt₂ OStmt₂ Wit₂ pSpec₁)
    (R₂ : OracleReduction oSpec Stmt₂ OStmt₂ Wit₂ Stmt₃ OStmt₃ Wit₃ pSpec₂) :
      OracleReduction oSpec Stmt₁ OStmt₁ Wit₁ Stmt₃ OStmt₃ Wit₃ (pSpec₁ ++ₚ pSpec₂) where
  prover := Prover.append R₁.prover R₂.prover
  verifier := OracleVerifier.append R₁.verifier R₂.verifier

def extract {n : ℕ} {α : Fin n → Sort*} (start stop : ℕ) (h1 : start ≤ stop) (h2 : stop ≤ n)
    (v : (i : Fin n) → α i) : (i : Fin (stop - start)) → α ⟨i + start, by admit /- proof elided -/
    ⟩ :=
  fun i ↦ v ⟨i + start, by admit /- proof elided -/
  ⟩

Matrix.vecMul in Mathlib.Data.Matrix.Mul

@[elab_as_elim] def Fin.predRecOnSameFinType {motive : Fin r → Sort _}
    (last : motive (⟨r - 1, by
      have h_r_ne_0: r ≠ 0 := by exact NeZero.ne r
      omega
    ⟩ : Fin r))
    (succ : ∀ i : Fin r, i.val > 0 → motive i → motive (⟨i.val - 1, by omega⟩ : Fin r))
    (i : Fin r): motive i :=

@[reducible, inline, specialize]
def ChallengesUpTo (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type :=
  ∀ i, (pSpec.take k k.is_le).Challenge i

List.Vector.snoc in Mathlib.Data.Vector.Snoc

def simulateQ' (oa : OracleComp spec α) (h : oa.neverFails) : m α :=

def additiveNTTInvariant (evaluation_buffer : Fin (2 ^ (ℓ + R_rate)) → L)
    (original_coeffs : Fin (2 ^ ℓ) → L) (i : Fin (ℓ + 1)) : Prop :=
  ∀ (j : Fin (2^(ℓ + R_rate))),
    let u_b_v := j.val
    let v: Fin (2^i.val) := ⟨Nat.getLowBits i.val u_b_v, by admit /- proof elided -/
    ⟩ 
    let u_b := u_b_v / (2^i.val) 
    have h_u_b : u_b = u_b_v / (2^i.val) := by admit /- proof elided -/

@[reducible, simp] def StmtIn : Type := R

eval₂_eq {S : Type w} [CommSemiring S] (g : P →+* S) :
    g = eval₂ (g.comp (Algebra.ofId R P)) (g X)

def U (i : Fin r) : Subspace 𝔽q L := Submodule.span 𝔽q (β '' (Set.Ico 0 i))

def toMessagesChallenges (transcript : FullTranscript pSpec) : Messages pSpec × Challenges pSpec :=

def rho (n : ℕ) : Option ℕ := Id.run do
  for st in [2:n] do
    for c in [1:n] do
      if let some d := rho' n st c then
        return some d

@[inline, reducible]
protected def id :
    Witness.Lens OuterStmtIn OuterStmtOut OuterWitIn OuterWitOut OuterWitIn OuterWitOut :=
  ⟨Prod.snd, fun _ => Prod.snd⟩

def proximityMeasure (u v : n → F) (d : ℕ) : ℕ :=
  Fintype.card {r : F | Δ₀'(r • u + (1 - r) • v, C) ≤ d}

noncomputable def proximityError (F : Type*) [Fintype F] (d : ℕ) (ρ : ℝ) (δ : ℝ) (m : ℕ) : ℝ :=
  if δ ≤ (1 - ρ) / 2 then
    ((m - 1) * d) / (ρ * (Fintype.card F))
  else
    let min_val := min (1 - (Real.sqrt ρ) - δ ) ((Real.sqrt ρ) / 20)
    ((m - 1) * d^2) / ((Fintype.card F) * (2 * min_val)^7)

noncomputable def polyQuotient (S : Finset F) (fPoly : F[X]) : F[X] :=
    (fPoly - (ansPoly S (fun s => fPoly.eval s))) / (vanishingPoly S)

Subtype in Init.Prelude

hδLe : ∀ i : Fin (M + 1),
    (δ i) ≤ 1 - Finset.univ.sup (fun j => BStar i j (C i j) (Gen_α i j).parℓ)

noncomputable def coeffs_of_close_proximity (ωs : Fin n ↪ F) (δ : ℚ) (u₀ u₁ : Fin n → F)
  : Finset F := Set.toFinset { z | ∃ v : ReedSolomon.code ωs (k + 1), δᵣ(u₀ + z • u₁, v) ≤ δ}

inductive SkeletonNodeIndex : Skeleton → Type
  | ofLeaf : SkeletonNodeIndex Skeleton.leaf
  | ofInternal {left right} :
      SkeletonNodeIndex (Skeleton.internal left right)
  | ofLeft {left right : Skeleton} (idxLeft : SkeletonNodeIndex left) :
      SkeletonNodeIndex (Skeleton.internal left right)
  | ofRight {left right : Skeleton} (idxRight : SkeletonNodeIndex right) :
      SkeletonNodeIndex (Skeleton.internal left right)

@[inline] def add (a b : AssocNat) : AssocNat :=
  ⟨a ∘ b, by admit /- proof elided -/
  ⟩

abbrev BaseField := ZMod baseFieldSize

Polynomial.compRingHom in Mathlib.Algebra.Polynomial.Eval.Defs

instance : Unique (ProtocolSpec 0) where
  default := empty
  uniq := fun ⟨_, _⟩ => by admit /- proof elided -/

ZeroMemClass in Mathlib.Algebra.Group.Submonoid.Defs

noncomputable instance : Algebra K (Left ⊗[K] Right) := Algebra.TensorProduct.instAlgebra

instance : ∀ j, OracleInterface ((pSpec D x l).Message j) := fun j =>
  match j with
  | ⟨0, h⟩ => nomatch h

Function.Bijective in Mathlib.Logic.Function.Defs

δ : Fin (M + 1) → ℝ≥0
  dist : (i : Fin (M + 1)) → Fin ((P.foldingParam i) + 1) → ℝ≥0

CanLift in Mathlib.Tactic.Lift

instance : DecidableEq BTF₃ := (inferInstance : DecidableEq (ConcreteBTField 3))

st3
</all_available_defs>

<all_available_lemmas>
Nat.lt_succ_self in Init.Prelude
Array.foldl_induction in Init.Data.Array.Lemmas
Array.getD_eq_getD_getElem? in Init.Data.Array.Lemmas
Array.getElem?_eq_none in Init.Data.Array.Lemmas
Array.getElem_zipIdx in Init.Data.Array.MapIdx
Nat.lt_trichotomy in Init.Data.Nat.Basic
Option.getD_none in Init.Data.Option.Basic
Polynomial.coeff_C_mul in Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_X_pow in Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_add in Mathlib.Algebra.Polynomial.Coeff
ite_eq_left_iff in Init.PropLemmas
mul_ite in Mathlib.Algebra.Notation.Defs
mul_one in Mathlib.Algebra.Group.Defs
Array.size_rightpad in Init.Data.Array.Lemmas
Polynomial.ext in Mathlib.Algebra.Polynomial.Basic
congrArg in Init.Prelude
Bool.false_eq_true in Init.Data.Bool
bne_iff_ne in Init.SimpLemmas
bne_self_eq_false in Init.SimpLemmas
ne_eq in Init.SimpLemmas
Array.getElem?_eq_getElem in Init.Data.Array.Lemmas
Array.getElem_extract in Init.Data.Array.Lemmas
Array.size_extract in Init.Data.Array.Lemmas
Nat.lt_or_ge in Init.Prelude
Nat.succ_le_of_lt in Init.Data.Nat.Basic
Option.getD_some in Init.Data.Option.Basic
Fin.le_antisymm in Init.Data.Fin.Lemmas
Nat.lt_of_not_ge in Init.Data.Nat.Basic
Nat.le_of_not_lt in Init.Data.Nat.Basic
Fin.is_lt in Init.Data.Fin.Lemmas
Nat.pred_lt_self in Init.Data.Nat.Basic
Nat.le_of_pred_lt in Init.Data.Nat.Lemmas
Option.some_inj in Init.Data.Option.Instances
Array.eq_empty_of_size_eq_zero in Init.Data.Array.Lemmas
Array.ne_empty_of_size_pos in Init.Data.Array.Lemmas
Nat.le_antisymm in Init.Prelude
Nat.succ_pred_eq_of_pos in Init.Data.Nat.Basic
le_refl in Mathlib.Order.Defs.PartialOrder
Nat.eq_zero_or_pos in Init.Data.Nat.Basic
Polynomial.degree_eq_bot in Mathlib.Algebra.Polynomial.Degree.Definitions
Polynomial.degree_eq_natDegree in Mathlib.Algebra.Polynomial.Degree.Definitions
Polynomial.degree_ne_bot in Mathlib.Algebra.Polynomial.Degree.Definitions
Polynomial.leadingCoeff_ne_zero in Mathlib.Algebra.Polynomial.Degree.Definitions
Array.getElem?_ofFn in Init.Data.Array.Lemmas
Nat.lt_of_succ_le in Init.Data.Nat.Basic
Polynomial.coeff_eq_zero_of_natDegree_lt in Mathlib.Algebra.Polynomial.Degree.Operations
not_lt in Mathlib.Order.Defs.LinearOrder
symm in Mathlib.Order.Defs.Unbundled

theorem findIdxRev?_eq_some {cond} {as : Array α} (h : ∃ i, ∃ hi : i < as.size, cond as[i]) :
  ∃ k : Fin as.size, findIdxRev? cond as = some k

theorem findIdxRev?_eq_none {cond} {as : Array α} (h : ∀ i, (hi : i < as.size) → ¬ cond as[i]) :
  findIdxRev? cond as = none

theorem findIdxRev?_emtpy_none {cond} {as : Array α} (h : as = #[]) :
  findIdxRev? cond as = none

@[simp]
theorem OracleVerifier.run_eq_run_verifier [Oₘ : ∀ i, OracleInterface (pSpec.Message i)]
    {stmt : StmtIn} {oStmt : ∀ i, OStmtIn i} {transcript : FullTranscript pSpec}
    {verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec} :
      verifier.run stmt oStmt transcript =
        verifier.toVerifier.run ⟨stmt, oStmt⟩ transcript

lemma mul_by_2_def {s : Finset ℕ} :
    mul_by_2 s = s.map ⟨fun n => 2 * n, by {
      intro a b
      simp
    }⟩

omit hF₂ in
theorem W_linear_comp_decomposition (i : Fin r) (h_i_add_1 : i + 1 < r) :
    ∀ p: L[X], (W 𝔽q β (i + 1)).comp p =
      ((W 𝔽q β i).comp p) ^ Fintype.card 𝔽q -
        C (eval (β i) (W 𝔽q β i)) ^ (Fintype.card 𝔽q - 1) * ((W 𝔽q β i).comp p)

lemma separable_iff_discr_eq_zero {F : Type} [Field F] [Inhabited F] (f : F[X]) :
  f.Separable ↔ discriminant f ≠ 0

theorem zero_lt_pow_n (m : ℕ) (n : ℕ) (h_m : m > 0): 0 < m^n

theorem toNatInRange {k : ℕ} (b : ConcreteBTField k) :
  BitVec.toNat b ≤ 2 ^ (2 ^ k) * 1

Nat.le_add_left in Init.Data.Nat.Basic

theorem verifier_rbrKnowledgeSoundness [Fintype R] :
    (verifier R n deg D oSpec i).rbrKnowledgeSoundness init impl
    (relationRound R n deg D i.castSucc) (relationRound R n deg D i.succ)
    (fun _ => (deg : ℝ≥0) / Fintype.card R)

@[simp]
theorem generateProof_ofRight {sleft sright : Skeleton}
    (cache_tree : FullData α (Skeleton.internal sleft sright))
    (idxRight : SkeletonLeafIndex sright) :
    generateProof cache_tree (BinaryTree.SkeletonLeafIndex.ofRight idxRight) =
      (cache_tree.leftSubtree).getRootValue ::
        (generateProof cache_tree.rightSubtree idxRight)

@[simp]
theorem oracleVerifier_rbrKnowledgeSoundness (hRel : ∀ stmtIn oStmtIn witOut,
      ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), witOut) ∈ relOut →
      ((stmtIn, oStmtIn), mapWitInv (stmtIn, oStmtIn) witOut) ∈ relIn) :
    (oracleVerifier oSpec mapStmt embedIdx hEq).rbrKnowledgeSoundness init impl relIn relOut 0

theorem rightpad_eq_self (v : Fin n → α) (a : α) : rightpad n a v = v

omit Oₘ in
theorem seqCompose_completeness (hInit : init.neverFails)
    (rel : (i : Fin (m + 1)) → Set (Stmt i × Wit i))
    (R : ∀ i, Reduction oSpec (Stmt i.castSucc) (Wit i.castSucc) (Stmt i.succ) (Wit i.succ)
      (pSpec i))
    (completenessError : Fin m → ℝ≥0)
    (h : ∀ i, (R i).completeness init impl (rel i.castSucc) (rel i.succ) (completenessError i)) :
      (Reduction.seqCompose Stmt Wit R).completeness init impl (rel 0) (rel (Fin.last m))
        (∑ i, completenessError i)

theorem BitVec.extractLsb_concat_hi {hi_size lo_size : ℕ} (hi : BitVec hi_size)
  (lo : BitVec lo_size) (h_hi : hi_size > 0) :
  BitVec.extractLsb (hi:=hi_size + lo_size - 1) (lo:=lo_size)
  (BitVec.append (msbs:=hi) (lsbs:=lo)) = dcast (by
    rw [←Nat.sub_add_comm (by omega), Nat.sub_add_cancel (by omega), Nat.add_sub_cancel]
  ) hi

theorem dext_iff {α : Fin n → Sort u} {v w : (i : Fin n) → α i} :
    v = w ↔ ∀ i, v i = w i

theorem seqCompose_rbrKnowledgeSoundness
    (rel : ∀ i, Set ((Stmt i × ∀ j, OStmt i j) × Wit i))
    (V : (i : Fin m) → OracleVerifier oSpec (Stmt i.castSucc) (OStmt i.castSucc)
      (Stmt i.succ) (OStmt i.succ) (pSpec i))
    (rbrKnowledgeError : ∀ i, (pSpec i).ChallengeIdx → ℝ≥0)
    (h : ∀ i, (V i).rbrKnowledgeSoundness init impl
      (rel i.castSucc) (rel i.succ) (rbrKnowledgeError i)) :
    (OracleVerifier.seqCompose Stmt OStmt V).rbrKnowledgeSoundness
        init impl (rel 0) (rel (Fin.last m))
        (fun combinedIdx =>
          letI ij := seqComposeChallengeIdxToSigma combinedIdx
          rbrKnowledgeError ij.1 ij.2)

@[simp]
theorem dcons_zero {motive : Fin (n + 1) → Sort u} (a : motive 0)
    (v : (i : Fin n) → motive i.succ) : (a ::ᵈ⟨motive⟩ v) 0 = a

theorem BitVec.dcast_dcast_bitvec_extractLsb_eq {w hi lo : ℕ} (x : BitVec w)
  (h_width_eq : w = hi - lo + 1) : dcast h_width_eq (dcast (h_width_eq.symm)
  (BitVec.extractLsb (hi:=hi) (lo:=lo) x)) = BitVec.extractLsb (hi:=hi) (lo:=lo) x

lemma proximity_gap
  {F : Type} [Field F] [Fintype F] [DecidableEq F]
  {ι : Type} [Fintype ι] [Nonempty ι] {φ : ι ↪ F}
  {degree m : ℕ} {δ : ℝ≥0} {f : Fin m → ι → F} {GenFun : F → Fin m → F}
  (h : ∀ (hδLe : δ < 1 - Bstar (LinearCode.rate (code φ degree))) {f : Fin m → ι → F},
        Pr_{
          let r ← $ᵖ F}[δᵣ((fun x => ∑ j : Fin m, (GenFun r j) * f j x), code φ degree) ≤ (δ : ℝ)]
            > ENNReal.ofReal (proximityError F degree (LinearCode.rate (code φ degree)) δ m)) :

@[grind _=_]
lemma total_deg_as_weighted_deg :
  totalDegree f = natWeightedDegree f 1 1

Nat.add_le_add_left in Init.Data.Nat.Basic

lemma domain_injective {i : ℕ} : i ≤ n → Function.Injective (domain D x n i)

@[to_additive]
lemma prod_univ_twos {M : Type*} [CommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) :
    (∏ i, f i) = f (Fin.cast hn.symm 0) * f (Fin.cast hn.symm 1)

theorem succ'_injective : Function.Injective (succ' : Nat → Nat)

theorem randomOracle_cache_neverFails_iff_runWithOracle_neverFails {β}
    [DecidableEq ι] [spec.DecidableEq] [(i : ι) → SelectableType (OracleSpec.range spec i)]
    (oa : OracleComp (spec) β) (preexisting_cache : spec.QueryCache)
    :
    ((oa.simulateQ randomOracle).run preexisting_cache).neverFails
    ↔
    (∀ (f : spec.FunctionType),
      Oracle.containsCache f preexisting_cache →
      (runWithOracle f oa).isSome)

@[simp]
theorem oracleReduction_completeness (h : init.neverFails) :
    (oracleReduction oSpec Statement OStatement pred).perfectCompleteness init impl
    (toRelInput pred hPred) Set.univ

lemma solution_gamma_is_linear_in_Z
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  :
  ∃ (v₀ v₁ : F[X]),
    γ' x₀ (R k δ x₀ h_gs) (irreducible_H k (x₀ := x₀) (δ := δ) h_gs) =
        AppendixA.polyToPowerSeries𝕃 _
          (
            (Polynomial.map Polynomial.C v₀) +
            (Polynomial.C Polynomial.X) * (Polynomial.map Polynomial.C v₁)
          )

lemma and_one_eq_of_eq {a b : ℕ} : a = b → a &&& 1 = b &&& 1

@[simp]
theorem seqCompose_succ_eq_append {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    {T : ∀ i, FullTranscript (pSpec i)} :
    seqCompose T = append (T 0) (seqCompose (fun i => T (Fin.succ i)))

theorem hcons_eq_cons {β : Fin n → Sort u} (a : α) (v : (i : Fin n) → β i) :
    hcons a v = cons (α := vcons α β) (hcons a v 0) (fun i => hcons a v i.succ)

omit [CharP L 2] [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 [NeZero 𝓡] in
lemma take_snoc_oracle_eq_oStmtIn (i : Fin ℓ)
    (oStmtIn : (j : Fin (toOutCodewordsCount ℓ ϑ i.castSucc)) →
      OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)
    (newOracleFn : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :
    (take_snoc_oracle 𝔽q β i oStmtIn newOracleFn) = oStmtIn

lemma mkLastOracleIndex_last : mkLastOracleIndex ℓ ϑ (Fin.last ℓ) = ℓ / ϑ - 1

@[simp]
theorem simulateQ'_query (q : OracleQuery spec α) :
    simulateQ' so q (by simp) = so.impl q

@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
    twoAdicGenerators[idx.val + 1] ^ 2 = twoAdicGenerators[idx]

private lemma le_sum_choose_K [Zero F]
  (h_card : 2 ≤ (Fintype.card F)) :
  choose_2 (K B i 0) + (Fintype.card (α := F) - 1) *
  choose_2 ((B.card - K B i 0) / (Fintype.card (α := F) - 1)) ≤ sum_choose_K_i B i

lemma forwardRange_length (n : ℕ) (r : Fin n) (l : Fin (r.val + 1)) :
    (forwardRange n r l).length = r.val - l.val + 1

Fin.eta in Init.Data.Fin.Lemmas

lemma decoded_polynomial_lt_deg (c : ReedSolomon.code domain deg) :
  decode c ∈ (degreeLT F deg : Submodule F F[X])

lemma getLowBits_zero_eq_zero {n : ℕ} : getLowBits 0 n = 0

@[simp]
theorem cast_run (stmt : StmtIn) (transcript : FullTranscript pSpec₁) :
    V.run stmt transcript = (V.cast hn hSpec).run stmt (transcript.cast hn hSpec)

@[simp]
lemma finite_possibleDeltas : (possibleDeltas U V).Finite

theorem neg_trim [LawfulBEq R] (p : UniPoly R) : p.trim = p → (-p).trim = -p

@[simp]
protected lemma elocPoly_one :
  ElocPoly 1 ωs f p = if f 0 ≠ p.eval (ωs 0) then X - (C (ωs 0)) else 1

theorem cast_injective : Function.Injective (ChallengeIdx.cast hn hSpec)

theorem Nat.reconstruct_from_hi_and_lo_parts_or_ver (n hi_len lo_len : ℕ)
  (h_n : n < 2 ^ (hi_len + lo_len)) :
    n = (((n >>> lo_len) % (2 ^ hi_len)) <<< lo_len) ||

lemma testBit_of_sub_two_pow_of_bit_1 {n i : ℕ} (h_testBit_eq_1 : (n).testBit i = true) :
  (n - 2^i).testBit i = false

theorem liftContext_rbr_knowledgeSoundness [Inhabited InnerWitIn]
    {rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0}
    {stmtLens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                                OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut}
    {witLens : Witness.InvLens (OuterStmtIn × ∀ i, OuterOStmtIn i)
                            OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
    (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec)
    [lensKS : Extractor.Lens.IsKnowledgeSound
      outerRelIn innerRelIn outerRelOut innerRelOut
      (V.toVerifier.compatStatement stmtLens) (fun _ _ => True) ⟨stmtLens, witLens⟩]
    (h : V.rbrKnowledgeSoundness init impl innerRelIn innerRelOut rbrKnowledgeError) :
      (V.liftContext stmtLens).rbrKnowledgeSoundness init impl outerRelIn outerRelOut
        rbrKnowledgeError

theorem size_eq_degree (p : UniPoly R) : p.trim.size = p.degree

@[simp]
lemma weight_constantCode [DecidableEq F] :
  wt (constantCode x ι) = 0 ↔ IsEmpty ι ∨ x = 0

lemma listOfCloseCodewords_eq_zero :
  listOfCloseCodewords C y n = 0 ↔ IsEmpty (hammingBall C y n) ∨ Infinite (hammingBall C y n)

lemma shift_left_def {s : Finset ℕ} :
    shift_left s = s.filterMap
    (fun n => match n with
      | 0 => .none
      | n + 1 => .some n
      )
    (by aesop)

theorem fullOracleReduction_perfectCompleteness (hInit : init.neverFails) :
  OracleReduction.perfectCompleteness
    (oracleReduction := fullOracleReduction 𝔽q β γ_repetitions (ϑ:=ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑))
    (relIn := roundRelation (mp := BBF_SumcheckMultiplierParam) 𝔽q β (ϑ:=ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑) 0)
    (relOut := acceptRejectOracleRel)
    (init := init)
    (impl := impl)

lemma Z_ne_zero {k : ℕ} : Z k ≠ zero

theorem SkeletonNodeIndex.rightChild_bind_parent {s : Skeleton}
    (idx : SkeletonNodeIndex s) :
    idx.rightChild >>= parent = idx.rightChild.map (fun _ => idx)

@[simp]
lemma OracleReduction.append_toReduction
    (R₁ : OracleReduction oSpec Stmt₁ OStmt₁ Wit₁ Stmt₂ OStmt₂ Wit₂ pSpec₁)
    (R₂ : OracleReduction oSpec Stmt₂ OStmt₂ Wit₂ Stmt₃ OStmt₃ Wit₃ pSpec₂) :
      (OracleReduction.append R₁ R₂).toReduction =
        Reduction.append R₁.toReduction R₂.toReduction

omit [Finite F] in
lemma mul_root_of_unity {x : Fˣ} :
  ∀ {a b : Fˣ} {i j : ℕ},
    i ≤ j → a ∈ evalDomain D x i → b ∈ Domain.evalDomain D j →
      a * b ∈ evalDomain D x i

lemma getBit_of_add_distrib {n m k : ℕ}
  (h_n_AND_m : n &&& m = 0) : getBit k (n + m) = getBit k n + getBit k m

@[simp]
theorem mul_accepts_iff : (mul a b c).accepts x ↔ x c = x a * x b

@[simp]
theorem MLE_eval_zeroOne (x : σ → Fin 2) (evals : (σ → Fin 2) → R) :
    MvPolynomial.eval (x : σ → R) (MLE evals) = evals x

theorem vcons_inj (a b : α) (v w : Fin n → α) : a ::ᵛ v = b ::ᵛ w ↔ a = b ∧ v = w

@[simp]
lemma width_pos : 0 < params.width

@[simp]
protected lemma elocPoly_leading_coeff_one : (ElocPoly n ωs f p).leadingCoeff = 1

theorem degreeOf_linear_le {a b : R} : degreeOf n (C a + C b * p) ≤ degreeOf n p

theorem join_add_join {k : ℕ} (h_pos : k > 0) (hi₀ lo₀ hi₁ lo₁ : ConcreteBTField (k - 1)) :
  《 hi₀, lo₀ 》 + 《 hi₁, lo₁ 》 = 《 hi₀ + hi₁, lo₀ + lo₁ 》

@[simp]
lemma coe_fn_of_coe (f : ∀ a, β a) : (f : F) = inst.equiv.invFun f

theorem eval_zeroOne_eq_MLE_toEvalsZeroOne (p : MvPolynomial σ R) (x : σ → Fin 2) :
    eval (x : σ → R) p = eval (x : σ → R) (MLE p.toEvalsZeroOne)

@[simp] theorem idxOf'_nil [BEq α] {a : α} : idxOf' a [] = 0

omit h_β₀_eq_1 in
theorem sDomainFin_bijective (i : Fin r) (h_i : i < ℓ + R_rate)
: Function.Bijective
  (sDomainFinEquiv 𝔽q β h_ℓ_add_R_rate i h_i)

@[simp]
theorem zero_dappend {motive : Fin (0 + n) → Sort u} {u : (i : Fin 0) → motive (castAdd n i)}
    (v : (i : Fin n) → motive (natAdd 0 i)) :
    dappend (motive := motive) u v = fun i => cast (by simp) (v (i.cast (by omega)))

theorem hconcat_eq_snoc {α : Fin n → Sort u} {β : Sort u} (v : (i : Fin n) → α i) (b : β) :
    hconcat v b = snoc (α := vconcat α β)
      (fun i => cast (vconcat_castSucc _ _ i).symm (v i))
      (cast (vconcat_last _ _).symm b)

@[simp]
lemma Rhs_add_one : Rhs (e + 1) ωs f = fun i ↦ Rhs e ωs f i * ωs i

theorem coeffs_of_comp_minus_x {f : Polynomial F} {n : ℕ} :
    (f.comp (-X)).coeff n = if Even n then f.coeff n else -f.coeff n

lemma eval₂_f_eq_C (r : R) (x : P) : eval₂ (P := P) (C : R →+* P) x (C r) = C r

lemma concrete_mul_comm
  {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k := k - 1))
  (a b : ConcreteBTField k) :
  concrete_mul a b = concrete_mul b a

theorem split_Z {k : ℕ} (h_pos : k > 0) :
    split h_pos (Z k) = (one (k:=k - 1), zero (k:=k - 1))

@[simp]
theorem mul_by_2_mem {s : Finset ℕ} {d : ℕ} :
    d ∈ mul_by_2 s ↔ Even d ∧ (d / 2) ∈ s

lemma coeff_toPoly {p : UniPoly Q} {n : ℕ} : p.toPoly.coeff n = p.coeff n

theorem degreeOf_eval_C_finSuccEquiv (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (x : R) :
    degreeOf j (Polynomial.eval (C x) (finSuccEquiv R n p)) ≤ degreeOf j.succ p

@[simp]
lemma seqCompose_succ {m : ℕ} (Stmt : Fin (m + 2) → Type)
    {n : Fin (m + 1) → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    (V : (i : Fin (m + 1)) → Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i)) :
    seqCompose Stmt V = append (V 0) (seqCompose (Stmt ∘ Fin.succ) (fun i => V (Fin.succ i)))

theorem dconcat_inj {motive : Fin (n + 1) → Sort u} (v w : (i : Fin n) → motive (castSucc i))
    (a b : motive (last n)) :
    (v :+ᵈ⟨motive⟩ a) = (w :+ᵈ⟨motive⟩ b) ↔ v = w ∧ a = b

lemma concrete_exists_pair_ne {k : ℕ} : ∃ x y : ConcreteBTField k, x ≠ y

@[simp]
theorem BTField.PowerBasis.dim_of_eq_rec
    (r1 r : ℕ)
    (h_r : r = r1 + 1)
    (b : PowerBasis (BTField r1) (BTField (r1 + 1))) :
    letI instAlgebra : Algebra (BTField r1) (BTField r) :=
      binaryAlgebraTower (l:=r1) (r:=r) (h_le:=by omega)
    ((Eq.rec (motive:=fun (x : ℕ) (_ : r1 + 1 = x) => by
      letI instAlgebraCur : Algebra (BTField r1) (BTField x) :=
        binaryAlgebraTower (l:=r1) (r:=x) (h_le:=by omega)
      exact PowerBasis (BTField r1) (BTField x)) (refl:=b) (t:=h_r.symm)) :
        PowerBasis (BTField r1) (BTField r)).dim
    = b.dim

lemma if_self_rfl {α : Type*} [DecidableEq α] (a b : α) :
  (if a = b then b else a) = a

lemma relHammingDist_le_blockRelDistance
  (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} {φ' : (indexPowT S φ i) ↪ F}
  [DecidableEq F] [DecidableEq ι] [Smooth φ]
  (f g : (indexPowT S φ i) → F) (S' : Finset (indexPowT S φ i))
  [h_fintype : ∀ i : ℕ, Fintype (indexPowT S φ i)]
  [DecidableEq (indexPowT S φ i)] [Smooth φ']
  [h_dec : DecidableBlockDisagreement i k f S' φ'] :
  δᵣ(f, g) ≤ Δᵣ(i, k, f, S', φ', g)

theorem ScalarField_is_prime : Nat.Prime scalarFieldSize

Nat.succ_le_succ in Init.Prelude

private lemma natDegree_Q
  (h : (Δ₀(f, p.eval ∘ ωs) : ℕ) ≤ e) :
  (Q ωs f p e).natDegree ≤ e + p.natDegree

theorem getBit_repr_univ {ℓ : Nat} : ∀ j, j < 2^ℓ →
  j = ∑ k ∈ Finset.univ (α:=Fin ℓ), (getBit k j) * 2^k.val

@[simp]
private lemma E_ne_zero : (E ωs f p e) ≠ 0

theorem two_le_two_pow_n_plus_1 (n : ℕ) : 2 ≤ 2 ^ (n + 1)

theorem funext_heq_iff {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v}
    {f : (x : α) → β x} {g : (x : α') → β' x} (ha : α = α') (hb : ∀ x, β x = β' (cast ha x)) :
      HEq f g ↔ ∀ x, HEq (f x) (g (cast ha x))

Fin.ext in Init.Data.Fin.Lemmas

lemma getBit_zero_eq_zero {k : Nat} : getBit k 0 = 0

theorem LeafData.composeBuild_leaf {α} (a : α)
    (compose : α → α → α) :
    (LeafData.leaf a).composeBuild compose = FullData.leaf a

@[simp]
lemma concrete_natCast_one_eq_one {k : ℕ} : natCast 1 = (1 : ConcreteBTField k)

lemma eqRec_fun_eqRec_sort_eq_self {α : Sort*} {β : α → Sort u} {a a' : α}
    (h : a = a') (h' : β a = β a') (b : β a) :
  b = h ▸ h' ▸ b

@[simp]
theorem dflatten_splitSum {m : ℕ} {n : Fin m → ℕ} {motive : (k : Fin (vsum n)) → Sort*}
    (v : (k : Fin (vsum n)) → motive k) (k : Fin (vsum n)) :
    dflatten (motive := motive) (fun i j => v (embedSum i j)) k = v k

lemma W_prod_comp_decomposition
    (i : Fin r) (hi : i > 0) :
    (W 𝔽q β i) = ∏ c: 𝔽q, (W 𝔽q β (i-1)).comp (X - C (c • β (i-1)))

@[simp]
theorem LeafData.ofFun_get {α} {s} (tree : LeafData α s) :
    LeafData.ofFun s (fun idx => tree.get idx) = tree

omit [NeZero ℓ] in
lemma fin_ℓ_steps_lt_ℓ_add_R (i : Fin ℓ) (steps : ℕ) (h : i.val + steps ≤ ℓ)
    : i.val + steps < ℓ + 𝓡

@[simp] lemma mod_two_eq_zero (m : ℤ) : m % 2 = ( - m) % 2

theorem is_unit_iff_deg_0 {R : Type*} [Field R] {p : R[X]} : p.degree = 0 ↔ IsUnit p
</all_available_lemmas>

<local_ctx>
import Mathlib.Algebra.Tropical.Basic

import Mathlib.RingTheory.Polynomial.Basic

import ArkLib.Data.Array.Lemmas

open Polynomial

@[reducible, inline, specialize]
def UniPoly (R : Type*) := Array R

def Polynomial.toImpl {R : Type*} [Semiring R] (p : R[X]) : UniPoly R :=
  match p.degree with
  | ⊥ => #[]
  | some d  => .ofFn (fun i : Fin (d + 1) => p.coeff i)

namespace UniPoly

@[reducible]
def mk {R : Type*} (coeffs : Array R) : UniPoly R := coeffs

variable {R : Type*} [Ring R] [BEq R]

variable {Q : Type*} [Ring Q]

@[reducible]
def coeff (p : UniPoly Q) (i : ℕ) : Q := p.getD i 0

def last_nonzero (p : UniPoly R) : Option (Fin p.size) :=
  p.findIdxRev? (· != 0)

def trim (p : UniPoly R) : UniPoly R :=
  match p.last_nonzero with
  | none => #[]
  | some i => p.extract 0 (i.val + 1)

def degree (p : UniPoly R) : Nat :=
  match p.last_nonzero with
  | none => 0
  | some i => i.val + 1

namespace Trim

def last_nonzero_prop {p : UniPoly R} (k : Fin p.size) : Prop :=
  p[k] ≠ 0 ∧ (∀ j, (hj : j < p.size) → j > k → p[j] = 0)

def equiv (p q : UniPoly R) : Prop :=
  ∀ i, p.coeff i = q.coeff i

end Trim

def UniPolyC (R : Type*) [BEq R] [Ring R] := { p : UniPoly R // p.trim = p }

section Operations

variable {S : Type*}

def eval₂ [Semiring S] (f : R →+* S) (x : S) (p : UniPoly R) : S :=
  p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0

@[inline, specialize]
def add_raw (p q : UniPoly R) : UniPoly R :=
  let ⟨p', q'⟩ := Array.matchSize p q 0
  .mk (Array.zipWith (· + ·) p' q' )

variable (p q r : UniPoly R)

def canonical (p : UniPoly R) := p.trim = p

end Operations

namespace OperationsC

variable {R : Type*} [Ring R] [BEq R] [LawfulBEq R]

variable (p q r : UniPolyC R)

end OperationsC

section ToPoly

noncomputable def toPoly (p : UniPoly R) : Polynomial R :=
  p.eval₂ Polynomial.C Polynomial.X

noncomputable def UniPolyC.toPoly (p : UniPolyC R) : Polynomial R := p.val.toPoly

alias ofPoly := Polynomial.toImpl
</local_ctx>

<target_theorem>
lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : UniPolyC R) : p.toPoly.toImpl = p :=
</target_theorem>

