ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Semiring R<VAR>p q : ℕ<VAR>hp : CharP R p<VAR>hq : ExpChar R q<GOAL>p = q ↔ Nat.Prime p
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p : ℕ<VAR>hp : CharP R p<VAR>hq : ExpChar R 1<GOAL>p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>hq : ExpChar R 1<GOAL>CharZero R
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>p q : ℕ<VAR>CharP R p<VAR>ExpChar R q<GOAL>q = 1 ↔ p = 0
<VAR>R : Type u<VAR>Semiring R<VAR>Nontrivial R<VAR>NoZeroDivisors R<VAR>p : ℕ<VAR>hp : CharP R p<VAR>p_ne_zero : p ≠ 0<GOAL>Nat.Prime p
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>hq : ExpChar R q<GOAL>Nat.Prime q ∨ q = 1
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>ExpChar R q<GOAL>0 < q
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>ExpChar R q<VAR>n : ℕ<GOAL>0 < q ^ n
<VAR>R : Type u<VAR>Ring R<VAR>IsDomain R<GOAL>∃ q, ExpChar R q
<VAR>R : Type u<VAR>Ring R<VAR>IsDomain R<GOAL>∃! q, ExpChar R q
<VAR>R : Type u<VAR>Ring R<VAR>IsDomain R<VAR>q : ℕ<VAR>h : ringExpChar R = q<GOAL>ExpChar R q
<VAR>R : Type u<VAR>Ring R<VAR>IsDomain R<VAR>q : ℕ<GOAL>ringExpChar R = q ↔ ExpChar R q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>Semiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>q : ℕ<VAR>hR : ExpChar R q<GOAL>ExpChar A q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>Semiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<VAR>ExpChar A p<GOAL>ExpChar R p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Semiring R<VAR>Semiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<GOAL>ExpChar R p ↔ ExpChar A p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>h : Function.Injective ⇑(algebraMap R A)<VAR>q : ℕ<VAR>ExpChar R q<GOAL>ExpChar A q
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>x y : R<VAR>h : Commute x y<GOAL>(x + y) ^ q = x ^ q + y ^ q
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>n : ℕ<VAR>x y : R<VAR>h : Commute x y<GOAL>(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
<VAR>R : Type u<VAR>Ring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ q = x ^ q - y ^ q
<VAR>R : Type u<VAR>Ring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>n : ℕ<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>x y : R<GOAL>(x + y) ^ q = x ^ q + y ^ q
<VAR>R : Type u<VAR>CommSemiring R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>n : ℕ<VAR>x y : R<GOAL>(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
<VAR>R : Type u<VAR>CommRing R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>x y : R<GOAL>(x - y) ^ q = x ^ q - y ^ q
<VAR>R : Type u<VAR>CommRing R<VAR>q : ℕ<VAR>hR : ExpChar R q<VAR>n : ℕ<VAR>x y : R<GOAL>(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n
<VAR>R : Type u<VAR>Ring R<VAR>q : ℕ<VAR>hR : ExpChar R q<GOAL>(-1) ^ q = -1
<VAR>R : Type u<VAR>Ring R<VAR>q n : ℕ<VAR>hR : ExpChar R q<GOAL>(-1) ^ q ^ n = -1
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(frobenius R p) x = x ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(iterateFrobenius R p n) x = x ^ p ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p n : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(⇑(frobenius R p))^[n] x = x ^ p ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p n : ℕ<VAR>ExpChar R p<GOAL>⇑(iterateFrobenius R p n) = (⇑(frobenius R p))^[n]
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(iterateFrobenius R p 1) x = x ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<GOAL>iterateFrobenius R p 1 = frobenius R p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(iterateFrobenius R p 0) x = x
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<GOAL>iterateFrobenius R p 0 = RingHom.id R
<VAR>R : Type u<VAR>CommSemiring R<VAR>p m n : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p m n : ℕ<VAR>ExpChar R p<GOAL>iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n)
<VAR>R : Type u<VAR>CommSemiring R<VAR>p m n : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x
<VAR>R : Type u<VAR>CommSemiring R<VAR>p m n : ℕ<VAR>ExpChar R p<GOAL>⇑(iterateFrobenius R p (m * n)) = (⇑(iterateFrobenius R p m))^[n]
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x y : R<GOAL>(frobenius R p) (x * y) = (frobenius R p) x * (frobenius R p) y
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<GOAL>(frobenius R p) 1 = 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>f : R →* S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>x : R<GOAL>f ((frobenius R p) x) = (frobenius S p) (f x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>g : R →+* S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>x : R<GOAL>g ((frobenius R p) x) = (frobenius S p) (g x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>f : R →* S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>x : R<VAR>n : ℕ<GOAL>f ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (f x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>g : R →+* S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>x : R<VAR>n : ℕ<GOAL>g ((⇑(frobenius R p))^[n] x) = (⇑(frobenius S p))^[n] (g x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<VAR>f : R →* R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<GOAL>(⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>x : R<VAR>f : R →+* R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<GOAL>(⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>Algebra R S<VAR>x : S<GOAL>(LinearMap.frobenius R S p) x = x ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Type u_1<VAR>CommSemiring S<VAR>p : ℕ<VAR>ExpChar R p<VAR>ExpChar S p<VAR>Algebra R S<VAR>n : ℕ<VAR>x : S<GOAL>(LinearMap.iterateFrobenius R S p n) x = x ^ p ^ n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<GOAL>(frobenius R p) 0 = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x y : R<GOAL>(frobenius R p) (x + y) = (frobenius R p) x + (frobenius R p) y
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<GOAL>(frobenius R p) ↑n = ↑n
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>l : List R<GOAL>l.sum ^ p = (List.map (fun x => x ^ p) l).sum
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>s : Multiset R<GOAL>s.sum ^ p = (Multiset.map (fun x => x ^ p) s).sum
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∑ i ∈ s, f i) ^ p = ∑ i ∈ s, f i ^ p
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<VAR>l : List R<GOAL>l.sum ^ p ^ n = (List.map (fun x => x ^ p ^ n) l).sum
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<VAR>s : Multiset R<GOAL>s.sum ^ p ^ n = (Multiset.map (fun x => x ^ p ^ n) s).sum
<VAR>R : Type u<VAR>CommSemiring R<VAR>p : ℕ<VAR>ExpChar R p<VAR>n : ℕ<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → R<GOAL>(∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n
<VAR>R : Type u<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x : R<GOAL>(frobenius R p) (-x) = -(frobenius R p) x
<VAR>R : Type u<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x y : R<GOAL>(frobenius R p) (x - y) = (frobenius R p) x - (frobenius R p) y
<VAR>M : Type u_4<VAR>AddZeroClass M<GOAL>[].sum = 0
<VAR>M : Type u_4<VAR>MulOneClass M<GOAL>[].prod = 1
<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>a : M<GOAL>[a].sum = a
<VAR>M : Type u_4<VAR>MulOneClass M<VAR>a : M<GOAL>[a].prod = a
<VAR>M : Type u_4<VAR>MulOneClass M<VAR>l : List M<GOAL>(1 :: l).prod = l.prod
<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>l : List M<GOAL>(0 :: l).sum = l.sum
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>MulOneClass M<VAR>l : List ι<GOAL>(List.map (fun x => 1) l).prod = 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>AddZeroClass M<VAR>l : List ι<GOAL>(List.map (fun x => 0) l).sum = 0
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>a : M<GOAL>(a :: l).prod = a * l.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>a : M<GOAL>(a :: l).sum = a + l.sum
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a + b)<VAR>unit : p 0<VAR>base : ∀ x ∈ l, p x<GOAL>p l.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ l, p x<GOAL>p l.prod
<VAR>M : Type u_4<VAR>Monoid M<VAR>l₁ l₂ : List M<GOAL>(l₁ ++ l₂).prod = l₁.prod * l₂.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l₁ l₂ : List M<GOAL>(l₁ ++ l₂).sum = l₁.sum + l₂.sum
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>a : M<GOAL>(l.concat a).sum = l.sum + a
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>a : M<GOAL>(l.concat a).prod = l.prod * a
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List (List M)<GOAL>l.join.sum = (List.map List.sum l).sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List (List M)<GOAL>l.join.prod = (List.map List.prod l).prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<GOAL>l.sum = List.foldr (fun x x_1 => x + x_1) 0 l
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<GOAL>l.prod = List.foldr (fun x x_1 => x * x_1) 1 l
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>n : ℕ<VAR>a : M<GOAL>(List.replicate n a).sum = n • a
<VAR>M : Type u_4<VAR>Monoid M<VAR>n : ℕ<VAR>a : M<GOAL>(List.replicate n a).prod = a ^ n
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>m : M<VAR>h : ∀ x ∈ l, x = m<GOAL>l.prod = m ^ l.length
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>m : M<VAR>h : ∀ x ∈ l, x = m<GOAL>l.sum = l.length • m
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>l : List ι<VAR>r : M → N → Prop<VAR>f : ι → M<VAR>g : ι → N<VAR>h₁ : r 1 1<VAR>h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)<GOAL>r (List.map f l).prod (List.map g l).prod
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>l : List ι<VAR>r : M → N → Prop<VAR>f : ι → M<VAR>g : ι → N<VAR>h₁ : r 0 0<VAR>h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i + a) (g i + b)<GOAL>r (List.map f l).sum (List.map g l).sum
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>R : M → N → Prop<VAR>h : R 0 0<VAR>hf : (R ⇒ R ⇒ R) (fun x x_1 => x + x_1) fun x x_1 => x + x_1<GOAL>(List.Forall₂ R ⇒ R) List.sum List.sum
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>R : M → N → Prop<VAR>h : R 1 1<VAR>hf : (R ⇒ R ⇒ R) (fun x x_1 => x * x_1) fun x x_1 => x * x_1<GOAL>(List.Forall₂ R ⇒ R) List.prod List.prod
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>l : List M<VAR>F : Type u_8<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<GOAL>(List.map (⇑f) l).sum = f l.sum
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>l : List M<VAR>F : Type u_8<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<GOAL>(List.map (⇑f) l).prod = f l.prod
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddMonoid M<VAR>AddMonoid N<VAR>AddMonoid P<VAR>l : List ι<VAR>f : M → N → P<VAR>hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d<VAR>hf' : f 0 0 = 0<VAR>f₁ : ι → M<VAR>f₂ : ι → N<GOAL>(List.map (fun i => f (f₁ i) (f₂ i)) l).sum = f (List.map f₁ l).sum (List.map f₂ l).sum
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Monoid M<VAR>Monoid N<VAR>Monoid P<VAR>l : List ι<VAR>f : M → N → P<VAR>hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → M<VAR>f₂ : ι → N<GOAL>(List.map (fun i => f (f₁ i) (f₂ i)) l).prod = f (List.map f₁ l).prod (List.map f₂ l).prod
<VAR>ι : Type u_1<VAR>α : Type u_8<VAR>CommMonoid α<VAR>l : List ι<VAR>f g : ι → α<GOAL>(List.map (fun i => f i * g i) l).prod = (List.map f l).prod * (List.map g l).prod
<VAR>ι : Type u_1<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>l : List ι<VAR>f g : ι → α<GOAL>(List.map (fun i => f i + g i) l).sum = (List.map f l).sum + (List.map g l).sum
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>L : List ι<VAR>f : ι → M<VAR>G : Type u_8<VAR>FunLike G M N<VAR>MonoidHomClass G M N<VAR>g : G<GOAL>(List.map (⇑g ∘ f) L).prod = g (List.map f L).prod
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>L : List ι<VAR>f : ι → M<VAR>G : Type u_8<VAR>FunLike G M N<VAR>AddMonoidHomClass G M N<VAR>g : G<GOAL>(List.map (⇑g ∘ f) L).sum = g (List.map f L).sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>L : List M<GOAL>(∀ m ∈ L, IsUnit m) → IsUnit L.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>L : List M<GOAL>(∀ m ∈ L, IsAddUnit m) → IsAddUnit L.sum
<VAR>α : Type u_8<VAR>AddCommMonoid α<VAR>L : List α<GOAL>IsAddUnit L.sum ↔ ∀ m ∈ L, IsAddUnit m
<VAR>α : Type u_8<VAR>CommMonoid α<VAR>L : List α<GOAL>IsUnit L.prod ↔ ∀ m ∈ L, IsUnit m
<VAR>M : Type u_4<VAR>Monoid M<VAR>L : List M<VAR>i : ℕ<GOAL>(List.take i L).prod * (List.drop i L).prod = L.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>L : List M<VAR>i : ℕ<GOAL>(List.take i L).sum + (List.drop i L).sum = L.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>L : List M<VAR>i : ℕ<VAR>p : i < L.length<GOAL>(List.take (i + 1) L).prod = (List.take i L).prod * L[i]
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>L : List M<VAR>i : ℕ<VAR>p : i < L.length<GOAL>(List.take (i + 1) L).sum = (List.take i L).sum + L[i]
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>L : List M<VAR>h : L.sum ≠ 0<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>Monoid M<VAR>L : List M<VAR>h : L.prod ≠ 1<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>Preorder M<VAR>L : List M<VAR>h : 0 < L.sum<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>Monoid M<VAR>Preorder M<VAR>L : List M<VAR>h : 1 < L.prod<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>Monoid M<VAR>Preorder M<VAR>L : List M<VAR>h : L.prod < 1<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>Preorder M<VAR>L : List M<VAR>h : L.sum < 0<GOAL>0 < L.length
<VAR>M : Type u_4<VAR>Monoid M<VAR>L : List M<VAR>n : ℕ<VAR>a : M<GOAL>(L.set n a).prod = ((List.take n L).prod * if n < L.length then a else 1) * (List.drop (n + 1) L).prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>L : List M<VAR>n : ℕ<VAR>a : M<GOAL>(L.set n a).sum = ((List.take n L).sum + if n < L.length then a else 0) + (List.drop (n + 1) L).sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<GOAL>(l.get? 0).getD 1 * l.tail.prod = l.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<GOAL>(l.get? 0).getD 0 + l.tail.sum = l.sum
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>Inhabited M<VAR>l : List M<VAR>h : l ≠ []<GOAL>l.headI + l.tail.sum = l.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>Inhabited M<VAR>l : List M<VAR>h : l ≠ []<GOAL>l.headI * l.tail.prod = l.prod
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>y : M<VAR>h : ∀ x ∈ l, Commute y x<GOAL>Commute y l.prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>y : M<VAR>h : ∀ x ∈ l, AddCommute y x<GOAL>AddCommute y l.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>y : M<VAR>h : ∀ x ∈ l, Commute x y<GOAL>Commute l.prod y
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>y : M<VAR>h : ∀ x ∈ l, AddCommute x y<GOAL>AddCommute l.sum y
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>(List.map f (List.range n.succ)).sum = (List.map f (List.range n)).sum + f n
<VAR>M : Type u_4<VAR>Monoid M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>(List.map f (List.range n.succ)).prod = (List.map f (List.range n)).prod * f n
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>(List.map f (List.range n.succ)).sum = f 0 + (List.map (fun i => f i.succ) (List.range n)).sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>(List.map f (List.range n.succ)).prod = f 0 * (List.map (fun i => f i.succ) (List.range n)).prod
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>hl : ∀ x ∈ l, x = 0<GOAL>l.sum = 0
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>hl : ∀ x ∈ l, x = 1<GOAL>l.prod = 1
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>h : l.sum ≠ 0<GOAL>∃ x ∈ l, x ≠ 0
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>h : l.prod ≠ 1<GOAL>∃ x ∈ l, x ≠ 1
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>a : M<VAR>DecidableEq M<VAR>ha : a ∈ l<VAR>comm : ∀ x ∈ l, ∀ y ∈ l, x + y = y + x<GOAL>a + (l.erase a).sum = l.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>a : M<VAR>DecidableEq M<VAR>ha : a ∈ l<VAR>comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x<GOAL>a * (l.erase a).prod = l.prod
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>Monoid M<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<VAR>f : α → M<VAR>hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1<GOAL>(List.map f l).prod = f a ^ List.count a l
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>AddMonoid M<VAR>DecidableEq α<VAR>l : List α<VAR>a : α<VAR>f : α → M<VAR>hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0<GOAL>(List.map f l).sum = List.count a l • f a
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l : List M<VAR>DecidableEq M<VAR>a : M<VAR>h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 0<GOAL>l.sum = List.count a l • a
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<VAR>DecidableEq M<VAR>a : M<VAR>h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1<GOAL>l.prod = a ^ List.count a l
<VAR>M : Type u_4<VAR>AddMonoid M<VAR>l₁ l₂ : List M<VAR>h : l₁ ~ l₂<VAR>hc : List.Pairwise AddCommute l₁<GOAL>l₁.sum = l₂.sum
<VAR>M : Type u_4<VAR>Monoid M<VAR>l₁ l₂ : List M<VAR>h : l₁ ~ l₂<VAR>hc : List.Pairwise Commute l₁<GOAL>l₁.prod = l₂.prod
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>a : M<VAR>l : List M<VAR>DecidableEq M<VAR>ha : a ∈ l<GOAL>a * (l.erase a).prod = l.prod
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>a : M<VAR>l : List M<VAR>DecidableEq M<VAR>ha : a ∈ l<GOAL>a + (l.erase a).sum = l.sum
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>DecidableEq α<VAR>f : α → M<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → f a + (List.map f (l.erase a)).sum = (List.map f l).sum
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CommMonoid M<VAR>DecidableEq α<VAR>f : α → M<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → f a * (List.map f (l.erase a)).prod = (List.map f l).prod
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>l₁ l₂ : List M<VAR>h : l₁ ~ l₂<GOAL>l₁.sum = l₂.sum
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>l₁ l₂ : List M<VAR>h : l₁ ~ l₂<GOAL>l₁.prod = l₂.prod
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>l : List M<GOAL>l.reverse.sum = l.sum
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>l : List M<GOAL>l.reverse.prod = l.prod
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>l l' : List M<GOAL>l.sum + l'.sum = (List.zipWith (fun x x_1 => x + x_1) l l').sum + (List.drop l'.length l).sum + (List.drop l.length l').sum
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>l l' : List M<GOAL>l.prod * l'.prod = (List.zipWith (fun x x_1 => x * x_1) l l').prod * (List.drop l'.length l).prod * (List.drop l.length l').prod
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>l l' : List M<VAR>h : l.length = l'.length<GOAL>l.prod * l'.prod = (List.zipWith (fun x x_1 => x * x_1) l l').prod
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>l l' : List M<VAR>h : l.length = l'.length<GOAL>l.sum + l'.sum = (List.zipWith (fun x x_1 => x + x_1) l l').sum
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f g : α → M<VAR>l : List α<GOAL>(List.map (fun a => if p a then f a else g a) l).sum = (List.map f (List.filter (fun b => decide (p b)) l)).sum + (List.map g (List.filter (fun a => decide ¬p a) l)).sum
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f g : α → M<VAR>l : List α<GOAL>(List.map (fun a => if p a then f a else g a) l).prod = (List.map f (List.filter (fun b => decide (p b)) l)).prod * (List.map g (List.filter (fun a => decide ¬p a) l)).prod
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>CommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → M<VAR>l : List α<GOAL>(List.map f (List.filter (fun b => decide (p b)) l)).prod * (List.map f (List.filter (fun x => decide ¬p x) l)).prod = (List.map f l).prod
<VAR>α : Type u_2<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : α → M<VAR>l : List α<GOAL>(List.map f (List.filter (fun b => decide (p b)) l)).sum + (List.map f (List.filter (fun x => decide ¬p x) l)).sum = (List.map f l).sum
<VAR>M : Type u_4<VAR>AddLeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (List.take i L).sum = (List.take i L').sum<GOAL>L = L'
<VAR>M : Type u_4<VAR>LeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (List.take i L).prod = (List.take i L').prod<GOAL>L = L'
<VAR>G : Type u_7<VAR>Group G<VAR>L : List G<GOAL>L.prod⁻¹ = (List.map (fun x => x⁻¹) L).reverse.prod
<VAR>G : Type u_7<VAR>AddGroup G<VAR>L : List G<GOAL>-L.sum = (List.map (fun x => -x) L).reverse.sum
<VAR>G : Type u_7<VAR>Group G<VAR>L : List G<GOAL>L.reverse.prod = (List.map (fun x => x⁻¹) L).prod⁻¹
<VAR>G : Type u_7<VAR>AddGroup G<VAR>L : List G<GOAL>L.reverse.sum = -(List.map (fun x => -x) L).sum
<VAR>G : Type u_7<VAR>Group G<VAR>L : List G<VAR>i : ℕ<VAR>p : i < L.length<GOAL>(List.drop (i + 1) L).prod = (L.get ⟨i, p⟩)⁻¹ * (List.drop i L).prod
<VAR>G : Type u_7<VAR>AddGroup G<VAR>L : List G<VAR>i : ℕ<VAR>p : i < L.length<GOAL>(List.drop (i + 1) L).sum = -L.get ⟨i, p⟩ + (List.drop i L).sum
<VAR>G : Type u_7<VAR>Group G<VAR>n : ℕ<VAR>f : ℕ → G<GOAL>(List.map (fun k => f k / f (k + 1)) (List.range n)).prod = f 0 / f n
<VAR>G : Type u_7<VAR>AddGroup G<VAR>n : ℕ<VAR>f : ℕ → G<GOAL>(List.map (fun k => f k - f (k + 1)) (List.range n)).sum = f 0 - f n
<VAR>G : Type u_7<VAR>Group G<VAR>l : List G<GOAL>l.prod = 1 → ∀ (n : ℕ), (l.rotate n).prod = 1
<VAR>G : Type u_7<VAR>AddCommGroup G<VAR>L : List G<GOAL>-L.sum = (List.map (fun x => -x) L).sum
<VAR>G : Type u_7<VAR>CommGroup G<VAR>L : List G<GOAL>L.prod⁻¹ = (List.map (fun x => x⁻¹) L).prod
<VAR>G : Type u_7<VAR>AddCommGroup G<VAR>n : ℕ<VAR>f : ℕ → G<GOAL>(List.map (fun k => f (k + 1) - f k) (List.range n)).sum = f n - f 0
<VAR>G : Type u_7<VAR>CommGroup G<VAR>n : ℕ<VAR>f : ℕ → G<GOAL>(List.map (fun k => f (k + 1) / f k) (List.range n)).prod = f n / f 0
<VAR>G : Type u_7<VAR>AddCommGroup G<VAR>L : List G<VAR>n : ℕ<VAR>a : G<GOAL>(L.set n a).sum = L.sum + if hn : n < L.length then -L.get ⟨n, hn⟩ + a else 0
<VAR>G : Type u_7<VAR>CommGroup G<VAR>L : List G<VAR>n : ℕ<VAR>a : G<GOAL>(L.set n a).prod = L.prod * if hn : n < L.length then (L.get ⟨n, hn⟩)⁻¹ * a else 1
<VAR>G : Type u_7<VAR>CommGroup G<VAR>A : Type u_8<VAR>DecidableEq A<VAR>l : List A<VAR>f g : A → G<VAR>a : A<GOAL>(List.map (fun x => if x = a then f x else g x) l).prod = (f a / g a) ^ List.count a l * (List.map g l).prod
<VAR>G : Type u_7<VAR>AddCommGroup G<VAR>A : Type u_8<VAR>DecidableEq A<VAR>l : List A<VAR>f g : A → G<VAR>a : A<GOAL>(List.map (fun x => if x = a then f x else g x) l).sum = List.count a l • (f a - g a) + (List.map g l).sum
<VAR>m n : ℕ<GOAL>(List.replicate m n).sum = m * n
<VAR>L : List ℕ<GOAL>L.headI + L.tail.sum = L.sum
<VAR>L : List ℕ<GOAL>L.headI ≤ L.sum
<VAR>L : List ℕ<GOAL>L.tail.sum = L.sum - L.headI
<VAR>α : Type u_2<VAR>One α<VAR>Mul α<VAR>Inv α<GOAL>[].alternatingProd = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>Add α<VAR>Neg α<GOAL>[].alternatingSum = 0
<VAR>α : Type u_2<VAR>One α<VAR>Mul α<VAR>Inv α<VAR>a : α<GOAL>[a].alternatingProd = a
<VAR>α : Type u_2<VAR>Zero α<VAR>Add α<VAR>Neg α<VAR>a : α<GOAL>[a].alternatingSum = a
<VAR>α : Type u_2<VAR>One α<VAR>Mul α<VAR>Inv α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
<VAR>α : Type u_2<VAR>Zero α<VAR>Add α<VAR>Neg α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingSum = a + -b + l.alternatingSum
<VAR>α : Type u_2<VAR>SubNegMonoid α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingSum = a - b + l.alternatingSum
<VAR>α : Type u_2<VAR>DivInvMonoid α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingProd = a / b * l.alternatingProd
<VAR>α : Type u_2<VAR>AddCommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).alternatingSum = a + -l.alternatingSum
<VAR>α : Type u_2<VAR>CommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).alternatingProd = a * l.alternatingProd⁻¹
<VAR>α : Type u_2<VAR>AddCommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).alternatingSum = a - l.alternatingSum