Theorem: changeExponent_soundness (FormalSnarksProject/Transformations/Transformations.lean)

State before:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
⊢ AGMProofSystemInstantiation.soundness F (changeExponent_G1 𝓟 sample d) Wit relation extractor
Tactic:
intros stmt agm checks_pass
State after:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
checks_pass : (changeExponent_G1 𝓟 sample d).verify agm stmt
⊢ relation stmt (extractor agm)

State before:
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
checks_pass : (changeExponent_G1 𝓟 sample d).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, _⟩
State after:
case intro
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)

State before:
case intro
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)
Tactic:
apply h_sound
State after:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt

State before:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound
State after:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt

State before:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (changeExponent_G1 𝓟 sample d).check_poly agm stmt check_idx = 0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (changeExponent_G1 𝓟 sample d).proof_element_G1_as_poly agm pfs.1 =
      (changeExponent_G1 𝓟 sample d).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
unfold AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.check_poly AGMProofSystemInstantiation.pairing_poly AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly at *
State after:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ (∀ (check_idx : 𝓟.EqualityChecks),
      (List.map
            (fun pairing =>
              ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                              𝓟.ListSRSElements_G1).sum)
                      𝓟.ListProof_G1).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum) *
                ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                              𝓟.ListSRSElements_G2).sum)
                      𝓟.ListProof_G2).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum))
            (𝓟.ListPairings check_idx)).sum =
        0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum

State before:
case intro.a
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ (∀ (check_idx : 𝓟.EqualityChecks),
      (List.map
            (fun pairing =>
              ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                              𝓟.ListSRSElements_G1).sum)
                      𝓟.ListProof_G1).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G1 SRS_elem)
                      𝓟.ListSRSElements_G1).sum) *
                ((List.map
                      (fun pf_elem =>
                        MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                          (List.map
                              (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                              𝓟.ListSRSElements_G2).sum)
                      𝓟.ListProof_G2).sum +
                  (List.map
                      (fun SRS_elem =>
                        MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                          𝓟.SRSElementValue_G2 SRS_elem)
                      𝓟.ListSRSElements_G2).sum))
            (𝓟.ListPairings check_idx)).sum =
        0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
      (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
            𝓟.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
            𝓟.ListSRSElements_G2).sum
Tactic:
constructor
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ (check_idx : 𝓟.EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0

case intro.a.right
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
          𝓟.ListSRSElements_G2).sum

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ (check_idx : 𝓟.EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G1 SRS_elem)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0
Tactic:
intro check_idx
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
replace poly_checks_pass := poly_checks_pass check_idx
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                  (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                  (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                  (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                  (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
        ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                  (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                  (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                  (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                  (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
        ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
unfold changeExponent_G1 at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G1
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G1
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G2
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G2
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum))
        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1, ListProof_G1 := 𝓟.ListProof_G1,
              Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
              Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
              verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListPairings
          check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G1
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G1
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G1
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingProof_G2
                          stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                              { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                                    ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                                    ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                                    SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                                    SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                                    ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2,
                                    ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
                                    Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                                    verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                                    verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                                    verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                                    verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                                    Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                                SRS_elem)
                          { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C
                        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                              ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                              EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings,
                              ListPairings := 𝓟.ListPairings, verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.verificationPairingSRS_G2
                          stmt check_idx pairing SRS_elem) *
                      { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                            ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                            ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                            SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                            SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                            ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                            EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                            verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                            verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                            verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                            verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                            Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.SRSElementValue_G2
                        SRS_elem)
                  { Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
                      ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
                      ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
                      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
                      SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1,
                      ListProof_G1 := 𝓟.ListProof_G1, Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2,
                      EqualityChecks := 𝓟.EqualityChecks, Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
                      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
                      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
                      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
                      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
                      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListSRSElements_G2).sum))
        ({ Stmt := 𝓟.Stmt, Sample := 𝓟.Sample, SRSElements_G1 := 𝓟.SRSElements_G1,
              ListSRSElements_G1 := 𝓟.ListSRSElements_G1, SRSElements_G2 := 𝓟.SRSElements_G2,
              ListSRSElements_G2 := 𝓟.ListSRSElements_G2,
              SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i,
              SRSElementValue_G2 := 𝓟.SRSElementValue_G2, Proof_G1 := 𝓟.Proof_G1, ListProof_G1 := 𝓟.ListProof_G1,
              Proof_G2 := 𝓟.Proof_G2, ListProof_G2 := 𝓟.ListProof_G2, EqualityChecks := 𝓟.EqualityChecks,
              Pairings := 𝓟.Pairings, ListPairings := 𝓟.ListPairings,
              verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1,
              verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2,
              verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1,
              verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2,
              Identified_Proof_Elems := 𝓟.Identified_Proof_Elems }.ListPairings
          check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
simp only at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 SRS_elem))
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      (MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 SRS_elem))
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem =>
                            MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                              (MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 SRS_elem))
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      (MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 SRS_elem))
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
simp only [
  mul_comm _ (MvPolynomial.X sample ^ d),
  mul_left_comm _ (MvPolynomial.X sample ^ d),
  mul_assoc (MvPolynomial.X sample ^ d),
  List.sum_map_mul_right, List.sum_map_mul_left,
  ←mul_add (MvPolynomial.X sample ^ d)] at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  MvPolynomial.X sample ^ d *
      (List.map
          (fun b =>
            ((List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx b b_1) *
                        (List.map (fun b => MvPolynomial.C (agm.1 b_1 b) * 𝓟.SRSElementValue_G1 b)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx b b_1) * 𝓟.SRSElementValue_G1 b_1)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx b pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx b SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  MvPolynomial.X sample ^ d *
      (List.map
          (fun b =>
            ((List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx b b_1) *
                        (List.map (fun b => MvPolynomial.C (agm.1 b_1 b) * 𝓟.SRSElementValue_G1 b)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx b b_1) * 𝓟.SRSElementValue_G1 b_1)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx b pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx b SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
rw [mul_eq_zero] at poly_checks_pass
State after:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  MvPolynomial.X sample ^ d = 0 ∨
    (List.map
          (fun b =>
            ((List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx b b_1) *
                        (List.map (fun b => MvPolynomial.C (agm.1 b_1 b) * 𝓟.SRSElementValue_G1 b)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx b b_1) * 𝓟.SRSElementValue_G1 b_1)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx b pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx b SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0

State before:
case intro.a.left
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  MvPolynomial.X sample ^ d = 0 ∨
    (List.map
          (fun b =>
            ((List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx b b_1) *
                        (List.map (fun b => MvPolynomial.C (agm.1 b_1 b) * 𝓟.SRSElementValue_G1 b)
                            𝓟.ListSRSElements_G1).sum)
                    𝓟.ListProof_G1).sum +
                (List.map
                    (fun b_1 =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx b b_1) * 𝓟.SRSElementValue_G1 b_1)
                    𝓟.ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx b pf_elem) *
                        (List.map
                            (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                            𝓟.ListSRSElements_G2).sum)
                    𝓟.ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx b SRS_elem) *
                        𝓟.SRSElementValue_G2 SRS_elem)
                    𝓟.ListSRSElements_G2).sum))
          (𝓟.ListPairings check_idx)).sum =
      0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
cases poly_checks_pass with
| inl poly_checks_pass =>
  exfalso
  simp only [pow_eq_zero_iff', MvPolynomial.X_ne_zero, ne_eq, false_and] at poly_checks_pass
| inr poly_checks_pass =>
  exact poly_checks_pass
State after:
no goals

State before:
case intro.a.left.inl
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass : MvPolynomial.X sample ^ d = 0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
exfalso
State after:
case intro.a.left.inl
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass : MvPolynomial.X sample ^ d = 0
⊢ False

State before:
case intro.a.left.inl
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass : MvPolynomial.X sample ^ d = 0
⊢ False
Tactic:
simp only [pow_eq_zero_iff', MvPolynomial.X_ne_zero, ne_eq, false_and] at poly_checks_pass
State after:
no goals

State before:
case intro.a.left.inr
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (List.map
        (fun b =>
          ((List.map
                  (fun b_1 =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx b b_1) *
                      (List.map (fun b => MvPolynomial.C (agm.1 b_1 b) * 𝓟.SRSElementValue_G1 b)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun b_1 =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx b b_1) * 𝓟.SRSElementValue_G1 b_1)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx b pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx b SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
⊢ (List.map
        (fun pairing =>
          ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.1 pf_elem SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
                          𝓟.ListSRSElements_G1).sum)
                  𝓟.ListProof_G1).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G1 SRS_elem)
                  𝓟.ListSRSElements_G1).sum) *
            ((List.map
                  (fun pf_elem =>
                    MvPolynomial.C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                      (List.map
                          (fun SRS_elem => MvPolynomial.C (agm.2 pf_elem SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
                          𝓟.ListSRSElements_G2).sum)
                  𝓟.ListProof_G2).sum +
              (List.map
                  (fun SRS_elem =>
                    MvPolynomial.C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                      𝓟.SRSElementValue_G2 SRS_elem)
                  𝓟.ListSRSElements_G2).sum))
        (𝓟.ListPairings check_idx)).sum =
    0
Tactic:
exact poly_checks_pass
State after:
no goals

State before:
case intro.a.right
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
          𝓟.ListSRSElements_G2).sum
Tactic:
rw [hTypeIII]
State after:
case intro.a.right
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ pfs ∈ [],
    (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
          𝓟.ListSRSElements_G2).sum

State before:
case intro.a.right
F : Type
inst✝ : Field F
𝓟 : AGMProofSystemInstantiation F
sample : 𝓟.Sample
d : ℕ
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (changeExponent_G1 𝓟 sample d).Stmt
agm : AGMProofSystemInstantiation.Prover F (changeExponent_G1 𝓟 sample d)
poly_checks_pass :
  ∀ (check_idx : (changeExponent_G1 𝓟 sample d).EqualityChecks),
    (List.map
          (fun pairing =>
            ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G1 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.1 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G1).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum) *
              ((List.map
                    (fun pf_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingProof_G2 stmt check_idx pairing pf_elem) *
                        (List.map
                            (fun SRS_elem =>
                              MvPolynomial.C (agm.2 pf_elem SRS_elem) *
                                (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                            (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum)
                    (changeExponent_G1 𝓟 sample d).ListProof_G2).sum +
                (List.map
                    (fun SRS_elem =>
                      MvPolynomial.C
                          ((changeExponent_G1 𝓟 sample d).verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) *
                        (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
                    (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum))
          ((changeExponent_G1 𝓟 sample d).ListPairings check_idx)).sum =
      0
right✝ :
  ∀ pfs ∈ (changeExponent_G1 𝓟 sample d).Identified_Proof_Elems,
    (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.1 pfs.1 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G1 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G1).sum =
      (List.map
          (fun SRS_elem =>
            MvPolynomial.C (agm.2 pfs.2 SRS_elem) * (changeExponent_G1 𝓟 sample d).SRSElementValue_G2 SRS_elem)
          (changeExponent_G1 𝓟 sample d).ListSRSElements_G2).sum
⊢ ∀ pfs ∈ [],
    (List.map (fun SRS_elem => MvPolynomial.C (agm.1 pfs.1 SRS_elem) * 𝓟.SRSElementValue_G1 SRS_elem)
          𝓟.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => MvPolynomial.C (agm.2 pfs.2 SRS_elem) * 𝓟.SRSElementValue_G2 SRS_elem)
          𝓟.ListSRSElements_G2).sum
Tactic:
simp
State after:
no goals