ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>CommGroup α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).alternatingProd = a / l.alternatingProd
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>l.sum % n = (List.map (fun x => x % n) l).sum % n
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>l.prod % n = (List.map (fun x => x % n) l).prod % n
<VAR>l : List ℤ<VAR>n : ℤ<GOAL>l.sum % n = (List.map (fun x => x % n) l).sum % n
<VAR>l : List ℤ<VAR>n : ℤ<GOAL>l.prod % n = (List.map (fun x => x % n) l).prod % n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>p : α → Bool<VAR>l : List α<GOAL>(List.map (fun x => List.count x l) (List.filter p l.dedup)).sum = List.countP p l
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>l : List α<GOAL>(List.map (fun x => List.count x l) l.dedup).sum = l.length
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>F : Type u_8<VAR>FunLike F M N<VAR>AddMonoidHomClass F M N<VAR>f : F<VAR>l : List M<GOAL>f l.sum = (List.map (⇑f) l).sum
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>F : Type u_8<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>f : F<VAR>l : List M<GOAL>f l.prod = (List.map (⇑f) l).prod
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddMonoid M<VAR>AddMonoid N<VAR>f : M →+ N<VAR>l : List M<GOAL>f l.sum = (List.map (⇑f) l).sum
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>l : List M<GOAL>f l.prod = (List.map (⇑f) l).prod
<VAR>l : List ℕ<GOAL>Nat.sum l = l.sum
<VAR>α : Type u_2<VAR>σ : α → Type u_8<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>(l₁.sigma l₂).length = (List.map (fun a => (l₂ a).length) l₁).sum
<VAR>l : List ℕ<GOAL>l.ranges.join = List.range l.sum
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>(∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum
<VAR>α : Type u_2<VAR>L : List (List α)<GOAL>L.join.length = (List.map List.length L).sum
<VAR>α : Type u_2<VAR>p : α → Bool<VAR>L : List (List α)<GOAL>List.countP p L.join = (List.map (List.countP p) L).sum
<VAR>α : Type u_2<VAR>BEq α<VAR>L : List (List α)<VAR>a : α<GOAL>List.count a L.join = (List.map (List.count a) L).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : List α<VAR>f : α → List β<GOAL>(l.bind f).length = (List.map (List.length ∘ f) l).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>p : β → Bool<VAR>l : List α<VAR>f : α → List β<GOAL>List.countP p (l.bind f) = (List.map (List.countP p ∘ f) l).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BEq β<VAR>l : List α<VAR>f : α → List β<VAR>x : β<GOAL>List.count x (l.bind f) = (List.map (List.count x ∘ f) l).sum
<VAR>α : Type u_2<VAR>L : List (List α)<VAR>i : ℕ<GOAL>List.take (List.take i (List.map List.length L)).sum L.join = (List.take i L).join
<VAR>α : Type u_2<VAR>L : List (List α)<VAR>i : ℕ<GOAL>List.drop (List.take i (List.map List.length L)).sum L.join = (List.drop i L).join
<VAR>α : Type u_2<VAR>L : List (List α)<VAR>i : ℕ<VAR>h : i < L.length<GOAL>List.drop (List.take i (List.map List.length L)).sum (List.take (List.take (i + 1) (List.map List.length L)).sum L.join) = L[i]
<VAR>α : Type u_2<VAR>L : List (List α)<VAR>i : Fin L.length<GOAL>List.drop (List.take (↑i) (List.map List.length L)).sum (List.take (List.take (↑i + 1) (List.map List.length L)).sum L.join) = L.get i
<VAR>l : List ℤ<VAR>h : l.prod = -1<GOAL>-1 ∈ l
<VAR>L : List ℕ<VAR>h : ∀ i ∈ L, 1 ≤ i<GOAL>L.length ≤ L.sum
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>a : M<VAR>l : List M<VAR>ha : a ∈ l<GOAL>a ∣ l.prod
<VAR>M : Type u_4<VAR>CommMonoid M<VAR>l₁ l₂ : List M<VAR>h : l₁ <+ l₂<GOAL>l₁.prod ∣ l₂.prod
<VAR>α : Type u_2<VAR>CommGroup α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length
<VAR>α : Type u_2<VAR>AddCommGroup α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).alternatingSum = l₁.alternatingSum + (-1) ^ l₁.length • l₂.alternatingSum
<VAR>α : Type u_2<VAR>AddCommGroup α<VAR>l : List α<GOAL>l.reverse.alternatingSum = (-1) ^ (l.length + 1) • l.alternatingSum
<VAR>α : Type u_2<VAR>CommGroup α<VAR>l : List α<GOAL>l.reverse.alternatingProd = l.alternatingProd ^ (-1) ^ (l.length + 1)
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List M<GOAL>MulOpposite.op l.prod = (List.map MulOpposite.op l).reverse.prod
<VAR>M : Type u_4<VAR>Monoid M<VAR>l : List Mᵐᵒᵖ<GOAL>MulOpposite.unop l.prod = (List.map MulOpposite.unop l).reverse.prod
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>F : Type u_8<VAR>FunLike F M Nᵐᵒᵖ<VAR>MonoidHomClass F M Nᵐᵒᵖ<VAR>f : F<VAR>l : List M<GOAL>MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* Nᵐᵒᵖ<VAR>l : List M<GOAL>MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>c : RingCon A<VAR>s : S<GOAL>↑((algebraMap S A) s) = (algebraMap S c.Quotient) s
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : RingQuot.Rel r b c<GOAL>RingQuot.Rel r (a + b) (a + c)
<VAR>R : Type uR<VAR>Ring R<VAR>r : R → R → Prop<VAR>a b : R<VAR>h : RingQuot.Rel r a b<GOAL>RingQuot.Rel r (-a) (-b)
<VAR>R : Type uR<VAR>Ring R<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : RingQuot.Rel r a b<GOAL>RingQuot.Rel r (a - c) (b - c)
<VAR>R : Type uR<VAR>Ring R<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : RingQuot.Rel r b c<GOAL>RingQuot.Rel r (a - b) (a - c)
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>r : A → A → Prop<VAR>k : S<VAR>a b : A<VAR>h : RingQuot.Rel r a b<GOAL>RingQuot.Rel r (k • a) (k • b)
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>EqvGen (RingQuot.Rel r) = RingConGen.Rel r
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>RingQuot.zero r = { toQuot := Quot.mk (RingQuot.Rel r) 0 }
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>RingQuot.one r = { toQuot := Quot.mk (RingQuot.Rel r) 1 }
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>∀ (x x_1 : RingQuot r), RingQuot.add r x x_1 = match x, x_1 with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x x_2 => x + x_2) ⋯ ⋯ a b }
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>∀ (x x_1 : RingQuot r), RingQuot.mul r x x_1 = match x, x_1 with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x x_2 => x * x_2) ⋯ ⋯ a b }
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R → R → Prop<GOAL>∀ (x : RingQuot r), RingQuot.neg r x = match x with | { toQuot := a } => { toQuot := Quot.map (fun a => -a) ⋯ a }
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R → R → Prop<GOAL>∀ (x x_1 : RingQuot r), RingQuot.sub r x x_1 = match x, x_1 with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ Sub.sub ⋯ ⋯ a b }
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<VAR>n : ℕ<GOAL>∀ (x : RingQuot r), RingQuot.npow r n x = match x with | { toQuot := a } => { toQuot := Quot.lift (fun a => Quot.mk (RingQuot.Rel r) (a ^ n)) ⋯ a }
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) 0 } = 0
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) 1 } = 1
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<VAR>a b : R<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a + b) }
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<VAR>a b : R<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a * b) }
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<VAR>a : R<VAR>n : ℕ<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) a } ^ n = { toQuot := Quot.mk (RingQuot.Rel r) (a ^ n) }
<VAR>R : Type uR<VAR>Ring R<VAR>r : R → R → Prop<VAR>a : R<GOAL>-{ toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (-a) }
<VAR>R : Type uR<VAR>Ring R<VAR>r : R → R → Prop<VAR>a b : R<GOAL>{ toQuot := Quot.mk (RingQuot.Rel r) a } - { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a - b) }
<VAR>R : Type uR<VAR>Semiring R<VAR>S : Type uS<VAR>CommSemiring S<VAR>r : R → R → Prop<VAR>Algebra S R<VAR>n : S<VAR>a : R<GOAL>n • { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (n • a) }
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>RingQuot.mkRingHom r = { toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<VAR>x y : R<VAR>w : r x y<GOAL>(RingQuot.mkRingHom r) x = (RingQuot.mkRingHom r) y
<VAR>R : Type uR<VAR>Semiring R<VAR>r : R → R → Prop<GOAL>Function.Surjective ⇑(RingQuot.mkRingHom r)
<VAR>R : Type uR<VAR>Semiring R<VAR>T : Type uT<VAR>Semiring T<VAR>r : R → R → Prop<VAR>f g : RingQuot r →+* T<VAR>w : f.comp (RingQuot.mkRingHom r) = g.comp (RingQuot.mkRingHom r)<GOAL>f = g
<VAR>R : Type u_1<VAR>Semiring R<VAR>T : Type u_2<VAR>Semiring T<VAR>r : R → R → Prop<VAR>f : R →+* T<VAR>h : ∀ ⦃x y : R⦄, r x y → f x = f y<GOAL>RingQuot.preLift h = { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
<VAR>R : Type u_1<VAR>Semiring R<VAR>T : Type u_2<VAR>Semiring T<VAR>r : R → R → Prop<GOAL>RingQuot.lift = { toFun := fun f => RingQuot.preLift ⋯, invFun := fun F => ⟨F.comp (RingQuot.mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
<VAR>R : Type uR<VAR>Semiring R<VAR>T : Type uT<VAR>Semiring T<VAR>f : R →+* T<VAR>r : R → R → Prop<VAR>w : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>x : R<GOAL>(RingQuot.lift ⟨f, w⟩) ((RingQuot.mkRingHom r) x) = f x
<VAR>R : Type uR<VAR>Semiring R<VAR>T : Type uT<VAR>Semiring T<VAR>f : R →+* T<VAR>r : R → R → Prop<VAR>w : ∀ ⦃x y : R⦄, r x y → f x = f y<VAR>g : RingQuot r →+* T<VAR>h : g.comp (RingQuot.mkRingHom r) = f<GOAL>g = RingQuot.lift ⟨f, w⟩
<VAR>R : Type uR<VAR>Semiring R<VAR>T : Type uT<VAR>Semiring T<VAR>r : R → R → Prop<VAR>f : RingQuot r →+* T<GOAL>f = RingQuot.lift ⟨f.comp (RingQuot.mkRingHom r), ⋯⟩
<VAR>B : Type uR<VAR>CommRing B<VAR>r : B → B → Prop<VAR>x : B<GOAL>(RingQuot.ringQuotToIdealQuotient r) ((RingQuot.mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
<VAR>B : Type uR<VAR>CommRing B<VAR>r : B → B → Prop<VAR>x : B<GOAL>(RingQuot.idealQuotientToRingQuot r) ((Ideal.Quotient.mk (Ideal.ofRel r)) x) = (RingQuot.mkRingHom r) x
<VAR>S : Type u_1<VAR>CommSemiring S<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>s : A → A → Prop<GOAL>RingQuot.mkAlgHom S s = let __src := RingQuot.mkRingHom s; { toRingHom := __src, commutes' := ⋯ }
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>s : A → A → Prop<GOAL>↑(RingQuot.mkAlgHom S s) = RingQuot.mkRingHom s
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>s : A → A → Prop<VAR>x y : A<VAR>w : s x y<GOAL>(RingQuot.mkAlgHom S s) x = (RingQuot.mkAlgHom S s) y
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>s : A → A → Prop<GOAL>Function.Surjective ⇑(RingQuot.mkAlgHom S s)
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u₄<VAR>Semiring B<VAR>Algebra S B<VAR>s : A → A → Prop<VAR>f g : RingQuot s →ₐ[S] B<VAR>w : f.comp (RingQuot.mkAlgHom S s) = g.comp (RingQuot.mkAlgHom S s)<GOAL>f = g
<VAR>S : Type u_1<VAR>CommSemiring S<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u_3<VAR>Semiring B<VAR>Algebra S B<VAR>s : A → A → Prop<VAR>f : A →ₐ[S] B<VAR>h : ∀ ⦃x y : A⦄, s x y → f x = f y<GOAL>RingQuot.preLiftAlgHom S h = { toFun := fun x => Quot.lift ⇑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
<VAR>S : Type u_1<VAR>CommSemiring S<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u_3<VAR>Semiring B<VAR>Algebra S B<VAR>s : A → A → Prop<GOAL>RingQuot.liftAlgHom S = { toFun := fun f' => RingQuot.preLiftAlgHom S ⋯, invFun := fun F => ⟨F.comp (RingQuot.mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u₄<VAR>Semiring B<VAR>Algebra S B<VAR>f : A →ₐ[S] B<VAR>s : A → A → Prop<VAR>w : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>x : A<GOAL>((RingQuot.liftAlgHom S) ⟨f, w⟩) ((RingQuot.mkAlgHom S s) x) = f x
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u₄<VAR>Semiring B<VAR>Algebra S B<VAR>f : A →ₐ[S] B<VAR>s : A → A → Prop<VAR>w : ∀ ⦃x y : A⦄, s x y → f x = f y<VAR>g : RingQuot s →ₐ[S] B<VAR>h : g.comp (RingQuot.mkAlgHom S s) = f<GOAL>g = (RingQuot.liftAlgHom S) ⟨f, w⟩
<VAR>S : Type uS<VAR>CommSemiring S<VAR>A : Type uA<VAR>Semiring A<VAR>Algebra S A<VAR>B : Type u₄<VAR>Semiring B<VAR>Algebra S B<VAR>s : A → A → Prop<VAR>f : RingQuot s →ₐ[S] B<GOAL>f = (RingQuot.liftAlgHom S) ⟨f.comp (RingQuot.mkAlgHom S s), ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>m n : ℕ<VAR>hmn : m < n<GOAL>∑ i ∈ Finset.Ico m n, f i • g i = f (n - 1) • ∑ i ∈ Finset.range n, g i - f m • ∑ i ∈ Finset.range m, g i - ∑ i ∈ Finset.Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : ℕ → R<VAR>g : ℕ → M<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, f i • g i = f (n - 1) • ∑ i ∈ Finset.range n, g i - ∑ i ∈ Finset.range (n - 1), (f (i + 1) - f i) • ∑ i ∈ Finset.range (i + 1), g i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>CommRing A<VAR>Algebra R A<VAR>GCDMonoid R<VAR>M : Submonoid R<VAR>IsLocalization M A<VAR>z : A<GOAL>∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<GOAL>s.lcm f = (Multiset.map f s.val).lcm
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<GOAL>∅.lcm f = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ b ∈ s, f b ∣ a) → s.lcm f ∣ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>hb : b ∈ s<GOAL>f b ∣ s.lcm f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).lcm f = lcm (f b) (s.lcm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<VAR>b : β<GOAL>{b}.lcm f = normalize (f b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<GOAL>normalize (s.lcm f) = s.lcm f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>DecidableEq β<GOAL>(s₁ ∪ s₂).lcm f = lcm (s₁.lcm f) (s₂.lcm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f g : β → α<VAR>hs : s₁ = s₂<VAR>hfg : ∀ a ∈ s₂, f a = g a<GOAL>s₁.lcm f = s₂.lcm g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f g : β → α<VAR>h : ∀ b ∈ s, f b ∣ g b<GOAL>s.lcm f ∣ s.lcm g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.lcm f ∣ s₂.lcm f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<VAR>DecidableEq β<VAR>g : γ → β<VAR>s : Finset γ<GOAL>(Finset.image g s).lcm f = s.lcm (f ∘ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq α<GOAL>s.lcm f = (Finset.image f s).lcm id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>Nontrivial α<GOAL>s.lcm f = 0 ↔ 0 ∈ f '' ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<GOAL>s.gcd f = (Multiset.map f s.val).gcd
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<GOAL>∅.gcd f = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>hb : b ∈ s<GOAL>s.gcd f ∣ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).gcd f = gcd (f b) (s.gcd f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<VAR>b : β<GOAL>{b}.gcd f = normalize (f b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<GOAL>normalize (s.gcd f) = s.gcd f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>DecidableEq β<GOAL>(s₁ ∪ s₂).gcd f = gcd (s₁.gcd f) (s₂.gcd f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f g : β → α<VAR>hs : s₁ = s₂<VAR>hfg : ∀ a ∈ s₂, f a = g a<GOAL>s₁.gcd f = s₂.gcd g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f g : β → α<VAR>h : ∀ b ∈ s, f b ∣ g b<GOAL>s.gcd f ∣ s.gcd g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>h : s₁ ⊆ s₂<GOAL>s₂.gcd f ∣ s₁.gcd f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>f : β → α<VAR>DecidableEq β<VAR>g : γ → β<VAR>s : Finset γ<GOAL>(Finset.image g s).gcd f = s.gcd (f ∘ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq α<GOAL>s.gcd f = (Finset.image f s).gcd id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<GOAL>s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidablePred fun x => f x = 0<GOAL>s.gcd f = (Finset.filter (fun x => f x ≠ 0) s).gcd f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(s.gcd fun x => a * f x) = normalize a * s.gcd f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(s.gcd fun x => f x * a) = s.gcd f * normalize a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f g : β → α<VAR>hs : ∃ x ∈ s, f x ≠ 0<VAR>hg : ∀ b ∈ s, f b = s.gcd f * g b<GOAL>s.gcd g = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f : β → α<VAR>hs : s.Nonempty<GOAL>∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>Div α<VAR>MulDivCancelClass α<VAR>f : ι → α<VAR>s : Finset ι<VAR>i : ι<VAR>his : i ∈ s<VAR>hfi : f i ≠ 0<GOAL>(s.gcd fun j => f j / s.gcd f) = 1
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>Div α<VAR>MulDivCancelClass α<VAR>s : Finset α<VAR>a : α<VAR>has : a ∈ s<VAR>ha : a ≠ 0<GOAL>(s.gcd fun b => b / s.gcd id) = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommRing α<VAR>IsDomain α<VAR>NormalizedGCDMonoid α<VAR>s : Finset β<VAR>f g : β → α<VAR>a : α<VAR>h : ∀ x ∈ s, a ∣ f x - g x<GOAL>gcd a (s.gcd f) = gcd a (s.gcd g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoidWithOne α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>s : Finset ι<GOAL>↑(Finset.filter p s).card = ∑ a ∈ s, if p a then 1 else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoidWithOne α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>s : Finset ι<GOAL>(∑ x ∈ s, if p x then 1 else 0) = ↑(Finset.filter p s).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>κ : Type u_6<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>(∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>κ : Type u_6<VAR>Fintype ι<VAR>Fintype κ<VAR>f : ι → α<VAR>g : κ → α<GOAL>(∑ i : ι, f i) * ∑ j : κ, g j = ∑ i : ι, ∑ j : κ, f i * g j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>b : α<VAR>h : ∀ i ∈ s, Commute b (f i)<GOAL>Commute b (∑ i ∈ s, f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>b : α<VAR>h : ∀ i ∈ s, Commute (f i) b<GOAL>Commute (∑ i ∈ s, f i) b
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>m n : ℕ<VAR>f g : ℕ → α<GOAL>(∑ i ∈ Finset.range (m + 1), f i) * ∑ i ∈ Finset.range (n + 1), g i = (∑ i ∈ Finset.range m, f i) * ∑ i ∈ Finset.range n, g i + f m * ∑ i ∈ Finset.range n, g i + (∑ i ∈ Finset.range m, f i) * g n + f m * g n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : Finset ι<VAR>a : α<VAR>f : ι → α<VAR>NonUnitalSemiring α<VAR>h : ∀ i ∈ s, a ∣ f i<GOAL>a ∣ ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : ι<GOAL>(∑ j ∈ s, f j * if i = j then 1 else 0) = if i ∈ s then f i else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonAssocSemiring α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : ι<GOAL>∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>s : Finset ι<VAR>i : ι<VAR>f g h : ι → α<VAR>hi : i ∈ s<VAR>h1 : g i + h i = f i<VAR>h2 : ∀ j ∈ s, j ≠ i → g j = f j<VAR>h3 : ∀ j ∈ s, j ≠ i → h j = f j<GOAL>∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>CommSemiring α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>κ : ι → Type u_5<VAR>CommSemiring α<VAR>DecidableEq ι<VAR>Fintype ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>∏ i : ι, ∑ j ∈ t i, f i j = ∑ x ∈ Fintype.piFinset t, ∏ i : ι, f i (x i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>DecidableEq ι<VAR>κ : Type u_6<VAR>Fintype ι<VAR>s : Finset κ<VAR>g : ι → κ → α<GOAL>∑ f ∈ Fintype.piFinset fun x => s, ∏ i : ι, g i (f i) = ∏ i : ι, ∑ j ∈ s, g i j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ a ∈ s, f a) ^ n = ∑ p ∈ Fintype.piFinset fun _i => s, ∏ i : Fin n, f (p i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>DecidableEq ι<VAR>f g : ι → α<VAR>s : Finset ι<GOAL>∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>LinearOrder ι<VAR>CommSemiring α<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ Finset.filter (fun x => x < i) s, (f j + g j)) * ∏ j ∈ Finset.filter (fun j => i < j) s, f j