internlm/Lean-Github huggingface dataset:
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)
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
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)
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
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 : (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
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)
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
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 : (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
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)
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
Theorem: collapseToxicWaste_soundness
Proof 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
Proof state after:
no goals
Theorem: collapseToxicWaste_soundness
Proof 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
Proof state after:
no goals
Theorem: collapseToxicWaste_soundness
Proof 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]
Proof 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
Theorem: collapseToxicWaste_soundness
Proof 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
Proof state after:
no goals
Theorem: List.prod_map_ite_eq
Proof state before:
case nil
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a : A
⊢ (map (fun x => if x = a then f x else g x) []).prod = (f a / g a) ^ count a [] * (map g []).prod
Tactic:
simp
Proof state after:
no goals
Theorem: List.prod_map_ite_eq
Proof state before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (map (fun x => if x = a then f x else g x) (x :: xs)).prod = (f a / g a) ^ count a (x :: xs) * (map g (x :: xs)).prod
Tactic:
simp only [map_cons, prod_cons, nodup_cons, ne_eq, mem_cons] at ih ⊢
Proof state after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x => if x = a then f x else g x) xs).prod =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * (map (fun x => if x = a then f x else g x) xs).prod =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Tactic:
rw [ih]
Proof state after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
ih : (map (fun x => if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Tactic:
clear ih
Proof state after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ count a (x :: xs) * (g x * (map g xs).prod)
Tactic:
rw [List.count_cons]
Proof state after:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case cons
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
by_cases hx : x = a
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)

case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
simp [hx, ite_true, pow_add]
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a * (f a ^ count a xs / g a ^ count a xs * (map g xs).prod) =
    f a ^ count a xs / g a ^ count a xs * (f a / g a) * (g a * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a * (f a ^ count a xs / g a ^ count a xs * (map g xs).prod) =
    f a ^ count a xs / g a ^ count a xs * (f a / g a) * (g a * (map g xs).prod)
Tactic:
simp only [mul_assoc, mul_comm (f a / g a) _, mul_comm (f a) _]
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a ^ count a xs / g a ^ count a xs * ((map g xs).prod * f a) =
    f a ^ count a xs / g a ^ count a xs * (g a * ((map g xs).prod * (f a / g a)))
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a ^ count a xs / g a ^ count a xs * ((map g xs).prod * f a) =
    f a ^ count a xs / g a ^ count a xs * (g a * ((map g xs).prod * (f a / g a)))
Tactic:
simp only [mul_right_inj]
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = g a * ((map g xs).prod * (f a / g a))
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = g a * ((map g xs).prod * (f a / g a))
Tactic:
simp only [mul_assoc, mul_comm (g a) _]
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = (map g xs).prod * (f a / g a * g a)
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ (map g xs).prod * f a = (map g xs).prod * (f a / g a * g a)
Tactic:
simp only [mul_right_inj]
Proof state after:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a = f a / g a * g a
Theorem: List.prod_map_ite_eq
Proof state before:
case pos
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : x = a
⊢ f a = f a / g a * g a
Tactic:
simp only [div_mul_cancel]
Proof state after:
no goals
Theorem: List.prod_map_ite_eq
Proof state before:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if a = x then 1 else 0) * (g x * (map g xs).prod)
Tactic:
simp only [hx, ite_false, ne_comm.mp hx, add_zero]
Proof state after:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ g x * ((f a / g a) ^ count a xs * (map g xs).prod) = (f a / g a) ^ count a xs * (g x * (map g xs).prod)
Theorem: List.prod_map_ite_eq
Proof state before:
case neg
F : Type
inst✝² : Field F
A B : Type
inst✝¹ : DecidableEq A
inst✝ : CommGroup B
f g : A → B
a x : A
xs : List A
hx : ¬x = a
⊢ g x * ((f a / g a) ^ count a xs * (map g xs).prod) = (f a / g a) ^ count a xs * (g x * (map g xs).prod)
Tactic:
simp only [mul_assoc, mul_comm (g x) _]
Proof state after:
no goals
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) = degreeOf j f
Tactic:
rw [Nat.eq_iff_le_and_ge]
Proof state after:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f ∧ degreeOf j f ≤ degreeOf j (C c * f)
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f ∧ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
constructor
Proof state after:
case left
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f

case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case left
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j (C c * f) ≤ degreeOf j f
Tactic:
convert MvPolynomial.degreeOf_C_mul_le f j c
Proof state after:
no goals
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
have := MvPolynomial.degreeOf_C_mul_le (C (c) * f) j (1/c)
Proof state after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * (C c * f)) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * (C c * f)) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
rw [<-mul_assoc] at this
Proof state after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * C c * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Theorem: MvPolynomial.degreeOf_C_mul
Proof state before:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c) * C c * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)
Tactic:
rw [←C_mul] at this
Proof state after:
case right
F : Type
inst✝¹ : Field F
σ R : Type
inst✝ : Field R
j : σ
c : R
hc : c ≠ 0
f : MvPolynomial σ R
this : degreeOf j (C (1 / c * c) * f) ≤ degreeOf j (C c * f)
⊢ degreeOf j f ≤ degreeOf j (C c * f)