Theorem: collapseToxicWaste_soundness
Proof 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
Proof 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