ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 7 → β<GOAL>∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 7 → β<GOAL>∑ i : Fin 7, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : Fin 8 → β<GOAL>∑ i : Fin 8, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7
<VAR>β : Type u_2<VAR>CommMonoid β<VAR>f : Fin 8 → β<GOAL>∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
<VAR>n : ℕ<VAR>R : Type u_3<VAR>CommSemiring R<VAR>a b : R<GOAL>∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card) = (a + b) ^ n
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>n : ℕ<VAR>x : α<GOAL>∏ _i : Fin n, x = x ^ n
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>x : α<GOAL>∑ _i : Fin n, x = n • x
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>n : ℕ<VAR>v : Fin n.succ → M<GOAL>∏ i ∈ Finset.Ioi 0, v i = ∏ j : Fin n, v j.succ
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>v : Fin n.succ → M<GOAL>∑ i ∈ Finset.Ioi 0, v i = ∑ j : Fin n, v j.succ
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>n : ℕ<VAR>i : Fin n<VAR>v : Fin n.succ → M<GOAL>∏ j ∈ Finset.Ioi i.succ, v j = ∏ j ∈ Finset.Ioi i, v j.succ
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>i : Fin n<VAR>v : Fin n.succ → M<GOAL>∑ j ∈ Finset.Ioi i.succ, v j = ∑ j ∈ Finset.Ioi i, v j.succ
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>a b : ℕ<VAR>f : Fin b → M<VAR>h : a = b<GOAL>∏ i : Fin a, f (Fin.cast h i) = ∏ i : Fin b, f i
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>f : Fin b → M<VAR>h : a = b<GOAL>∑ i : Fin a, f (Fin.cast h i) = ∑ i : Fin b, f i
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<GOAL>∑ i : Fin (a + b), f i = ∑ i : Fin a, f (Fin.castAdd b i) + ∑ i : Fin b, f (Fin.natAdd a i)
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<GOAL>∏ i : Fin (a + b), f i = (∏ i : Fin a, f (Fin.castAdd b i)) * ∏ i : Fin b, f (Fin.natAdd a i)
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<VAR>hf : ∀ (j : Fin b), f (Fin.natAdd a j) = 0<GOAL>∑ i : Fin (a + b), f i = ∑ i : Fin a, f (Fin.castLE ⋯ i)
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<VAR>hf : ∀ (j : Fin b), f (Fin.natAdd a j) = 1<GOAL>∏ i : Fin (a + b), f i = ∏ i : Fin a, f (Fin.castLE ⋯ i)
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>Fin.partialSum f 0 = 0
<VAR>α : Type u_1<VAR>Monoid α<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>Fin.partialProd f 0 = 1
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<VAR>j : Fin n<GOAL>Fin.partialSum f j.succ = Fin.partialSum f j.castSucc + f j
<VAR>α : Type u_1<VAR>Monoid α<VAR>n : ℕ<VAR>f : Fin n → α<VAR>j : Fin n<GOAL>Fin.partialProd f j.succ = Fin.partialProd f j.castSucc * f j
<VAR>α : Type u_1<VAR>Monoid α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>j : Fin (n + 1)<GOAL>Fin.partialProd f j.succ = f 0 * Fin.partialProd (Fin.tail f) j
<VAR>α : Type u_1<VAR>AddMonoid α<VAR>n : ℕ<VAR>f : Fin (n + 1) → α<VAR>j : Fin (n + 1)<GOAL>Fin.partialSum f j.succ = f 0 + Fin.partialSum (Fin.tail f) j
<VAR>n : ℕ<VAR>G : Type u_3<VAR>Group G<VAR>f : Fin (n + 1) → G<GOAL>(f 0 • Fin.partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) = f
<VAR>n : ℕ<VAR>G : Type u_3<VAR>AddGroup G<VAR>f : Fin (n + 1) → G<GOAL>(f 0 +ᵥ Fin.partialSum fun i => -f ↑↑i + f i.succ) = f
<VAR>n : ℕ<VAR>G : Type u_3<VAR>AddGroup G<VAR>f : Fin n → G<VAR>i : Fin n<GOAL>-Fin.partialSum f i.castSucc + Fin.partialSum f i.succ = f i
<VAR>n : ℕ<VAR>G : Type u_3<VAR>Group G<VAR>f : Fin n → G<VAR>i : Fin n<GOAL>(Fin.partialProd f i.castSucc)⁻¹ * Fin.partialProd f i.succ = f i
<VAR>n : ℕ<VAR>G : Type u_3<VAR>AddGroup G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<GOAL>-Fin.partialSum g (j.succ.succAbove k.castSucc) + Fin.partialSum g (j.succAbove k).succ = j.contractNth (fun x x_1 => x + x_1) g k
<VAR>n : ℕ<VAR>G : Type u_3<VAR>Group G<VAR>g : Fin (n + 1) → G<VAR>j : Fin (n + 1)<VAR>k : Fin n<GOAL>(Fin.partialProd g (j.succ.succAbove k.castSucc))⁻¹ * Fin.partialProd g (j.succAbove k).succ = j.contractNth (fun x x_1 => x * x_1) g k
<VAR>m n : ℕ<VAR>f : Fin n → Fin m<GOAL>↑(finFunctionFinEquiv f) = ∑ i : Fin n, ↑(f i) * m ^ ↑i
<VAR>m n : ℕ<VAR>a : Fin (m ^ n)<VAR>b : Fin n<GOAL>↑(finFunctionFinEquiv.symm a b) = ↑a / m ^ ↑b % m
<VAR>m n : ℕ<VAR>NeZero m<VAR>i : Fin n<VAR>j : Fin m<GOAL>↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
<VAR>m : ℕ<VAR>n : Fin m → ℕ<VAR>f : (i : Fin m) → Fin (n i)<GOAL>↑(finPiFinEquiv f) = ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE ⋯ j)
<VAR>m : ℕ<VAR>n : Fin m → ℕ<VAR>∀ (i : Fin m), NeZero (n i)<VAR>i : Fin m<VAR>j : Fin (n i)<GOAL>↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j : Fin ↑i, n (Fin.castLE ⋯ j)
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<GOAL>(List.take i (List.ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) Finset.univ, f j
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<GOAL>(List.take i (List.ofFn f)).sum = ∑ j ∈ Finset.filter (fun j => ↑j < i) Finset.univ, f j
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(List.ofFn f).sum = ∑ i : Fin n, f i
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>(List.ofFn f).prod = ∏ i : Fin n, f i
<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>L : List G<GOAL>L.alternatingSum = ∑ i : Fin L.length, (-1) ^ ↑i • L.get i
<VAR>G : Type u_3<VAR>CommGroup G<VAR>L : List G<GOAL>L.alternatingProd = ∏ i : Fin L.length, L.get i ^ (-1) ^ ↑i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>p : ℕ<VAR>CharP R p<GOAL>CharP 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>p : ℕ<VAR>CharP R p<GOAL>CharP A p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>Field R<VAR>Semiring A<VAR>Algebra R A<VAR>Nontrivial A<VAR>p : ℕ<VAR>CharP R p<GOAL>CharP A p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring A<VAR>f : R →+* A<VAR>h : Function.Injective ⇑f<VAR>CharZero R<GOAL>CharZero A
<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>CharZero R<GOAL>CharZero A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<VAR>CharP A p<GOAL>CharP R p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring A<VAR>f : R →+* A<VAR>H : Function.Injective ⇑f<VAR>p : ℕ<GOAL>CharP R p ↔ CharP A p
<VAR>R : Type u_1<VAR>Nontrivial R<VAR>Semiring R<VAR>Algebra ℚ R<GOAL>CharP R 0
<VAR>R : Type u_1<VAR>Nontrivial R<VAR>Ring R<VAR>Algebra ℚ R<GOAL>CharZero R
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CommSemiring L<VAR>Nontrivial L<VAR>Algebra K L<VAR>p : ℕ<GOAL>CharP K p ↔ CharP L p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CommSemiring L<VAR>Nontrivial L<VAR>Algebra K L<GOAL>ringChar K = ringChar L
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>p : ℕ<VAR>CharP R p<GOAL>CharP K p
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>CharZero R<GOAL>CharZero K
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<GOAL>CharP R p ↔ ∀ (x : ℕ), ↑x = 0 ↔ p ∣ x
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>self : CharP R p<VAR>x : ℕ<GOAL>↑x = 0 ↔ p ∣ x
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a : ℕ<GOAL>↑a = 0 ↔ p ∣ a
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>q : ℕ<VAR>h : p = q<GOAL>CharP R q
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a b : ℕ<VAR>h : a ≡ b [MOD p]<GOAL>↑a = ↑b
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<GOAL>↑p = 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>p.AtLeastTwo<GOAL>OfNat.ofNat p = 0
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a : ℕ<GOAL>↑a = ↑(a % p)
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p q : ℕ<VAR>_hp : CharP R p<VAR>_hq : CharP R q<GOAL>p = q
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a b : ℕ<VAR>IsRightCancelAdd R<GOAL>↑a = ↑b ↔ a ≡ b [MOD p]
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>IsRightCancelAdd R<GOAL>Set.InjOn Nat.cast (Set.Iio p)
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a : ℤ<GOAL>↑a = 0 ↔ ↑p ∣ a
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a b : ℤ<GOAL>↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>a : ℤ<GOAL>↑a = ↑(a % ↑p)
<VAR>R : Type u_1<VAR>AddGroupWithOne R<VAR>CharP R 0<GOAL>CharZero R
<VAR>R : Type u_1<VAR>AddGroupWithOne R<GOAL>CharP R 0 ↔ CharZero R
<VAR>R : Type u_1<VAR>NonAssocSemiring R<GOAL>∃ p, CharP R p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<GOAL>∃! p, CharP R p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>x : ℕ<GOAL>↑x = 0 ↔ ringChar R ∣ x
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>p : ℕ<VAR>C : CharP R p<GOAL>ringChar R = p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>p : ℕ<VAR>h : ringChar R = p<GOAL>CharP R p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>p : ℕ<GOAL>ringChar R = p ↔ CharP R p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>x : ℕ<VAR>hx : ↑x = 0<GOAL>ringChar R ∣ x
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>CharZero R<GOAL>ringChar R = 0
<VAR>R : Type u_1<VAR>NonAssocSemiring R<GOAL>↑(ringChar R) = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>CharP R p<VAR>Fact (2 < p)<GOAL>-1 ≠ 1
<VAR>K : Type u_2<VAR>L : Type u_3<VAR>DivisionRing K<VAR>Semiring L<VAR>Nontrivial L<VAR>f : K →+* L<VAR>p : ℕ<GOAL>CharP K p ↔ CharP L p
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>p : ℕ<VAR>CharP R p<VAR>k : ℕ<GOAL>↑k = ↑(k % p)
<VAR>R : Type u_1<VAR>NonAssocRing R<GOAL>ringChar R = 0 ↔ CharZero R
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>Nontrivial R<VAR>p : ℕ<VAR>hc : CharP R p<GOAL>p ≠ 1
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>NoZeroDivisors R<VAR>p : ℕ<VAR>hc : CharP R p<VAR>hp : 2 ≤ p<GOAL>Nat.Prime p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>p : ℕ<VAR>hc : CharP R p<GOAL>Nat.Prime p ∨ p = 0
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>Nontrivial R<GOAL>CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>p : ℕ<VAR>NeZero p<VAR>CharP R p<GOAL>Fact (Nat.Prime p)
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>CharP R 1<GOAL>Subsingleton R
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>Nontrivial R<VAR>CharP R 1<GOAL>False
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>Nontrivial R<GOAL>ringChar R ≠ 1
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>v : ℕ<VAR>hv : v ≠ 1<VAR>hr : CharP R v<GOAL>Nontrivial R
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>Nontrivial R<VAR>p : ℕ<VAR>hprime : Nat.Prime p<VAR>hp0 : ↑p = 0<GOAL>ringChar R = p
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>Nontrivial R<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>CharP R p ↔ ↑p = 0
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>2 ≠ 0
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>-1 ≠ 1
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Nontrivial R<VAR>NoZeroDivisors R<VAR>hR : ringChar R ≠ 2<VAR>a : R<GOAL>-a = a ↔ a = 0
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Nontrivial R<VAR>hR : ringChar R ≠ 2<GOAL>Set.InjOn Int.cast {0, 1, -1}
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>n p : ℕ<VAR>CharP R p<VAR>h : ¬p ∣ n<GOAL>NeZero ↑n
<VAR>R : Type u_1<VAR>AddMonoidWithOne R<VAR>p : ℕ<VAR>CharP R p<VAR>k : ℕ<VAR>h : NeZero ↑k<GOAL>¬p ∣ k
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>NoZeroDivisors R<VAR>Nontrivial R<GOAL>CharZero R ↔ ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hR : ringChar R ≠ 0<GOAL>IsUnit ↑p ↔ ¬p ∣ ringChar R
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>Finite R<GOAL>IsUnit ↑p ↔ ¬p ∣ ringChar R
<VAR>R : Type u_1<VAR>CommRing R<VAR>Fintype R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>p ∣ ringChar R ↔ p ∣ Fintype.card R
<VAR>R : Type u_1<VAR>CommRing R<VAR>Fintype R<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hp : p ∣ Fintype.card R<GOAL>¬IsUnit ↑p
<VAR>R : Type u_1<VAR>NonAssocRing R<VAR>Fintype R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hR : Fintype.card R = p<GOAL>CharP R p
<VAR>m n : ℕ<GOAL>gcd m n = m.gcd n
<VAR>m n : ℕ<GOAL>lcm m n = m.lcm n
<VAR>z : ℤ<GOAL>normUnit z = if 0 ≤ z then 1 else -1
<VAR>z : ℤ<VAR>h : z ≤ 0<GOAL>normalize z = -z
<VAR>n : ℕ<GOAL>normalize ↑n = ↑n
<VAR>z : ℤ<VAR>hz : normalize z = z<GOAL>0 ≤ z
<VAR>z : ℤ<GOAL>normalize z = z ↔ 0 ≤ z
<VAR>a b : ℤ<VAR>h : Associated a b<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<GOAL>a = b
<VAR>i j : ℤ<GOAL>↑(i.gcd j) = gcd i j
<VAR>i j : ℤ<GOAL>↑(i.lcm j) = lcm i j
<VAR>i j : ℤ<GOAL>(gcd i j).natAbs = i.gcd j
<VAR>i j : ℤ<GOAL>(lcm i j).natAbs = i.lcm j
<VAR>a b : ℤ<GOAL>a.gcd b = a.natAbs.gcd b.natAbs
<VAR>k : ℤ<GOAL>Associated k ↑k.natAbs
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f b * ∏ x ∈ Finset.Ico a b, f x = ∏ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f b + ∑ x ∈ Finset.Ico a b, f x = ∑ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>(∏ x ∈ Finset.Ico a b, f x) * f b = ∏ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>∑ x ∈ Finset.Ico a b, f x + f b = ∑ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f a * ∏ x ∈ Finset.Ioc a b, f x = ∏ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f a + ∑ x ∈ Finset.Ioc a b, f x = ∑ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>(∏ x ∈ Finset.Ioc a b, f x) * f a = ∏ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>∑ x ∈ Finset.Ioc a b, f x + f a = ∑ x ∈ Finset.Icc a b, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>f a * ∏ x ∈ Finset.Ioi a, f x = ∏ x ∈ Finset.Ici a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>f a + ∑ x ∈ Finset.Ioi a, f x = ∑ x ∈ Finset.Ici a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>∑ x ∈ Finset.Ioi a, f x + f a = ∑ x ∈ Finset.Ici a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>(∏ x ∈ Finset.Ioi a, f x) * f a = ∏ x ∈ Finset.Ici a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>f a * ∏ x ∈ Finset.Iio a, f x = ∏ x ∈ Finset.Iic a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>f a + ∑ x ∈ Finset.Iio a, f x = ∑ x ∈ Finset.Iic a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>∑ x ∈ Finset.Iio a, f x + f a = ∑ x ∈ Finset.Iic a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>PartialOrder α<VAR>CommMonoid M<VAR>f : α → M<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>(∏ x ∈ Finset.Iio a, f x) * f a = ∏ x ∈ Finset.Iic a, f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Fintype α<VAR>LinearOrder α<VAR>LocallyFiniteOrderTop α<VAR>LocallyFiniteOrderBot α<VAR>CommMonoid M<VAR>f : α → α → M<GOAL>∏ i : α, ∏ j ∈ Finset.Ioi i, f j i * f i j = ∏ i : α, ∏ j ∈ {i}ᶜ, f j i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>Fintype α<VAR>LinearOrder α<VAR>LocallyFiniteOrderTop α<VAR>LocallyFiniteOrderBot α<VAR>AddCommMonoid M<VAR>f : α → α → M<GOAL>∑ i : α, ∑ j ∈ Finset.Ioi i, (f j i + f i j) = ∑ i : α, ∑ j ∈ {i}ᶜ, f j i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∏ x ∈ Finset.Ico a b, f (x + c) = ∏ x ∈ Finset.Ico (a + c) (b + c), f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∑ x ∈ Finset.Ico a b, f (x + c) = ∑ x ∈ Finset.Ico (a + c) (b + c), f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∏ x ∈ Finset.Ico a b, f (c + x) = ∏ x ∈ Finset.Ico (a + c) (b + c), f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>OrderedCancelAddCommMonoid α<VAR>ExistsAddOfLE α<VAR>LocallyFiniteOrder α<VAR>f : α → M<VAR>a b c : α<GOAL>∑ x ∈ Finset.Ico a b, f (c + x) = ∑ x ∈ Finset.Ico (a + c) (b + c), f x
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>f : ℕ → M<GOAL>∏ k ∈ Finset.Ico a (b + 1), f k = (∏ k ∈ Finset.Ico a b, f k) * f b
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>f : ℕ → M<GOAL>∑ k ∈ Finset.Ico a (b + 1), f k = ∑ k ∈ Finset.Ico a b, f k + f b
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>a b : ℕ<VAR>hab : a < b<VAR>f : ℕ → M<GOAL>∏ k ∈ Finset.Ico a b, f k = f a * ∏ k ∈ Finset.Ico (a + 1) b, f k
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>hab : a < b<VAR>f : ℕ → M<GOAL>∑ k ∈ Finset.Ico a b, f k = f a + ∑ k ∈ Finset.Ico (a + 1) b, f k
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>(∏ i ∈ Finset.Ico m n, f i) * ∏ i ∈ Finset.Ico n k, f i = ∏ i ∈ Finset.Ico m k, f i
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>∑ i ∈ Finset.Ico m n, f i + ∑ i ∈ Finset.Ico n k, f i = ∑ i ∈ Finset.Ico m k, f i
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>(∏ i ∈ Finset.Ioc m n, f i) * ∏ i ∈ Finset.Ioc n k, f i = ∏ i ∈ Finset.Ioc m k, f i
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>∑ i ∈ Finset.Ioc m n, f i + ∑ i ∈ Finset.Ioc n k, f i = ∑ i ∈ Finset.Ioc m k, f i
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>f : ℕ → M<GOAL>∑ k ∈ Finset.Ioc a (b + 1), f k = ∑ k ∈ Finset.Ioc a b, f k + f (b + 1)
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b<VAR>f : ℕ → M<GOAL>∏ k ∈ Finset.Ioc a (b + 1), f k = (∏ k ∈ Finset.Ioc a b, f k) * f (b + 1)
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b + 1<VAR>f : ℕ → M<GOAL>∏ k ∈ Finset.Icc a (b + 1), f k = (∏ k ∈ Finset.Icc a b, f k) * f (b + 1)
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>hab : a ≤ b + 1<VAR>f : ℕ → M<GOAL>∑ k ∈ Finset.Icc a (b + 1), f k = ∑ k ∈ Finset.Icc a b, f k + f (b + 1)
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∑ k ∈ Finset.range m, f k + ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(∏ k ∈ Finset.range m, f k) * ∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range n, f k
<VAR>δ : Type u_3<VAR>AddCommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k + -∑ k ∈ Finset.range m, f k
<VAR>δ : Type u_3<VAR>CommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) * (∏ k ∈ Finset.range m, f k)⁻¹
<VAR>δ : Type u_3<VAR>CommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∏ k ∈ Finset.Ico m n, f k = (∏ k ∈ Finset.range n, f k) / ∏ k ∈ Finset.range m, f k
<VAR>δ : Type u_3<VAR>AddCommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k - ∑ k ∈ Finset.range m, f k
<VAR>α : Type u_3<VAR>AddCommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>∑ k ∈ Finset.range m, f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.filter (fun k => n ≤ k) (Finset.range m), f k
<VAR>α : Type u_3<VAR>CommGroup α<VAR>f : ℕ → α<VAR>n m : ℕ<VAR>hnm : n ≤ m<GOAL>(∏ k ∈ Finset.range m, f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.filter (fun k => n ≤ k) (Finset.range m), f k
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico i b, f i j = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), f i j
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : ℕ → M<VAR>m n : ℕ<GOAL>∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range (n - m), f (m + k)
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>m n : ℕ<GOAL>∏ k ∈ Finset.Ico m n, f k = ∏ k ∈ Finset.range (n - m), f (m + k)
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>m n : ℕ<VAR>h : m ≤ n + 1<GOAL>∏ j ∈ Finset.Ico k m, f (n - j) = ∏ j ∈ Finset.Ico (n + 1 - m) (n + 1 - k), f j
<VAR>δ : Type u_3<VAR>AddCommMonoid δ<VAR>f : ℕ → δ<VAR>k : ℕ<VAR>m n : ℕ<VAR>h : m ≤ n + 1<GOAL>∑ j ∈ Finset.Ico k m, f (n - j) = ∑ j ∈ Finset.Ico (n + 1 - m) (n + 1 - k), f j
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : ℕ → M<VAR>n : ℕ<GOAL>∏ j ∈ Finset.range n, f (n - 1 - j) = ∏ j ∈ Finset.range n, f j
<VAR>δ : Type u_3<VAR>AddCommMonoid δ<VAR>f : ℕ → δ<VAR>n : ℕ<GOAL>∑ j ∈ Finset.range n, f (n - 1 - j) = ∑ j ∈ Finset.range n, f j
<VAR>n : ℕ<GOAL>∏ x ∈ Finset.Ico 1 (n + 1), x = n !
<VAR>n : ℕ<GOAL>∏ x ∈ Finset.range n, (x + 1) = n !
<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, i) * 2 = n * (n - 1)
<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, i = n * (n - 1) / 2
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>n : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (m + 1), f k (m - k) = ∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (n - m), f m k
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (m + 1), f k (m - k) = ∑ m ∈ Finset.range n, ∑ k ∈ Finset.range (n - m), f m k
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>n : ℕ<VAR>CommGroup M<GOAL>(∏ i ∈ Finset.range (n + 1), f i) / ∏ i ∈ Finset.range n, f i = f n
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>n : ℕ<VAR>AddCommGroup M<GOAL>∑ i ∈ Finset.range (n + 1), f i - ∑ i ∈ Finset.range n, f i = f n
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>n : ℕ<VAR>AddCommGroup M<GOAL>∑ i ∈ Finset.range (n + 1), f i - f n = ∑ i ∈ Finset.range n, f i
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>n : ℕ<VAR>CommGroup M<GOAL>(∏ i ∈ Finset.range (n + 1), f i) / f n = ∏ i ∈ Finset.range n, f i
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>AddCommGroup M<VAR>hmn : m < n<GOAL>∑ i ∈ Finset.Ico m n, f i - f m = ∑ i ∈ Finset.Ico (m + 1) n, f i
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>CommGroup M<VAR>hmn : m < n<GOAL>(∏ i ∈ Finset.Ico m n, f i) / f m = ∏ i ∈ Finset.Ico (m + 1) n, f i
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>CommGroup M<VAR>hmn : m ≤ n<GOAL>(∏ i ∈ Finset.Ico m (n + 1), f i) / f n = ∏ i ∈ Finset.Ico m n, f i
<VAR>M : Type u_3<VAR>f : ℕ → M<VAR>m n : ℕ<VAR>AddCommGroup M<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Finset.Ico m (n + 1), f i - f n = ∑ i ∈ Finset.Ico m n, f i
<VAR>R : Type u<VAR>Semiring R<VAR>p q : ℕ<VAR>hp : ExpChar R p<VAR>hq : ExpChar R q<GOAL>p = q
<VAR>R : Type u<VAR>Semiring R<VAR>p : ℕ<VAR>q : ℕ<VAR>hq : ExpChar R q<VAR>h : q = p<GOAL>ExpChar R p
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>h : ExpChar R q<GOAL>ringExpChar R = q
<VAR>R : Type u_1<VAR>NonAssocSemiring R<VAR>CharZero R<GOAL>ringExpChar R = 1
<VAR>R : Type u<VAR>Semiring R<VAR>q : ℕ<VAR>hp : CharP R 0<VAR>hq : ExpChar R q<GOAL>q = 1