Theorem: collapseToxicWaste_soundness
Proof state before:
case intro.a
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ (∀ (check_idx : 𝓟.EqualityChecks), 𝓟.check_poly agm stmt check_idx = 0) ∧
    ∀ pfs ∈ 𝓟.Identified_Proof_Elems, 𝓟.proof_element_G1_as_poly agm pfs.1 = 𝓟.proof_element_G2_as_poly agm pfs.2
Tactic:
constructor
Proof state after:
case intro.a.left
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ ∀ (check_idx : 𝓟.EqualityChecks), 𝓟.check_poly agm stmt check_idx = 0

case intro.a.right
F : Type
inst✝¹ : Field F
𝓟 : AGMProofSystemInstantiation F
d : ℕ
hd : 0 < d
inst✝ : DecidableEq 𝓟.Sample
sample_removed sample_target : 𝓟.Sample
sample_target_neq_removed : sample_target ≠ sample_removed
hdegree :
  ∀ (agm : AGMProofSystemInstantiation.Prover F 𝓟) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks),
    MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
hTypeIII : 𝓟.Identified_Proof_Elems = []
Wit : Type
relation : 𝓟.Stmt → Wit → Prop
extractor : AGMProofSystemInstantiation.Prover F 𝓟 → Wit
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
poly_checks_pass :
  ∀ (check_idx : (collapseToxicWaste 𝓟 d sample_removed sample_target).EqualityChecks),
    (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ ∀ pfs ∈ 𝓟.Identified_Proof_Elems, 𝓟.proof_element_G1_as_poly agm pfs.1 = 𝓟.proof_element_G2_as_poly agm pfs.2