ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>∀ (j : J), limMap (whiskerLeft F (restriction R (f ≫ g))) ≫ limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j = (limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).hom) ≫ limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limMap (whiskerLeft F (restriction R (f ≫ g))) ≫ limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j = (limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).hom) ≫ limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (f ≫ g)) ⋯).inv.app ((F.obj j).obj Z) = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g))) ≫ (ModuleCat.restrictScalars (R.map f)).map (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (limit (F ⋙ evaluation R Z))).inv ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).hom ≫ limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (f ≫ g)) ⋯).inv.app ((F.obj j).obj Z) = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g))) ≫ (ModuleCat.restrictScalars (R.map f)).map (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map ((ModuleCat.restrictScalars (R.map g)).map (limit.π (F ⋙ evaluation R Z) j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F ⋙ evaluation R Z).obj j)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g))) ≫ (ModuleCat.restrictScalars (R.map f)).map (preservesLimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map ((ModuleCat.restrictScalars (R.map g)).map (limit.π (F ⋙ evaluation R Z) j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limMap (whiskerLeft F (restriction R g)) ≫ limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (R.map g)) j) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limit.π (F ⋙ evaluation R Y) j ≫ (whiskerLeft F (restriction R g)).app j) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv = limMap (whiskerLeft F (restriction R f)) ≫ (preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (limit.π (F ⋙ evaluation R Y) j ≫ restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>limit.π (F ⋙ evaluation R X) j ≫ restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv = limMap (whiskerLeft F (restriction R f)) ≫ limit.π ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (R.map f)) j ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)<GOAL>Independent p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)<GOAL>∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)<VAR>i : ι<VAR>x : ↥(p i)<VAR>v : Π₀ (i : ι), ↥(p i)<VAR>hv : ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x<GOAL>x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)<VAR>i : ι<VAR>x : ↥(p i)<VAR>v : Π₀ (i : ι), ↥(p i)<VAR>hv : ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ((lsum ℕ) fun i => (p i).subtype) (single i x)<GOAL>x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)<VAR>i : ι<VAR>x : ↥(p i)<VAR>v : Π₀ (i : ι), ↥(p i)<VAR>hv : ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ((lsum ℕ) fun i => (p i).subtype) (single i x)<VAR>this : (erase i v) i = (single i x) i<GOAL>x = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>C.dFrom i = C.d i j ≫ (C.xNextIso r).inv
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i : ι<VAR>r : c.Rel i (c.next i)<GOAL>C.dFrom i = C.d i (c.next i) ≫ (C.xNextIso r).inv
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<GOAL>⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0<VAR>hc : 1 < ‖c‖<VAR>h₀ : r ≠ 0 ∨ x ≠ 0<GOAL>egauge 𝕜 (ball 0 ↑r) x ≤ ↑‖c‖₊ * ↑‖x‖₊ / ↑r
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>hc : 1 < ‖c‖<VAR>h₀ : 0 ≠ 0 ∨ x ≠ 0<GOAL>egauge 𝕜 (ball 0 ↑0) x ≤ ↑‖c‖₊ * ↑‖x‖₊ / ↑0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0<VAR>hc : 1 < ‖c‖<VAR>h₀ : r ≠ 0 ∨ x ≠ 0<VAR>hr : 0 < r<GOAL>egauge 𝕜 (ball 0 ↑r) x ≤ ↑‖c‖₊ * ↑‖x‖₊ / ↑r
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>x.1.card + (op e • x.1).card = 2 * x.1.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>limsup s cofinite = {x | {n | x ∈ s n}.Infinite}
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(coeff A (n + 1)) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff A (n + 1)) (X * exp A)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(coeff A (n + 1, 0).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (coeff A (n + 1, 0).2) (exp A - 1) + ∑ p ∈ antidiagonal n, (coeff A (p.1, p.2 + 1).1) (PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (coeff A (p.1, p.2 + 1).2) (exp A - 1) = (coeff A (n + 1)) (exp A * X)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹) * ↑n ! = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! = ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∀ x ∈ antidiagonal n, bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∀ (x : ℕ × ℕ), x.1 + x.2 = n → bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>i j : ℕ<GOAL>bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! = ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>i j : ℕ<VAR>this : i ! * j ! ∣ (i + j)!<GOAL>bernoulli' (i, j).1 / ↑(i, j).1! * ((↑(i, j).2 + 1) * ↑(i, j).2!)⁻¹ * ↑((i, j).1 + (i, j).2)! = ↑(((i, j).1 + (i, j).2).choose (i, j).2) / (↑(i, j).2 + 1) * bernoulli' (i, j).1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>i j : ℕ<VAR>this : i ! * j ! ∣ (i + j)!<GOAL>((↑j ! * (↑j + 1) = (↑j + 1) * ↑j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>i j : ℕ<VAR>this : i ! * j ! ∣ (i + j)!<GOAL>((j ! * (j + 1) = (j + 1) * j ! ∨ i ! = 0) ∨ (i + j)! = 0) ∨ bernoulli' i = 0
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : CommRing R✝<VAR>n✝ : ℕ<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>μ : R<VAR>n : ℕ<VAR>inst✝¹ : Algebra K R<VAR>hμ : IsPrimitiveRoot μ n<VAR>h : Irreducible (cyclotomic n K)<VAR>inst✝ : NeZero ↑n<GOAL>cyclotomic n K = minpoly K μ
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : CommRing R✝<VAR>n✝ : ℕ<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>μ : R<VAR>n : ℕ<VAR>inst✝¹ : Algebra K R<VAR>hμ : IsPrimitiveRoot μ n<VAR>h : Irreducible (cyclotomic n K)<VAR>inst✝ : NeZero ↑n<VAR>this : NeZero ↑n<GOAL>cyclotomic n K = minpoly K μ
<VAR>R✝ : Type u_1<VAR>inst✝⁵ : CommRing R✝<VAR>n✝ : ℕ<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>R : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>μ : R<VAR>n : ℕ<VAR>inst✝¹ : Algebra K R<VAR>hμ : IsPrimitiveRoot μ n<VAR>h : Irreducible (cyclotomic n K)<VAR>inst✝ : NeZero ↑n<VAR>this : NeZero ↑n<GOAL>(aeval μ) (cyclotomic n K) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = b ∆ a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : range f = ⊤<VAR>p : Submodule R M<GOAL>map f p = ⊤ ↔ p ⊔ ker f = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommGroup M<VAR>inst✝ : TopologicalAddGroup M<VAR>v w : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>h : v.restrict i ≤ w.restrict i<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<GOAL>↑((-w).restrict i) j ≤ ↑((-v).restrict i) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommGroup M<VAR>inst✝ : TopologicalAddGroup M<VAR>v w : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>h : v.restrict i ≤ w.restrict i<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<GOAL>-↑w (j ∩ i) ≤ -↑v (j ∩ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommGroup M<VAR>inst✝ : TopologicalAddGroup M<VAR>v w : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>h : v.restrict i ≤ w.restrict i<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<GOAL>↑v (j ∩ i) ≤ ↑w (j ∩ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommGroup M<VAR>inst✝ : TopologicalAddGroup M<VAR>v w : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>h : v.restrict i ≤ w.restrict i<VAR>j : Set α<VAR>hj₁ : MeasurableSet j<GOAL>↑(v.restrict i) j ≤ ↑(w.restrict i) j
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → β → α<VAR>a : α<VAR>hf : ∀ (b : β), f a b = a<VAR>b : β<VAR>l : List β<GOAL>foldl f a (b :: l) = a
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r
<VAR>α : Type w<VAR>inst✝ : Finite α<VAR>X : α → Profinite<VAR>a : α<VAR>x y : (forget Profinite).obj (X a)<VAR>hxy : (ι X a) x = (ι X a) y<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>hr : WellFounded (rᶜ ⊓ fun x x_1 => x ≠ x_1)<VAR>x : Π₀ (i : ι), α i<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : Cᵒᵖ<GOAL>colimMap (J.diagramNatTrans (𝟙 P) (unop x✝)) = (𝟙 { obj := fun X => colimit (J.diagram P (unop X)), map := fun {X Y} f => colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op, map_id := ⋯, map_comp := ⋯ }).app x✝
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>x✝ : Cᵒᵖ<GOAL>colimMap (𝟙 (J.diagram P (unop x✝))) = 𝟙 ({ obj := fun X => colimit (J.diagram P (unop X)), map := fun {X Y} f => colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op, map_id := ⋯, map_comp := ⋯ }.obj x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>f : β → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>(∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>f : β → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha : a ≠ ⊤<GOAL>(∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>x : ℕ<GOAL>x ≤ ⌊max 0 (↑x + 1)⌋₊
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p * q) = ↑p * ↑q
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p.den * q.den) ≠ 0
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>a : α<VAR>b : ↥(zpowers a)<GOAL>↑b ^ orderOf a = 1
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>hn : ∀ (n : ℕ), 0 < n → (filter (fun a => a ^ n = 1) univ).card ≤ n<VAR>a : α<VAR>b : ↥(zpowers a)<VAR>i : ℤ<VAR>hi : (fun x => a ^ x) i = ↑b<GOAL>↑b ^ orderOf a = 1
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>R : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : MulSemiringAction M R<VAR>S : Type u_3<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : MulSemiringAction M S<VAR>m : M<VAR>f : S[X]<VAR>x r : S<GOAL>eval (m • x) (m • C r) = m • eval x (C r)
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>R : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : MulSemiringAction M R<VAR>S : Type u_3<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : MulSemiringAction M S<VAR>m : M<VAR>f✝ : S[X]<VAR>x : S<VAR>f g : S[X]<VAR>ihf : eval (m • x) (m • f) = m • eval x f<VAR>ihg : eval (m • x) (m • g) = m • eval x g<GOAL>eval (m • x) (m • (f + g)) = m • eval x (f + g)
<VAR>M : Type u_1<VAR>inst✝⁴ : Monoid M<VAR>R : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : MulSemiringAction M R<VAR>S : Type u_3<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : MulSemiringAction M S<VAR>m : M<VAR>f : S[X]<VAR>x : S<VAR>n : ℕ<VAR>r : S<VAR>x✝ : eval (m • x) (m • (C r * X ^ n)) = m • eval x (C r * X ^ n)<GOAL>eval (m • x) (m • (C r * X ^ (n + 1))) = m • eval x (C r * X ^ (n + 1))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : IndepFun f g μ<VAR>hf : f =ᶠ[ae μ] f'<VAR>hg : g =ᶠ[ae μ] g'<GOAL>IndepFun f' g' μ