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

State before:
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
⊢ AGMProofSystemInstantiation.soundness F (collapseToxicWaste 𝓟 d sample_removed sample_target) Wit relation extractor
Tactic:
intros stmt agm checks_pass
State after:
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).verify agm stmt
⊢ relation stmt (extractor agm)

State before:
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
stmt : (collapseToxicWaste 𝓟 d sample_removed sample_target).Stmt
agm : AGMProofSystemInstantiation.Prover F (collapseToxicWaste 𝓟 d sample_removed sample_target)
checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).verify agm stmt
⊢ relation stmt (extractor agm)
Tactic:
rcases checks_pass with ⟨poly_checks_pass, proof_elem_checks_pass⟩
State after:
case intro
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
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
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ relation stmt (extractor agm)

State before:
case intro
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
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
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).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
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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
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
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt

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
h_sound : AGMProofSystemInstantiation.soundness F 𝓟 Wit relation extractor
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
proof_elem_checks_pass :
  ∀ pfs ∈ (collapseToxicWaste 𝓟 d sample_removed sample_target).Identified_Proof_Elems,
    (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G1_as_poly agm pfs.1 =
      (collapseToxicWaste 𝓟 d sample_removed sample_target).proof_element_G2_as_poly agm pfs.2
⊢ 𝓟.verify agm stmt
Tactic:
clear h_sound proof_elem_checks_pass
State after:
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
⊢ 𝓟.verify agm stmt

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
⊢ 𝓟.verify agm stmt
Tactic:
unfold AGMProofSystemInstantiation.verify
State after:
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

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
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

State before:
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
Tactic:
intro check_idx
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

State before:
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
Tactic:
replace poly_checks_pass := poly_checks_pass check_idx
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ 𝓟.check_poly agm stmt check_idx = 0

State before:
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ 𝓟.check_poly agm stmt check_idx = 0
Tactic:
have checked_poly_is_transformed :
    AGMProofSystemInstantiation.check_poly (collapseToxicWaste 𝓟 d sample_removed sample_target) agm stmt check_idx
      =
    MvPolynomial.bind₁
      ((fun x => (if x = sample_removed then MvPolynomial.X (R := F) sample_target ^ d else MvPolynomial.X x)))
      (AGMProofSystemInstantiation.check_poly 𝓟 agm stmt check_idx) := by
  exact collapseToxicWaste_check_poly 𝓟 d sample_removed sample_target agm stmt check_idx
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ 𝓟.check_poly agm stmt check_idx = 0

State before:
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ 𝓟.check_poly agm stmt check_idx = 0
Tactic:
rw [checked_poly_is_transformed] at poly_checks_pass
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ 𝓟.check_poly agm stmt check_idx = 0

State before:
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ 𝓟.check_poly agm stmt check_idx = 0
Tactic:
apply MvPolynomial.bind₁_ite_pow_eq_zero_of (σ := 𝓟.Sample) (AGMProofSystemInstantiation.check_poly 𝓟 agm stmt check_idx) d hd sample_removed sample_target
State after:
case intro.a.left.hsa
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ sample_target ≠ sample_removed

case intro.a.left.h
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0

case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d

State before:
case intro.a.left.hsa
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ sample_target ≠ sample_removed

case intro.a.left.h
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0

case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
Tactic:
exact sample_target_neq_removed
State after:
case intro.a.left.h
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0

case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d

State before:
case intro.a.left.h
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0

case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
Tactic:
exact poly_checks_pass
State after:
case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d

State before:
case intro.a.left.hdegree
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass :
  (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx) =
    0
checked_poly_is_transformed :
  (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
⊢ MvPolynomial.degreeOf sample_target (𝓟.check_poly agm stmt check_idx) < d
Tactic:
exact hdegree agm stmt check_idx
State after:
no goals

State before:
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)
check_idx : 𝓟.EqualityChecks
poly_checks_pass : (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx = 0
⊢ (collapseToxicWaste 𝓟 d sample_removed sample_target).check_poly agm stmt check_idx =
    (MvPolynomial.bind₁ fun x => if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)
      (𝓟.check_poly agm stmt check_idx)
Tactic:
exact collapseToxicWaste_check_poly 𝓟 d sample_removed sample_target agm stmt check_idx
State after:
no goals

State before:
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
Tactic:
rw [hTypeIII]
State after:
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 ∈ [], 𝓟.proof_element_G1_as_poly agm pfs.1 = 𝓟.proof_element_G2_as_poly agm pfs.2

State before:
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 ∈ [], 𝓟.proof_element_G1_as_poly agm pfs.1 = 𝓟.proof_element_G2_as_poly agm pfs.2
Tactic:
simp
State after:
no goals