Theorem: BabySNARK.is_sound (FormalSnarksProject/SNARKs/BabySnark.lean)

State before:
case intro.intro.intro
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
hH_01 hH_02 hH_12 hH_20 hH_21 hH_22 hV_01 hV_02 hV_12 hV_20 hV_21 hV_22 hB_01 hB_02 hB_12 hB_20 hB_21 hB_22 hI_01 hI_02 hI_12 :
  True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
      (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))) =
    0
hI_21 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
        (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
          -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                  (List.finRange n_wit)).sum *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ))) +
      -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    0
hI_22 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) =
    0
hII_00 hII_01 hII_02 : True
hII_10 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_12 : True
hII_20 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hII_21 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) +
      (-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    0
hII_22 : -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ)
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ)
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    sum_B_1_τ_pow
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hII_11 : -sum_V_2_τ_pow = 0
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      (-(sum_V_1_τ_pow *
                  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                      (List.finRange n_wit)).sum) +
              -((List.map
                      (fun x =>
                        Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                      (List.finRange n_wit)).sum) +
            (-(sum_V_1_τ_pow * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
              -((List.map
                      (fun x =>
                        Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))) +
          (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * sum_V_2_τ_pow) +
            -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                    (List.finRange n_wit)).sum *
                sum_V_2_τ_pow)) +
        (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum)) =
    0
hI_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) *
        (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      (-(sum_V_1_τ_pow * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
            -((List.map
                    (fun x =>
                      Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
          -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) * sum_V_2_τ_pow) +
        Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) =
    0
hV_00 : sum_V_1_τ_pow = sum_V_2_τ_pow
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hI_00 :
  sum_H_1_τ_pow * (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      ((List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (-(sum_V_1_τ_pow * sum_V_2_τ_pow) +
            -((List.map
                    (fun x =>
                      Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                sum_V_2_τ_pow) +
          (sum_V_1_τ_pow *
              (List.map
                  (fun x =>
                    -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x))
                  (List.finRange n_var)).sum +
            (List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map
                  (fun x =>
                    -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x))
                  (List.finRange n_var)).sum))) =
    0
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
integral_domain_tactic
State after:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    -(-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hII_22 : Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 : Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = 0
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 : Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -(-((List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                  (List.finRange n_wit)).sum) +
          -((List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum))
hV_00 : sum_V_1_τ_pow = 0
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum)
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
hI_11 : Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ) = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum

case intro.intro.intro.inr
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
ht : (List.map (fun x => Polynomial.C (Polynomial.coeff 0 ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = 0
ht0 : Polynomial.Monic 0
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    -(-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hII_22 : Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ)
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 : Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hI_10 :
  -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum)
hV_00 : sum_V_1_τ_pow = 0
hI_00 :
  (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
      (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum =
    -((List.map
            (fun x =>
              Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                Polynomial.X ^ ↑x)
            (List.finRange n_var)).sum *
        (List.map
            (fun x =>
              -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x))
            (List.finRange n_var)).sum)
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
hI_11 : t = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    0

State before:
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
eqnI :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G1 stmt ChecksIdx.CheckI pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
                          BabySNARK.ListSRSElements_G1).sum)
                  BabySNARK.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G1 stmt ChecksIdx.CheckI pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G1 SRS_elem)
                  BabySNARK.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G2 stmt ChecksIdx.CheckI pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
                          BabySNARK.ListSRSElements_G2).sum)
                  BabySNARK.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G2 stmt ChecksIdx.CheckI pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G2 SRS_elem)
                  BabySNARK.ListSRSElements_G2).sum))
        (BabySNARK.ListPairings ChecksIdx.CheckI)).sum =
    0
eqnII :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G1 stmt ChecksIdx.CheckII pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
                          BabySNARK.ListSRSElements_G1).sum)
                  BabySNARK.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G1 stmt ChecksIdx.CheckII pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G1 SRS_elem)
                  BabySNARK.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G2 stmt ChecksIdx.CheckII pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
                          BabySNARK.ListSRSElements_G2).sum)
                  BabySNARK.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G2 stmt ChecksIdx.CheckII pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G2 SRS_elem)
                  BabySNARK.ListSRSElements_G2).sum))
        (BabySNARK.ListPairings ChecksIdx.CheckII)).sum =
    0
eqnH :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.H SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.H SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
eqnV :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.V SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.V SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
eqnB :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.B SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.B SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
this :
  ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
⊢ (((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
              (List.map
                  (fun i =>
                    Polynomial.C ((fun prover i => prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) prover i) * u_wit i)
                  (List.finRange n_wit)).sum) ^
            2 -
          1).modByMonic
      t =
    0
Tactic:
rw [this]
State after:
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
eqnI :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G1 stmt ChecksIdx.CheckI pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
                          BabySNARK.ListSRSElements_G1).sum)
                  BabySNARK.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G1 stmt ChecksIdx.CheckI pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G1 SRS_elem)
                  BabySNARK.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G2 stmt ChecksIdx.CheckI pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
                          BabySNARK.ListSRSElements_G2).sum)
                  BabySNARK.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G2 stmt ChecksIdx.CheckI pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G2 SRS_elem)
                  BabySNARK.ListSRSElements_G2).sum))
        (BabySNARK.ListPairings ChecksIdx.CheckI)).sum =
    0
eqnII :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G1 stmt ChecksIdx.CheckII pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.1 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
                          BabySNARK.ListSRSElements_G1).sum)
                  BabySNARK.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G1 stmt ChecksIdx.CheckII pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G1 SRS_elem)
                  BabySNARK.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    C (BabySNARK.verificationPairingProof_G2 stmt ChecksIdx.CheckII pairing pf_elem) *
                      (List.map (fun SRS_elem => C (prover.2 pf_elem SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
                          BabySNARK.ListSRSElements_G2).sum)
                  BabySNARK.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    C (BabySNARK.verificationPairingSRS_G2 stmt ChecksIdx.CheckII pairing SRS_elem) *
                      BabySNARK.SRSElementValue_G2 SRS_elem)
                  BabySNARK.ListSRSElements_G2).sum))
        (BabySNARK.ListPairings ChecksIdx.CheckII)).sum =
    0
eqnH :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.H SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.H SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
eqnV :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.V SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.V SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
eqnB :
  (List.map (fun SRS_elem => C (prover.1 Proof_Idx.B SRS_elem) * BabySNARK.SRSElementValue_G1 SRS_elem)
        BabySNARK.ListSRSElements_G1).sum =
    (List.map (fun SRS_elem => C (prover.2 Proof_Idx.B SRS_elem) * BabySNARK.SRSElementValue_G2 SRS_elem)
        BabySNARK.ListSRSElements_G2).sum
this :
  ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
⊢ (t *
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum).modByMonic
      t =
    0

State before:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    -(-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hII_22 : Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 : Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = 0
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 : Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -(-((List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                  (List.finRange n_wit)).sum) +
          -((List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum))
hV_00 : sum_V_1_τ_pow = 0
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum)
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
hI_11 : Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ) = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
simp [ht, Polynomial.Monic.ne_zero ht0] at *
State after:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hV_00 : sum_V_1_τ_pow = 0
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
ht : True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_22 : prover.2 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hH_11 : prover.1 Proof_Idx.H SRS_Elements_Idx.γβ = 0
hV_11 : prover.1 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
        -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
      ((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) +
      -((List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum *
          (List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum)
hI_11 : prover.2 Proof_Idx.H SRS_Elements_Idx.γβ = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum

State before:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hV_00 : sum_V_1_τ_pow = 0
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
ht : True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_22 : prover.2 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hH_11 : prover.1 Proof_Idx.H SRS_Elements_Idx.γβ = 0
hV_11 : prover.1 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
        -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
      ((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) +
      -((List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum *
          (List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum)
hI_11 : prover.2 Proof_Idx.H SRS_Elements_Idx.γβ = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
rw [pow_two]
State after:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hV_00 : sum_V_1_τ_pow = 0
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
ht : True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_22 : prover.2 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hH_11 : prover.1 Proof_Idx.H SRS_Elements_Idx.γβ = 0
hV_11 : prover.1 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
        -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
      ((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) +
      -((List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum *
          (List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum)
hI_11 : prover.2 Proof_Idx.H SRS_Elements_Idx.γβ = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) *
        ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum

State before:
case intro.intro.intro.inl
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hV_00 : sum_V_1_τ_pow = 0
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
ht : True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_22 : prover.2 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hH_11 : prover.1 Proof_Idx.H SRS_Elements_Idx.γβ = 0
hV_11 : prover.1 Proof_Idx.V SRS_Elements_Idx.γβ = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) * t +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum *
        t =
    -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
        -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum) +
      ((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        (List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)
hI_00 :
  sum_H_2_τ_pow * t + t * t =
    -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) +
      -((List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum *
          (List.map (fun x => if ↑x = 0 then Polynomial.X ^ ↑x else 0) (List.finRange n_var)).sum)
hI_11 : prover.2 Proof_Idx.H SRS_Elements_Idx.γβ = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) *
        ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
sorry
State after:
no goals

State before:
case intro.intro.intro.inr
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
sum_B_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_B_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_V_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_1_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
sum_H_2_τ_pow : Polynomial F :=
  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
      (List.finRange n_var)).sum
ht : (List.map (fun x => Polynomial.C (Polynomial.coeff 0 ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = 0
ht0 : Polynomial.Monic 0
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) =
    -(-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))
hII_10 : sum_B_1_τ_pow = 0
hII_20 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hII_21 :
  Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hII_22 : Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ)
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 : Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
            (List.finRange n_wit)).sum +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) =
    -(-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 : sum_V_2_τ_pow = 0
hI_10 :
  -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum) +
      -((List.map
              (fun x =>
                Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum)
hV_00 : sum_V_1_τ_pow = 0
hI_00 :
  (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
      (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum =
    -((List.map
            (fun x =>
              Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                Polynomial.X ^ ↑x)
            (List.finRange n_var)).sum *
        (List.map
            (fun x =>
              -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                  Polynomial.X ^ ↑x))
            (List.finRange n_var)).sum)
hH_00 : sum_H_1_τ_pow = sum_H_2_τ_pow
hI_11 : t = 0
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    0
Tactic:
simp [ht, Polynomial.Monic.ne_zero ht0] at *
State after:
no goals