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>
Nat in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Finset.Icc in Mathlib.Order.Interval.Finset.Defs
And in Init.Prelude
AddCommMonoid in Mathlib.Algebra.Group.Defs

...

instance : Fact (Nat.Prime scalarFieldSize) := ⟨ScalarField_is_prime⟩

lift_complete : ∀ outerStmtIn outerWitIn innerStmtOut innerWitOut,
    compat (outerStmtIn, outerWitIn) (innerStmtOut, innerWitOut) →
    (outerStmtIn, outerWitIn) ∈ outerRelIn →
    (innerStmtOut, innerWitOut) ∈ innerRelOut →
    (lens.stmt.lift outerStmtIn innerStmtOut,
    lens.wit.lift (outerStmtIn, outerWitIn) (innerStmtOut, innerWitOut)) ∈ outerRelOut

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

def Verifier.liftContext
    (lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
    (V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec) :
      Verifier oSpec OuterStmtIn OuterStmtOut pSpec where
  verify := fun stmtIn transcript => do
    let innerStmtIn := lens.proj stmtIn
    let innerStmtOut ← V.verify innerStmtIn transcript
    return lens.lift stmtIn innerStmtOut

OracleSpec.QueryLog.inl in VCVio.OracleComp.QueryTracking.Structures

@[simp]
abbrev OracleStatement.AfterSecondSumcheck : R1CS.MatrixIdx ⊕ R1CS.MatrixIdx ⊕ Fin 1 → Type :=
  Sum.elim (EvalClaim R) (OracleStatement.AfterFirstSumcheck R pp)

example : !d⟨!v[]⟩[] = (Fin.dempty : (i : Fin 0) → !v[] i) := rfl

noncomputable def foldf (S : Finset ι) (φ : ι ↪ F)
  {k : ℕ} [Neg (indexPowT S φ k)] (y : indexPowT S φ (k + 1))
  (f : indexPowT S φ k → F) (α : F) : F :=
  let xPow := extract_x S φ k y
  let fx := f xPow
  let f_negx := f (-xPow)
  (fx + f_negx) / 2 + α * ((fx - f_negx) / (2 * (xPow.val : F)))

def range (n : ℕ) : Fin n → ℕ := fun i => i

noncomputable def H
  (δ : ℚ) (x₀ : F)
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  : F[Z][X] := (exists_factors_with_large_common_root_set k δ x₀ h_gs).choose_spec.choose

def two : ChurchNat α := succ one

@[reducible]
def OracleStatement (ϑ : ℕ) [NeZero ϑ] (i : Fin (ℓ + 1)) :
    Fin (toOutCodewordsCount ℓ ϑ (i:=i)) → Type := fun j =>
  by admit /- proof elided -/

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

@[reducible]
def VectorIOP
    (Statement : Type) {ιₛ : Type} (OStatement : ιₛ → Type) (Witness : Type)
    (vPSpec : ProtocolSpec.VectorSpec n) (A : Type)
    [∀ i, OracleInterface (OStatement i)] :=
  OracleProof []ₒ Statement OStatement Witness (vPSpec.toProtocolSpec A)

abbrev ScalarField := ZMod scalarFieldSize

private def Fi (B : Finset (Fin n → F)) (i : Fin n) (α : F) : Finset (Fin n → F) :=
  { x | x ∈ B ∧ x i = α }

def liftRightNil {ι : Type} {σ : Type} (oSpec : OracleSpec ι) :
    SimOracle.Stateful (oSpec ++ₒ []ₒ) oSpec σ where impl
  | query (.inl i) q => fun s ↦ do return ⟨← query i q, s⟩

@[reducible]
def index (op : MemoryWrite ι α) := op.1

@[inline, specialize]
def add {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p q : QuotientUniPoly R) : QuotientUniPoly R :=
  Quotient.lift₂ add_descending add_descends p q

let sumcheckFinalCheck : Prop := stmt.sumcheck_target = eqTilde r stmt.challenges * c
    let finalFoldingProp := finalNonDoomedFoldingProp 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (h_le := by admit /- proof elided -/
        ) (input := ⟨stmtOut, oStmt⟩)

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

def Function.extendDomain {α β : Type*} [DecidableEq α] [Zero β] {s : Finset α}
    (f : (x : α) → (x ∈ s) → β) : α → β :=
  fun x ↦ if hx : x ∈ s then f x hx else 0

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 δ

BitVec.xor in Init.Data.BitVec.Basic

instance : SMul R (UniPoly R) := ⟨UniPoly.smul⟩

output := fun _ => do 
    pure (⟨true, fun _ => ()⟩, ())

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

def powMod (a b m : ℕ) : ℕ := Id.run do
  let mut x := a
  let mut n := b
  let mut res := 1

def FullData.EquivIndexFun {α : Type} (s : Skeleton) :
    FullData α s ≃ (SkeletonNodeIndex s → α) where
  toFun := fun tree idx => tree.get idx
  invFun := fun f => FullData.ofFun s f
  left_inv := by admit /- proof elided -/

instance instTestLensComplete : testLens.IsComplete
      outerRelIn_Test innerRelIn_Test outerRelOut_Test innerRelOut_Test
      (fun ⟨⟨p, q, _⟩, _⟩ ⟨⟨f, _⟩, _⟩ => p * q = f) where
  proj_complete := fun ⟨p, q, t⟩ () hRelIn => by admit /- proof elided -/

@[reducible]
def duplexSpongeChallengeOracle (StartType : Type) (U : Type) [SpongeUnit U] [SpongeSize] :
    OracleSpec (Unit ⊕ PermuteDir) :=
  (StartType →ₒ Vector U SpongeSize.C) ++ₒ permutationOracle (CanonicalSpongeState U)

instance instDCast₂ : DCast₂ Nat ProtocolSpec (fun _ pSpec => FullTranscript pSpec) where
  dcast₂ h h' T := FullTranscript.cast h h' T
  dcast₂_id := cast_id

let columnSums := transposedMatrix.map (fun col => col.foldl (· + ·) 0)

Array.reverse in Init.Data.Array.Basic

def take_snoc_oracle (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) :
    (j : Fin (toOutCodewordsCount ℓ ϑ i.castSucc)) → 
      OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j
    := fun j => snoc_oracle 𝔽q β oStmtIn newOracleFn ⟨j, by admit /- proof elided -/
    ⟩

def add_descending (p q : UniPoly R) : QuotientUniPoly R :=
  Quotient.mk _ (add p q)

@[inline, specialize]
def Reduction.runWithLog (stmt : StmtIn) (wit : WitIn)
    (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) :
      OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
        (((FullTranscript pSpec × StmtOut × WitOut) × StmtOut) ×
          QueryLog (oSpec ++ₒ [pSpec.Challenge]ₒ) × QueryLog oSpec) := do
  
  let ⟨proverResult, proveQueryLog⟩ ← reduction.prover.runWithLog stmt wit
  let ⟨stmtOut, verifyQueryLog⟩ ←
    liftM (simulateQ loggingOracle (reduction.verifier.run stmt proverResult.1)).run
  return ⟨⟨proverResult, stmtOut⟩, proveQueryLog, verifyQueryLog⟩

instance {n : ℕ} : OfNat (Cayley T) n where
  ofNat := ofNat n

alias E_col_pinv_p := collisionBwdFwd

def outputRelation : Set ((StmtOut R × (∀ i, OStmtOut R deg i)) × Unit) :=
  { ⟨⟨⟨newTarget, chal⟩, oStmt⟩, _⟩ | (oStmt ()).1.eval chal = newTarget }

def subNat (c : AssocNat) : Nat → AssocNat
| 0            => c 
| Nat.succ k   => pred (subNat c k)

instance : OracleInterface (Witness R pp) where
  Query := Fin pp.ℓ_w → R
  Response := R
  answer := fun 𝕨 evalPoint => (MLE (𝕨 ∘ finFunctionFinEquiv)) ⸨evalPoint⸩

@[inline]
def zero [Zero R] : MlPolyEval R n := Vector.replicate (2 ^ n) 0

alias NonInteractive := ProverOnly

HasSum in Mathlib.Topology.Algebra.InfiniteSum.Defs

instance instDCastPSigmaPSigma :
    DCast ((a : α) ×' (b : β a) ×' γ a b) (fun a => δ a.1 a.2.1 a.2.2) where
  dcast hc d := dcast₃ (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  ) d
  dcast_id := by admit /- proof elided -/

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

def seqComposeChallengeEquiv {m : ℕ} {n : Fin m → ℕ} (pSpec : ∀ i, ProtocolSpec (n i)) :
    (i : Fin m) × (pSpec i).ChallengeIdx ≃ (seqCompose pSpec).ChallengeIdx where
  
  toFun := fun ⟨i, j⟩ => sigmaChallengeIdxToSeqCompose i j
  invFun := seqComposeChallengeIdxToSigma
  left_inv := by admit /- proof elided -/

state.zipWith (fun s d => sumAll + d * s) params.internalDiagVectors

instance {ι : Type u} (v : ι → Type v) [O : ∀ i, OracleInterface (v i)]
    [h : ∀ i, DecidableEq (Query (v i))]
    [h' : ∀ i, DecidableEq (Response (v i))] :
    [v]ₒ.DecidableEq where
  domain_decidableEq' := h
  range_decidableEq' := h'

alias E_inv := inv

@[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)))

def isZero {α : Type} (n : ChurchNat α) : ChurchBool α :=
  fun x y => n (fun _ => y) x

def soundness
    (langIn : Set (StmtIn × ∀ i, OStmtIn i))
    (langOut : Set (StmtOut × ∀ i, OStmtOut i))
    (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec)
    (soundnessError : ℝ≥0) : Prop :=
  verifier.toVerifier.soundness init impl langIn langOut soundnessError

@[reducible, simp]
def OracleStatement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
    {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)]
    {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)]
    {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)]
    {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)]
    (outerLangIn : Set (OuterStmtIn × (∀ i, OuterOStmtIn i)))
    (outerLangOut : Set (OuterStmtOut × (∀ i, OuterOStmtOut i)))
    (innerLangIn : Set (InnerStmtIn × (∀ i, InnerOStmtIn i)))
    (innerLangOut : Set (InnerStmtOut × (∀ i, InnerOStmtOut i)))
    (compatStmt :
      OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → Prop)
    (lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                                    OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) :=
  Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut compatStmt lens

PrvState := commitPrvState 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i

noncomputable def commitOracleProver (i : Fin ℓ) :
  OracleProver (oSpec := []ₒ)
    
    (StmtIn := Statement (L := L) Context i.succ)
    (OStmtIn := OracleStatement 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc)
    (WitIn := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ := ℓ) i.succ)
    (StmtOut := Statement (L := L) Context i.succ)
    (OStmtOut := OracleStatement 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
    (WitOut := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ := ℓ) i.succ)
    (pSpec := pSpecCommit 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) where

instance [Repr α] (αs : List Type) [HListRepr (HList αs)] : HListRepr (HList (α :: αs)) where
  repr
  | HList.cons x xs =>
    match xs with
    | HList.nil => reprPrec x 0
    | HList.cons _ _ => reprPrec x 0 ++ ", " ++ HListRepr.repr xs

@[inline] def div [Zero T] [DecidableEq T] [ToNat T]
    (dividend divisor : Cayley T) : Cayley T :=
  
  letI fuel := (↑dividend : Nat) + 1
  divNat dividend divisor fuel

MonoidHom in Mathlib.Algebra.Group.Hom.Defs

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

@[reducible, inline]
def OracleProver {ι : Type} (oSpec : OracleSpec ι)
    (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (WitIn : Type)
    (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) (WitOut : Type)
    {n : ℕ} (pSpec : ProtocolSpec n) :=
  Prover oSpec (StmtIn × (∀ i, OStmtIn i)) WitIn (StmtOut × (∀ i, OStmtOut i)) WitOut pSpec

noncomputable def fold_k_set
  {S : Finset ι} {φ : ι ↪ F} {k m : ℕ}
  [∀ j : ℕ, Neg (indexPowT S φ j)]
  (set : Set ((indexPowT S φ 0) → F)) (αs : Fin k → F) (hk : k ≤ m): Set (indexPowT S φ k → F) :=
    { g | ∃ f ∈ set, g = fold_k f αs hk}

instance polyIrreducibleFact (n : ℕ) : Fact (Irreducible (poly n)) := ⟨polyIrreducible n⟩

Equiv.cast in Mathlib.Logic.Equiv.Defs

class VCVCompatible (α : Type*) extends Fintype α, Inhabited α where
  [type_decidableEq' : DecidableEq α]

Nontrivial in Mathlib.Logic.Nontrivial.Defs

def concat' {k : Fin n}
    (challenges : (i : Fin k) → (pSpec.dir (i.castLE (by admit /- proof elided -/
    )) = .V_to_P
      → pSpec.«Type» (i.castLE (by admit /- proof elided -/
      ))))
    (chal : (h : pSpec.dir k = .V_to_P) → pSpec.Challenge ⟨k, h⟩) :
    (i : Fin (k + 1)) → (pSpec.dir (i.castLE (by admit /- proof elided -/
    )) = .V_to_P) →
      pSpec.«Type» (i.castLE (by admit /- proof elided -/
      )) :=
  Fin.dconcat challenges chal

def findSumIdx (l : List α) (j : α) : ℕ := l.partialSum.findIdx (j < ·)

instance : IsEmpty (AssocFin AssocNat.zero) :=

[numFullRounds_ne_zero : NeZero numFullRounds]

@[reducible, simp]
def rbrKnowledgeSoundness (relation : Set (Statement × Bool))
    (verifier : Verifier oSpec Statement Bool pSpec)
    (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) : Prop :=
  verifier.rbrKnowledgeSoundness init impl relation acceptRejectRel rbrKnowledgeError

IO in Init.System.IO

def OracleSpec.FunctionType (spec : OracleSpec ι) := (i : ι) → spec.domain i → spec.range i

receiveChallenge | ⟨0, h⟩ => nomatch h

def map {α β : Fin n → Sort*} (f : (i : Fin n) → α i → β i) (a : (i : Fin n) → α i) :
    (i : Fin n) → β i := fun i => f i (a i)

def MLE (evals : (σ → Fin 2) → R) : MvPolynomial σ R :=
    ∑ x : σ → Fin 2, (eqPolynomial (x : σ → R)) * C (evals x)

def StateRestoration.Soundness (oSpec : OracleSpec ι) (StmtIn : Type)
    {n : ℕ} (pSpec : ProtocolSpec n) :=
  OracleComp (oSpec ++ₒ (srChallengeOracle StmtIn pSpec)) (StmtIn × pSpec.Messages)

NNRat.castRec in Mathlib.Algebra.Field.Defs

def ofMessagesChallenges (messages : MessagesUpTo k pSpec)
    (challenges : ChallengesUpTo k pSpec) : Transcript k pSpec :=
  fun i => match h : pSpec.dir (i.castLE (by admit /- proof elided -/
  )) with
  | Direction.P_to_V => messages ⟨i.castLE (by admit /- proof elided -/
  ), h⟩
  | Direction.V_to_P => challenges ⟨i.castLE (by admit /- proof elided -/
  ), h⟩

class Smooth
  (domain : ι ↪ F) where
    H : Subgroup (Units F)
    a           : Units F
    h_coset     : Finset.image domain Finset.univ
                  = (fun h : Units F => (a : F) * (h : F)) '' (H : Set (Units F))
    h_card_pow2 : ∃ k : ℕ, Fintype.card ι = 2 ^ k

instance [ProverFirst pSpec] [h : OracleInterface (pSpec.«Type» 0)] :
    ∀ i, OracleInterface (pSpec.Message i)
  | ⟨0, _⟩ => inferInstance

instance instAlgebraLiftConcreteBTField (k : ℕ)
  (prevBTFResult : ConcreteBTFStepResult (k := k)) :
  letI := mkFieldInstance (prevBTFResult.toConcreteBTFieldProps)
  letI := liftConcreteBTField (k:=k) prevBTFResult
  Algebra (ConcreteBTField k) (ConcreteBTField (k + 1)) :=
  letI := mkFieldInstance (prevBTFResult.toConcreteBTFieldProps)
  letI := liftConcreteBTField (k:=k) prevBTFResult
  RingHom.toAlgebra (R:=ConcreteBTField k) (S:=ConcreteBTField (k + 1))
    (i:=(concreteCanonicalEmbedding (k:=k)
      (prevBTFieldProps:=prevBTFResult.toConcreteBTFieldProps)
      (curBTFieldProps:=liftBTFieldProps (k:=k) (prevBTFResult:=prevBTFResult))))

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

def correlatedAgreement (C : Set (n → F)) (δ : ℝ≥0) {k : ℕ} (W : Fin k → n → F) : Prop :=
  ∃ S : Finset n, #(S) ≥ (1 - δ) * (Fintype.card n) ∧
    ∃ v : Fin k → n → F, ∀ i, v i ∈ C ∧ {j | v i j = W i j} = S

def StraightlineExtractor (oSpec : OracleSpec ι) (Data Commitment : Type) :=
  Commitment → QueryLog oSpec → Data

Polynomial.charP in Mathlib.Algebra.Polynomial.Coeff

def oracleReduction.firstChallenge :
    OracleReduction oSpec
      (Statement.AfterFirstMessage R pp) (OracleStatement.AfterFirstMessage R pp) (Witness R pp)
      (Statement.AfterFirstChallenge R pp) (OracleStatement.AfterFirstChallenge R pp) Unit
      ⟨!v[.V_to_P], !v[FirstChallenge R pp]⟩ :=
  sorry

instance : LT AssocNat where
  lt a b := a 0 < b 0

UInt32 in Init.Prelude

def sumExceptFirst (n : ℕ) (D : Fin n → Finset R) :
    MvPolynomial (Fin (n + 1)) R →ₗ[R] Polynomial R :=

Finsupp.mapRange in Mathlib.Data.Finsupp.Defs

Eq.mp in Init.Core

embed := ⟨fun j => by admit /- proof elided -/
  ⟩
  hEq := fun oracleIdx => by admit /- proof elided -/

noncomputable def generateOpening [Fact (Nat.Prime p)] (srs : Vector G₁ (n + 1))
    (coeffs : Fin (n + 1) → ZMod p) (z : ZMod p) : G₁ :=
  letI poly : degreeLT (ZMod p) (n + 1) := (degreeLTEquiv (ZMod p) (n + 1)).invFun coeffs
  letI q : degreeLT (ZMod p) (n + 1) :=
    ⟨Polynomial.div (poly.val - C (poly.val.eval z)) (X - C z), by admit /- proof elided -/
      ⟩
  commit srs (degreeLTEquiv (ZMod p) (n + 1) q)

def listOfCloseCodewordsRel (C : Code ι F) (y : ι → F) (r : ℝ) : ℕ :=
  Nat.card (relHammingBall C y r)

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

instance : HListString (HList []) where
  toString
  | HList.nil => ""

noncomputable def ElocPolyF (ωs f : Fin n → F) (p : Polynomial F) : Polynomial F :=
  ElocPoly n (liftF ωs) (liftF f) p

def SkeletonNodeIndex.rightChild {s : Skeleton} (idx : SkeletonNodeIndex s) :
    Option (SkeletonNodeIndex s) :=
  match idx with
  | SkeletonNodeIndex.ofLeaf => none
  | @SkeletonNodeIndex.ofInternal left right =>
    some (SkeletonNodeIndex.ofRight (getRootIndex right))
  | SkeletonNodeIndex.ofLeft idxLeft =>
    idxLeft.rightChild.map (SkeletonNodeIndex.ofLeft)
  | SkeletonNodeIndex.ofRight idxRight =>
    idxRight.rightChild.map (SkeletonNodeIndex.ofRight)

def intCast {k : ℕ} (n : ℤ) : ConcreteBTField k := if n % 2 = 0 then zero else one

def knowledgeStateFunction (hRel : ∀ stmtIn witOut,
      (mapStmt stmtIn, witOut) ∈ relOut → (stmtIn, mapWitInv stmtIn witOut) ∈ relIn) :
    (verifier oSpec mapStmt).KnowledgeStateFunction
      init impl relIn relOut (extractor mapWitInv) where
  toFun | ⟨0, _⟩ => fun stmtIn _ witIn => ⟨stmtIn, witIn⟩ ∈ relIn
  toFun_empty := fun stmtIn witIn => by admit /- proof elided -/

Polynomial.support in Mathlib.Algebra.Polynomial.Basic

List.getLast in Init.Data.List.Basic

instance {k : Fin (n + 1)} : Fintype (pSpec.MessageIdxUpTo k) :=
  inferInstanceAs (Fintype <| MessageIdx (pSpec.take k k.is_le))

def ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : 𝒪 H :=
  (ξ_regular x₀ R H).choose

def finIdxOfIfTrue [BEq α] [LawfulBEq α] (a : α) (l : List α) (h : a ∈ l) : Fin l.length :=
  ⟨List.idxOf' a l, by admit /- proof elided -/
  ⟩

@[ext]
structure Verifier {ι : Type} (oSpec : OracleSpec ι)
    (StmtIn StmtOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) where
  verify : StmtIn → FullTranscript pSpec → OracleComp oSpec StmtOut

Tactic.ReduceModChar.normIntNumeral in Mathlib.Tactic.ReduceModChar

class IsSecureWithGap
    (completeRelation : Set ((Statement × ∀ i, OStatement i) × Witness))
    (soundRelation : Set ((Statement × ∀ i, OStatement i) × Witness))
    (ε_rbr : vPSpec.ChallengeIdx → ℝ≥0)
    (vectorIOP : VectorIOP Statement OStatement Witness vPSpec A) where

def findFinIdx (p : α → Bool) (l : List α) : Fin (l.length + 1) :=
  ⟨List.findIdx' p l,
    Nat.lt_succ_of_le (by admit /- proof elided -/
    )⟩

instance instDCast₁₂ : DCast (β a) (γ a) where
  dcast hb c := dcast₂ (Eq.refl a) (by admit /- proof elided -/
  ) c
  dcast_id := by admit /- proof elided -/

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

def notFunction : Prop :=
  let ⟨baseTrace, _⟩ := removeRedundantEntryDS trace
  ∃ j : Fin baseTrace.length, ∃ stateIn _stateOut : CanonicalSpongeState U,
    baseTrace[j] = ⟨.inr .Fwd, stateIn, _stateOut⟩ ∧
      ∃ j' < j,
        ∃ stateOut1 : CanonicalSpongeState U, baseTrace[j'] = ⟨.inr .Fwd, stateIn, stateOut1⟩ ∨
        ∃ stateOut2 : CanonicalSpongeState U, baseTrace[j'] = ⟨.inr .Bwd, stateOut2, stateIn⟩

def fnOracle (spec : OracleSpec ι) (f : (i : ι) → spec.domain i → spec.range i) :
    SimOracle.Impl spec where
  impl | query i t => pure (f i t)

structure BacktrackSequence (trace : QueryLog (duplexSpongeChallengeOracle StmtIn U))
    (state : CanonicalSpongeState U) where
   
  stmt : StmtIn
   
  inputState : List (CanonicalSpongeState U)
   
  outputState : List (CanonicalSpongeState U)

noncomputable def liftBivariate {H : F[X][Y]} : F[X][Y] →+* 𝕃 H :=
  RingHom.comp (Ideal.Quotient.mk (Ideal.span {H_tilde H})) bivPolyHom

ringChar.charP in Mathlib.Algebra.CharP.Defs

def finUInt16Equiv : Fin (2 ^ 16) ≃ UInt16 where
  toFun := fun i => UInt16.ofFin i
  invFun := fun u => u.toFin
  left_inv _ := rfl
  right_inv _ := rfl

instance instDCast₂ : DCast₂ Nat ProtocolSpec (fun _ pSpec => MessageIdx pSpec) where
  dcast₂ h := MessageIdx.cast h
  dcast₂_id := cast_id

MvPolynomial.totalDegree in Mathlib.Algebra.MvPolynomial.Degrees

@[reducible, simp] def OStmtIn := fun _ : Fin 2 => OStatement

noncomputable def blockRelDistance
  (i k : ℕ) {S : Finset ι} {φ : ι ↪ F}
  [DecidableEq F] [DecidableEq ι] [Smooth φ]
  (f : (indexPowT S φ i) → F) (S' : Finset (indexPowT S φ i))
  (φ' : (indexPowT S φ i) ↪ F) [∀ i : ℕ, Fintype (indexPowT S φ i)]
  [h : DecidableBlockDisagreement i k f S' φ'] :
  (g : (indexPowT S φ i) → F) → ℝ≥0 :=
  fun g =>
    (disagreementSet i k f S' φ' g).card / (Fintype.card (indexPowT S φ k) : ℝ≥0)

Id.run in Init.Control.Id

def isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) :=
    instAlgebraTowerConcreteBTF.toIsScalarTower (i:=l) (j:=r) (k:=r+1)
    (h1:=by admit /- proof elided -/
    ) (h2:=by admit /- proof elided -/
    )

def powFiber (S : Finset ι) (φ : ι ↪ F) (k : ℕ) (y : indexPow S φ k) : Finset ι :=
  S.filter (fun x => (φ x) ^ k = y)

@[reducible]
def GroupEncodeOracle : OracleSpec Unit := fun _ => (ι, BitVec bitLength)

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

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

while d = 1 do
    x := g n c x
    y := g n c (g n c y)
    d := Nat.gcd (Int.natAbs (x - y)) n

def getLowBits (numLowBits : ℕ) (n : ℕ) := n &&& ((1 <<< numLowBits) - 1)

def eval₂AlgHom {A : Type w} {B : Type*} [CommSemiring A] [CommSemiring B] [PolynomialLike A P]
    [Algebra R A] [IsScalarTower R A P] [Algebra R B] (f : A →ₐ[R] B) (b : B) :
      P →ₐ[R] B where
  toRingHom := eval₂ f b
  commutes' := by admit /- proof elided -/

DivisionRing in Mathlib.Algebra.Field.Defs

def finIdxOf [BEq α] [LawfulBEq α] (a : α) (l : List α) : Fin (l.length + 1) :=
  ⟨List.idxOf' a l, Nat.lt_succ_of_le (by admit /- proof elided -/
  )⟩

@[inline] def zero : Cayley T :=
  ⟨id, by admit /- proof elided -/
  ⟩

@[inline]
def nsmul [SMul ℕ R] (m : ℕ) (p : MlPolyEval R n) : MlPolyEval R n := p.map (fun a => m • a)

@[inline] def ge [Zero T] [ToNat T] (a b : Cayley T) : Prop :=
  (a : Nat) ≥ (b : Nat)

@[simp]
def finRangeTo {k : ℕ} (i : ℕ) : Finset (Fin k) :=
  (List.take i (List.finRange k)).toFinset

def NestedList (n : ℕ) : Type := dfoldr' n (fun _ => Type) (fun _ T => List T) Nat

@[reducible, simp]
def relOut : Set ((StmtOut OStatement × ∀ i, OStmtOut OStatement i) × WitOut) :=
  { ⟨⟨q, oStmt⟩, ()⟩ | answer (oStmt 0) q = answer (oStmt 1) q }

Sum.isRight in Init.Data.Sum.Basic

Mathlib.Meta.NormNum.instAddMonoidWithOne in Mathlib.Tactic.NormNum.Result

example : !d⟨MyTypeVec⟩[(1 : ℕ), true, "hello"] =
  (!h[1, true, "hello"] : (i : Fin 3) → MyTypeVec i) := rfl

[width_ne_zero : NeZero width]

class ProverOnly (pSpec : ProtocolSpec 1) extends ProverFirst pSpec

instance : ∀ i, VCVCompatible ((pSpec Witness).Challenge i) | ⟨0, h⟩ => nomatch h

abbrev Size.n_x : ℕ := sz.n - sz.n_w

def SkeletonNodeIndex.depth {s : Skeleton} : SkeletonNodeIndex s → Nat
  | SkeletonNodeIndex.ofLeaf => 0
  | SkeletonNodeIndex.ofInternal => 0
  | SkeletonNodeIndex.ofLeft idxLeft => idxLeft.depth + 1
  | SkeletonNodeIndex.ofRight idxRight => idxRight.depth + 1

structure WireIndices (numWires : ℕ) where
   
  a : Fin numWires
   
  b : Fin numWires
   
  c : Fin numWires
deriving DecidableEq

OneHom in Mathlib.Algebra.Group.Hom.Defs

List.IsPrefix in Init.Data.List.Basic

Sum.inl in Init.Core
</all_available_defs>

<all_available_lemmas>
Nat.shiftRight_add in Init.Data.Nat.Bitwise.Basic
add_comm in Mathlib.Algebra.Group.Defs
Finset.Icc_self in Mathlib.Order.Interval.Finset.Basic
Finset.mem_Icc in Mathlib.Order.Interval.Finset.Defs
Finset.sum_bij' in Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_congr in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_mul in Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_singleton in Mathlib.Algebra.BigOperators.Group.Finset.Basic
mul_assoc in Mathlib.Algebra.Group.Defs
mul_comm in Mathlib.Algebra.Group.Defs
mul_one in Mathlib.Algebra.Group.Defs
pow_one in Mathlib.Algebra.Group.Defs
pow_zero in Mathlib.Algebra.Group.Defs
tsub_self in Mathlib.Algebra.Order.Sub.Basic
zero_add in Mathlib.Algebra.Group.Defs
zero_tsub in Mathlib.Algebra.Order.Sub.Basic

theorem sum_Icc_split {α : Type*} [AddCommMonoid α] (f : ℕ → α) (a b c : ℕ)
    (h₁ : a ≤ b) (h₂ : b ≤ c):
    ∑ i ∈ Finset.Icc a c, f i = ∑ i ∈ Finset.Icc a b, f i + ∑ i ∈ Finset.Icc (b+1) c, f i

omit [(i : ιₛ) → OracleInterface (OStatement i)] [OracleInterface Witness] in
theorem oracleProver_run {stmt : Statement} {oStmt : ∀ i, OStatement i} {wit : Witness} :
    (oracleProver oSpec Statement OStatement Witness).run ⟨stmt, oStmt⟩ wit =
      pure (fun i => by aesop, ⟨stmt, Sum.rec oStmt (fun _ => wit)⟩, ())

theorem snoc_ne_zero_iff : snoc s y ≠ 0 ↔ s ≠ 0 ∨ y ≠ 0

@[simp]
theorem verifier_rbrKnowledgeSoundness (hRel : ∀ stmtIn witOut,
      (mapStmt stmtIn, witOut) ∈ relOut → (stmtIn, mapWitInv stmtIn witOut) ∈ relIn) :
    (verifier oSpec mapStmt).rbrKnowledgeSoundness init impl relIn relOut 0

Nat.sub_mul in Init.Data.Nat.Basic

theorem BTField.Basis_cast_dest_eq {ι : Type*} (k n m : ℕ) (h_k_le_n : k ≤ n)
  (h_k_le_m : k ≤ m) (h_eq : m = n) :
  letI instLeftAlgebra := binaryAlgebraTower (l:=k) (r:=m) (h_le:=h_k_le_m)
  letI instRightAlgebra := binaryAlgebraTower (l:=k) (r:=n) (h_le:=h_k_le_n)
  @Basis ι (BTField k) (BTField m) _ _ instLeftAlgebra.toModule =
  @Basis ι (BTField k) (BTField n) _ _ instRightAlgebra.toModule

theorem sum_of_root_and_inverse_is_t1
    {curBTField : Type*} [Field curBTField]
    (u : curBTField) (t1 : curBTField) -- here t1 is already lifted to curBTField
    (specialElementNeZero : u ≠ 0)
    (eval_prevPoly_at_root : u ^ 2 + t1 * u + 1 = 0)
    (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y) :
    u + u⁻¹ = t1

theorem relayOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ)
    (hNCR : ¬ isCommitmentRound ℓ ϑ i) :
    OracleReduction.perfectCompleteness
      (pSpec := pSpecRelay)
      (relIn := foldStepRelOut (mp := mp) 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        (𝓑 := 𝓑) i)
      (relOut := roundRelation (mp := mp) 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        (𝓑 := 𝓑) i.succ)
      (oracleReduction := relayOracleReduction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        i hNCR)
      (init := init)
      (impl := impl)

@[simp] -- main lemma for bIdx: Fin (ℓ / ϑ - 1) bounds
lemma bIdx_mul_ϑ_add_x_lt_ℓ_sub_ϑ (bIdx : Fin (ℓ / ϑ - 1)) (x : ℕ) {hx : x ≤ ϑ} :
    ↑bIdx * ϑ + x ≤ ℓ - ϑ

@[simp]
lemma shift_left_empty :
    shift_left ∅ = ∅

theorem two_eq_zero_in_char2_field {F : Type*} [Field F]
  (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) : (2 : F) = 0

lemma towerRingHomForwardMap_Z (k : ℕ) :
  towerRingHomForwardMap k (Z k) = BinaryTower.Z k

@[simp]
lemma ofPolynomialAlgHom_toPolynomialAlgHom_X :
    ofPolynomialAlgHom (toPolynomialAlgHom (X : P)) = (Polynomial.X : R[X])

lemma towerRingHomForwardMap_split_eq (k : ℕ) (h_pos : k > 0) (x : ConcreteBTField k) :
  let p := split (k:=k) (h:=h_pos) x
  towerRingHomForwardMap (k:=k) (x) =
    BinaryTower.join_via_add_smul (k:=k) (h_pos:=h_pos)
      (hi_btf := towerRingHomForwardMap (k:=k-1) (p.1))
      (lo_btf := towerRingHomForwardMap (k:=k-1) (p.2))

theorem frobenius_identity_in_ground_field
  [Fact (Nat.Prime (ringChar Fq))] (f g : Fq[X]) :
    (f + g)^(Fintype.card Fq) = f^(Fintype.card Fq) + g^(Fintype.card Fq)

theorem seqCompose_completeness (hInit : init.neverFails)
    (rel : (i : Fin (m + 1)) → Set ((Stmt i × ∀ j, OStmt i j) × Wit i))
    (R : ∀ i, OracleReduction oSpec (Stmt i.castSucc) (OStmt i.castSucc) (Wit i.castSucc)
      (Stmt i.succ) (OStmt 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)) :
      (OracleReduction.seqCompose Stmt OStmt Wit R).completeness
        init impl (rel 0) (rel (Fin.last m)) (∑ i, completenessError i)

lemma E_and_Q_unique
  [NeZero n]
  {e k : ℕ}
  {E Q E' Q' : Polynomial F}
  {ωs f : Fin n → F}
  (he : 2 * e < n - k + 1)
  (hk_n : k ≤ n)
  (h_Q : Q ≠ 0)
  (h_Q' : Q' ≠ 0)
  (h_inj : Function.Injective ωs)
  (h_bw₁ : BerlekampWelchCondition e k ωs f E Q)
  (h_bw₂ : BerlekampWelchCondition e k ωs f E' Q')
: E * Q' = E' * Q

@[simp]
theorem Prover.run_of_prover_first [ProverOnly pSpec] (stmt : StmtIn) (wit : WitIn)
    (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) :
      prover.run stmt wit = (do
        let state := prover.input (stmt, wit)
        let ⟨msg, state⟩ ← liftComp (prover.sendMessage ⟨0, by simp⟩ state) _
        let ctxOut ← prover.output state
        return ((fun i => match i with | ⟨0, _⟩ => msg), ctxOut))

@[simp]
lemma coeffsOfPolynomial_polynomialOfCoeffs :
  coeffsOfPolynomial (polynomialOfCoeffs coeffs) = coeffs

theorem linear_form_of_elements_in_adjoined_commring
    {R : Type*} [CommRing R] (f : R[X]) (hf_deg : f.natDegree = 2)
    (hf_monic : Monic f) (c1 : AdjoinRoot f) :
    ∃ a b : R, c1 = (AdjoinRoot.of f) a * root f + (AdjoinRoot.of f) b

lemma linsolve_to_BerlekampWelch_condition {e k : ℕ}
  [NeZero n]
  {ωs f : Fin n → F}
  {v : Fin (2 * e + k) → F}
  (h_sol : linsolve (BerlekampWelchMatrix e k ωs f) (Rhs e ωs f) = some v)
  : BerlekampWelchCondition e k ωs f (solutionToE e k v) (solutionToQ e k v)

@[simp]
lemma Transcript.def_eq {k : Fin (n + 1)} {pSpec : ProtocolSpec n} :
    (pSpec.take k k.is_le).FullTranscript =
      ((i : Fin k) → pSpec.«Type» (Fin.castLE (by omega) i))

lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) :
  Matrix.vandermonde α = Matrix.subLeftFull (nonsquare n α) (Fin.castLE h)

@[simp]
theorem rightpad_apply_lt (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n)
    (h : i.val < m) : rightpad n a v i = v ⟨i.val, h⟩

theorem tail_init_eq_init_tail (s : Fin (n + 2) →₀ M) : tail (init s) = init (tail s)

theorem zero_mul {a : AssocNat} : 0 * a = 0

theorem add_zero {n : ℕ} (a : CNat (n + 1)) : a + 0 = a

theorem liftContext_processRound
    {lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
    {i : Fin n}
    {P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
    {resultRound : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
      (pSpec.Transcript i.castSucc × (P.liftContext lens).PrvState i.castSucc)} :
      (P.liftContext lens).processRound i resultRound
      = do
        let ⟨transcript, prvState, outerStmtIn, outerWitIn⟩ ← resultRound
        let ⟨newTranscript, newPrvState⟩ ← P.processRound i (do return ⟨transcript, prvState⟩)
        return ⟨newTranscript, ⟨newPrvState, outerStmtIn, outerWitIn⟩⟩

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

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

lemma towerRingHomForwardMap_join {k : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) :
  towerRingHomForwardMap (k:=k) (《 hi, lo 》) =
    BinaryTower.join_via_add_smul (k:=k) (h_pos:=by omega)
      (hi_btf := towerRingHomForwardMap (k:=k-1) hi)
      (lo_btf := towerRingHomForwardMap (k:=k-1) lo)

@[simp]
theorem minPoly_of_powerBasisSucc_generator (k : ℕ) :
  (minpoly (BTField k) (powerBasisSucc k).gen) = X^2 + (Z k) • X + 1

theorem eqPolynomial_zeroOne (r : σ → Fin 2) : (eqPolynomial r : MvPolynomial σ R) =
    ∏ i : σ, if r i = 0 then 1 - X i else X i

private lemma Monad.map_of_prod_fst_eq_prod_fst {m : Type u → Type v} [Monad m] [LawfulMonad m]
    {α β γ : Type u} (ma : m (α × β)) (c : γ) :
    (fun a => (c, a.1)) <$> ma = Prod.mk c <$> Prod.fst <$> ma

@[grind _=_]
theorem monomialXY_mul_monomialXY {n m p q : ℕ} {a b : F} :
    monomialXY n m a * monomialXY p q b = monomialXY (n + p) (m + q) (a * b)

theorem add_zero : @add α zero = @id (ChurchNat α)

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

lemma take_eq_take : transcript⟦:m⟧ = transcript.take m h

lemma concentration_bounds {deg : ℕ} {domain : ι ↪ F}
  {U : AffineSubspace F (ι → F)} [Nonempty U]
  (hdiv_pos : 0 < (divergence U (RScodeSet domain deg) : ℝ≥0))
  (hdiv_lt : (divergence U (RScodeSet domain deg) : ℝ≥0) < 1 - ReedSolomonCode.sqrtRate deg domain)
  : let δ' := divergence U (RScodeSet domain deg)
    Pr_{let u ← $ᵖ U}[Code.relHammingDistToCode u (RScodeSet domain deg) ≠ δ']
    ≤ errorBound δ' deg domain

theorem take_drop_addCases' (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
    Fin.addCases' (take m h v) (drop m h v) =
      fun i =>
        cast (by simp [append, addCases, castLE, Fin.cast]; intro hi; rw! [Nat.sub_add_cancel hi])
          (v (i.cast (by omega)))

@[simp]
lemma seqCompose_toVerifier {m : ℕ}
    (Stmt : Fin (m + 1) → Type)
    {ιₛ : Fin (m + 1) → Type} (OStmt : (i : Fin (m + 1)) → ιₛ i → Type)
    [Oₛ : ∀ i, ∀ j, OracleInterface (OStmt i j)]
    {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    [Oₘ : ∀ i, ∀ j, OracleInterface ((pSpec i).Message j)]
    (V : (i : Fin m) →
      OracleVerifier oSpec (Stmt i.castSucc) (OStmt i.castSucc) (Stmt i.succ) (OStmt i.succ)
        (pSpec i)) :
    (seqCompose Stmt OStmt V).toVerifier =
      Verifier.seqCompose (fun i => Stmt i × (∀ j, OStmt i j)) (fun i => (V i).toVerifier)

lemma eq_poly_deg_one {a b c d : F} {x₁ x₂ : F}
  (h1 : a + b * x₁ = c + d * x₁)
  (h2 : a + b * x₂ = c + d * x₂)
  (h1_2 : x₁ ≠ x₂) :
  Polynomial.C a + Polynomial.C b * Polynomial.X
    = Polynomial.C c + Polynomial.C d * Polynomial.X

@[simp]
theorem insertNth_removeNth : insertNth p y (removeNth p t) = update t p y

@[simp]
lemma solutionToE_and_Q_E_and_Q_to_a_solution :
  E_and_Q_to_a_solution e (solutionToE e k v) (solutionToQ e k v) = v

lemma toCodewordsCount_mul_ϑ_lt_ℓ (ℓ ϑ : ℕ) [NeZero ϑ] [NeZero ℓ] (i : Fin (ℓ + 1)) :
  ∀ j: Fin (toOutCodewordsCount ℓ ϑ i), j.val * ϑ < ℓ

theorem vcons_injective2 : Function.Injective2 (@vcons α n)

lemma erase_odd_def {s : Finset ℕ} :
    erase_odd s = s.filter Even

private lemma solutionToE_from_E
  (h_p_deg : p.natDegree < k)
  (h_dist : (Δ₀(f, p.eval ∘ ωs) : ℕ) ≤ e)
  : solutionToE e k (E_and_Q_to_a_solution e (E ωs f p e) (Q ωs f p e)) = E ωs f p e

theorem rename_eq_zero_of_injective {τ : Type*} {f : σ → τ} (hf : Function.Injective f)
    {p : MvPolynomial σ R} (h : rename f p = 0) : p = 0

@[simp, grind _=_]
theorem totalDegree_mul {f g : F[X][Y]} (hf : f ≠ 0) (hg : g ≠ 0) :
    totalDegree (f * g) = totalDegree f + totalDegree g

@[simp]
theorem vflatten_two_eq_append {n : Fin 2 → ℕ} {v : (i : Fin 2) → Fin (n i) → α} :
    vflatten v = vappend (v 0) (v 1)

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

lemma split_join_via_add_smul_eq_iff_split {k : ℕ} (h_pos : k > 0)
    (hi_btf lo_btf : ConcreteBTField (k - 1)) :
    split (k:=k) (h:=by omega) (x:=join_via_add_smul (k:=k) (h_pos:=h_pos) hi_btf lo_btf) =
      (hi_btf, lo_btf)

@[simp]
theorem happend_empty {α : Fin m → Sort u} {β : Fin 0 → Sort u} (v : (i : Fin m) → α i) :
    happend v !h⟨β⟩[] = v

private lemma sum_add_one {i : Fin (k + 1)} :
  ∑ j' ∈ finRangeTo (i.1 + 1), (s j').1 = (∑ j' ∈ finRangeTo i.1, (s j').1) + (s i).1

lemma principal_is_maximal_iff_irred {F : Type} [Field F] (f : F[X]) :
  (principalIdeal f).IsMaximal ↔ Irreducible f

@[simp]
theorem divide_by_2_mem {s : Finset ℕ} {d : ℕ} :
  d ∈ divide_by_2 s ↔ 2 * d ∈ s

@[simp]
theorem tail_vcons (a : α) (v : Fin n → α) : tail (a ::ᵛ v) = v

lemma roots_comp_X_sub_C (p : L[X]) (a : L) :
    (p.comp (X - C a)).roots = p.roots.map (fun r => r + a)

@[simp]
theorem embedSum_splitSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (vsum n)) :
    embedSum (splitSum k).1 (splitSum k).2 = k

lemma definingPoly_ne_zero {F : Type*} [Field F] [Fintype F] (s : F) [NeZero s] :
  (definingPoly s) ≠ 0

lemma bwm_of_pos [NeZero n] (h : j.1 < e) :
  BerlekampWelchMatrix e k ωs f i j = -Rhs j.1 ωs f i

@[to_additive]
theorem prod_Iic_succ (i : Fin n) :
    ∏ j ∈ Iic i.succ, v j = (∏ j ∈ Iic i.castSucc, v j) * v i.succ

theorem prime_23 : Nat.Prime 23

@[simp]
theorem vappend_vempty (v : Fin m → α) : vappend v !v[] = v

@[simp, grind =]
theorem monomialXY_eq_zero_iff {n m : ℕ} {a : F} : monomialXY n m a = 0 ↔ a = 0

theorem succ'_ne_zero (n : Nat) : succ' n ≠ 0

theorem polynomial_sum_ext.{u, u_1}
  {R : Type u}
  [Semiring R]
  {S : Type u_1}
  [AddCommMonoid S]
  {p : Polynomial R} {f g : ℕ → R → S}
  (h : ∀ i x, f i x = g i x)
  : p.sum f = p.sum g

lemma comm_map_smul_tmul (s s' : Right) (m : Left) :
    e (s • (s' ⊗ₜ[K] m)) = s • (e (s' ⊗ₜ[K] m))

lemma oodSampling_rs_le_bound
    {f : ι → F} {m s : ℕ} {φ : ι ↪ F} [Smooth φ]
    (δ l : ℝ≥0) (hδLe : δ ≤ 1)
    (C : Set (ι → F)) (hcode : C = smoothCode φ m ∧ listDecodable C δ l) :
    Pr_{ let rs ←$ᵖ (Fin s → F) }[ ∃ u u' : smoothCode φ m,
                        u.val ≠ u'.val ∧
                        u.val ∈ relHammingBall C f δ ∧
                        u'.val ∈ relHammingBall C f δ ∧
                        ∀ i : Fin s,
                          let ri := rs i
                          let rVec := fun j : Fin m => ri ^ (2^(j : ℕ))
                          (mVdecode u).eval (rVec) = (mVdecode u').eval (rVec)
                      ] ≤ ENNReal.ofReal (((l : ℝ)^2 / 2) * (((2^m : ℝ) / Fintype.card F)^s))

lemma getHighBits_no_shl_joinBits {n m : ℕ} (low : Fin (2 ^ n)) (high : Fin (2 ^ m)) :
  getHighBits_no_shl n (joinBits low high).val = high.val

theorem append_soundness (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁)
    (V₂ : OracleVerifier oSpec Stmt₂ OStmt₂ Stmt₃ OStmt₃ pSpec₂)
    {soundnessError₁ soundnessError₂ : ℝ≥0}
    (h₁ : V₁.soundness init impl lang₁ lang₂ soundnessError₁)
    (h₂ : V₂.soundness init impl lang₂ lang₃ soundnessError₂) :
      (V₁.append V₂).soundness init impl lang₁ lang₃ (soundnessError₁ + soundnessError₂)

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

theorem vconcat_right_injective (v : Fin n → α) : Function.Injective (vconcat v)

@[simp]
theorem vconcat_castSucc (v : Fin n → α) (a : α) (i : Fin n) :
    vconcat v a (castSucc i) = v i

theorem is_multilinear_iff_eq_evals_zeroOne {p : MvPolynomial σ R} :
    p ∈ R⦃≤ 1⦄[X σ] ↔ MLE p.toEvalsZeroOne = p

Pr_{let αs ←$ᵖ (Fin k → F)}[ -- for every function `f : ι → F` and
                      ∀ (f : (indexPowT S φ 0) → F),
                      -- `hδLe` : `δ ∈ (0, max_{j ∈ [0,k]} BStar(Cⱼ, parℓ = 2))`
                       (0 < δ ∧ δ < 1 - Finset.univ.sup
                        (fun j => params.BStar j (params.Gen_α j).C (params.Gen_α j).parℓ)) →

lemma one_le_sub_middle_of_pow2 {k : ℕ} (h_k : 1 ≤ k) : 1 ≤ 2 ^ k - 2 ^ (k - 1)

theorem hconcat_injective2 {α : Fin n → Sort u} {β : Sort u} :
    Function.Injective2 (@hconcat n α β)

lemma getBit_of_highBits_no_shl {n: ℕ} (numLowBits : ℕ) :
    ∀ k, getBit k (getHighBits_no_shl numLowBits n)
  = getBit (k + numLowBits) (n)

@[simp]
theorem drop_zero (v : (i : Fin n) → α i) : drop 0 n.zero_le v = v

theorem canonical_nonempty_iff [LawfulBEq R] {p : UniPoly R} (hp : p.size > 0) :
  p.trim = p ↔ p.last_nonzero = some ⟨ p.size - 1, Nat.pred_lt_self hp ⟩

theorem fconcat_injective2 {α : Fin n → A} {β : A} :
    Function.Injective2 (@fconcat A F n α β)

Nat.cast_ofNat in Mathlib.Data.Nat.Cast.Defs

@[simp] lemma natCast_eq {k : ℕ} (n : ℕ) : (↑n : ConcreteBTField k) = natCast n

lemma card_le_card_of_count_inj {α β : Type*} [DecidableEq α] [DecidableEq β]
    {s : Multiset α} {s' : Multiset β}
  {f : α → β} (inj : Function.Injective f) (h : ∀ a : α, s.count a ≤ s'.count (f a)) :
  s.card ≤ s'.card

theorem is_prime : Nat.Prime fieldSize

theorem unique_linear_decomposition_succ (k : ℕ) :
  ∀ (x : BTField (k+1)), ∃! (p : BTField k × BTField k),
    x = ⋘ p.1, p.2 ⋙

lemma forwardRange_tail (n : ℕ) (r : Fin n) (l : Fin (r.val + 1)) (h_l_gt_0 : l.val > 0) :
  (forwardRange n r ⟨l.val - 1, by omega⟩).tail = forwardRange n r l

theorem matchSize_comm (l₁ : List α) (l₂ : List α) (unit : α) :
    matchSize l₁ l₂ unit = (matchSize l₂ l₁ unit).swap

@[simp]
theorem simulateQ_bind_fst (oa : OracleComp spec α) (f : α → OracleComp spec β) :
    (do let a ← (simulateQ loggingOracle oa).run; f a.1) = oa >>= f

lemma split_smul_Z_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) :
  letI instAlgebra := ConcreteBTFieldAlgebra (l:=k-1) (r:=k) (h_le:=by omega)
  split h_pos (x • Z k) = (x, 0)

theorem seqCompose_soundness
    (lang : (i : Fin (m + 1)) → Set (Stmt i))
    (V : (i : Fin m) → Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i))
    (soundnessError : Fin m → ℝ≥0)
    (h : ∀ i, (V i).soundness init impl (lang i.castSucc) (lang i.succ) (soundnessError i)) :
      (Verifier.seqCompose Stmt V).soundness init impl (lang 0) (lang (Fin.last m))
        (∑ i, soundnessError i)

theorem sumcheckFoldOracleReduction_perfectCompleteness (hInit : init.neverFails) :
    OracleReduction.perfectCompleteness
      (pSpec := pSpecSumcheckFold 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
      (relIn := roundRelation (mp := mp) 𝔽q β (ϑ:=ϑ)
        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑) 0)
      (relOut := roundRelation (mp := mp) 𝔽q β (ϑ:=ϑ)
        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑) (Fin.last ℓ))
      (oracleReduction := sumcheckFoldOracleReduction 𝔽q β (ϑ:=ϑ)
        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑))
      (init := init)
      (impl := impl)

Fin.is_le' in Init.Data.Fin.Lemmas

@[simp]
theorem addCases'_left {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u}
    (left : (i : Fin m) → α i) (right : (j : Fin n) → β j) (i : Fin m) :
      addCases' left right (Fin.castAdd n i) = (Fin.append_left α β i) ▸ (left i)

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

@[simp] theorem rightpad_eq_self (l : List α) (n : Nat) (h : n ≤ l.length) :
    rightpad n unit l = l

beq_iff_eq in Init.Core

@[simp]
private lemma leadingCoeff_E : (E ωs f p e).leadingCoeff = 1

lemma rootMultiplicity_some_implies_root {F : Type} [CommSemiring F] [DecidableEq F]
  {x y : F} {f : F[X][Y]} (h : some 0 < (rootMultiplicity (f := f) x y))
  : (f.eval 0).eval 0 = 0

theorem MLE_degreeOf (evals : (σ → Fin 2) → R) (i : σ) : degreeOf i (MLE evals) ≤ 1

@[simp]
lemma seqCompose_succ {m : ℕ}
    (Stmt : Fin (m + 2) → Type)
    {ιₛ : Fin (m + 2) → Type} (OStmt : (i : Fin (m + 2)) → ιₛ i → Type)
    [Oₛ : ∀ i, ∀ j, OracleInterface (OStmt i j)]
    {n : Fin (m + 1) → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    [Oₘ : ∀ i, ∀ j, OracleInterface ((pSpec i).Message j)]
    (V : (i : Fin (m + 1)) → OracleVerifier oSpec
      (Stmt i.castSucc) (OStmt i.castSucc) (Stmt i.succ) (OStmt i.succ) (pSpec i)) :
    seqCompose Stmt OStmt V =
      append (V 0) (seqCompose (Stmt ∘ Fin.succ) (fun i => OStmt (Fin.succ i))
        (Oₛ := fun i => Oₛ (Fin.succ i)) (Oₘ := fun i => Oₘ (Fin.succ i))
          (fun i => V (Fin.succ i)))

@[simp]
theorem fappend_left {α : Fin m → A} {β : Fin n → A}
    (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) (i : Fin m) :
    fappend u v (castAdd n i) = cast (by simp [vappend_left]) (u i)

lemma add_two_pow_of_getBit_eq_zero_lt_two_pow {n m i : ℕ} (h_n: n < 2^m) (h_i: i < m)
  (h_getBit_at_i_eq_zero: getBit i n = 0) :
  n + 2^i < 2^m

@[grind =] theorem idxOf'_cons [BEq α] {a : α} {x : α} {xs : List α} :
    idxOf' a (x :: xs) = bif x == a then 0 else idxOf' a xs + 1

omit [NeZero ℓ] [NeZero r] [NeZero 𝓡] in
lemma ℓ_lt_r {h_ℓ_add_R_rate : ℓ + 𝓡 < r}
    : ℓ < r

theorem mul_two_eq_add {a : CNat 50} : a * 2 = a + a

lemma is_berlekamp_welch_solution_ext
  (h : ∀ i, (Matrix.mulVec (BerlekampWelchMatrix e k ωs f) v) i = -(f i) * (ωs i) ^ e)
  : IsBerlekampWelchSolution e k ωs f v

Finset.sup_lt_iff in Mathlib.Data.Finset.Lattice.Fold

lemma β_regular (R : F[X][X][Y])
                (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)]
                {D : ℕ} (hD : D ≥ Bivariate.totalDegree H) :
    ∀ t : ℕ, ∃ β : 𝒪 H, weight_Λ_over_𝒪 β ≤ (2 * t + 1) * Bivariate.natDegreeY R * D
</all_available_lemmas>

<local_ctx>
import ArkLib.Data.Fin.BigOperators

import Mathlib.Algebra.BigOperators.Ring.Finset

import Mathlib.Algebra.Order.Ring.Star

import Mathlib.Data.Nat.Bitwise

import Mathlib.Data.Nat.Digits.Defs

import Mathlib.Data.Finsupp.Basic

import Mathlib.Algebra.Order.BigOperators.Group.Finset

import Mathlib.Algebra.BigOperators.Fin

namespace Nat

def getBit (k n : Nat) : Nat := (n >>> k) &&& 1
</local_ctx>

<target_theorem>
theorem getBit_repr {ℓ : Nat} : ∀ j, j < 2^ℓ →
  j = ∑ k ∈ Finset.Icc 0 (ℓ-1), (getBit k j) * 2^k :=
</target_theorem>

