ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<VAR>hd : DifferentiableWithinAt 𝕜 f s b<GOAL>dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<VAR>hd : DifferentiableWithinAt 𝕜 f s b<GOAL>{a}ᶜ ∈ 𝓝[s] b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : UpperSet α<VAR>t t₁ t₂ : UpperSet β<VAR>x : α × β<GOAL>Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>k : Rˣ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>(k • z₁).comp z₂ h = k • z₁.comp z₂ h
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a
<VAR>m n k : ℕ<GOAL>m.Coprime (k * m + n) ↔ m.Coprime n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<GOAL>atBot ≤ 𝓝 ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<GOAL>pure ⊥ ≤ 𝓝 ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>μ : Measure α<GOAL>∑ y ∈ f.range, μ (↑f ⁻¹' {y}) = μ univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<GOAL>s.min = ⊤ ↔ s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite (μ.trim hm)<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n<VAR>hs_univ : ⋃ i, s i = univ<GOAL>∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n<VAR>hs_univ : ⋃ i, s i = univ<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s n<GOAL>‖f x‖ ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n<VAR>hs_univ : ⋃ i, s i = univ<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s n<VAR>hx_nnnorm : ‖f x‖₊ ≤ ↑n<GOAL>‖f x‖ ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : SeminormedAddCommGroup β<VAR>m m0 : MeasurableSpace α<VAR>hm : m ≤ m0<VAR>hf : StronglyMeasurable f<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n<VAR>hs_univ : ⋃ i, s i = univ<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ s n<VAR>hx_nnnorm : ‖f x‖₊ ≤ ↑n<GOAL>↑‖f x‖₊ ≤ ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Orthonormal 𝕜 fun i => gramSchmidtNormed 𝕜 f ↑i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Pairwise fun i j => ⟪(fun i => gramSchmidtNormed 𝕜 f ↑i) i, (fun i => gramSchmidtNormed 𝕜 f ↑i) j⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}<VAR>hij : ¬i = j<GOAL>⟪(fun i => gramSchmidtNormed 𝕜 f ↑i) i, (fun i => gramSchmidtNormed 𝕜 f ↑i) j⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ↑{i | gramSchmidtNormed 𝕜 f i ≠ 0}<VAR>hij : ¬↑i = ↑j<GOAL>⟪(fun i => gramSchmidtNormed 𝕜 f ↑i) i, (fun i => gramSchmidtNormed 𝕜 f ↑i) j⟫_𝕜 = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish (q + 1) φ<VAR>j : Fin (n + 1)<VAR>hj : n + 1 ≤ ↑j + q<GOAL>n + 1 ≤ ↑j + (q + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c • f' x) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => c • f' x) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => ‖c • f' x‖) =o[l] g ↔ f' =o[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => ‖c‖ * ‖f' x‖) =o[l] g ↔ f' =o[l] g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y<GOAL>HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) t y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y<GOAL>HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) t y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y<VAR>this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y<GOAL>HasDerivWithinAt (fun z => (((↑k + 1) * ↑k !)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z) ((((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) t y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y<VAR>this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y<GOAL>(((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y - ((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y = (((↑k + 1) * ↑k !)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y + -((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x y : ℝ<VAR>k : ℕ<VAR>s t : Set ℝ<VAR>ht : UniqueDiffWithinAt ℝ t y<VAR>hs : s ∈ 𝓝[t] y<VAR>hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y<VAR>this : HasDerivWithinAt (fun t => ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (-((↑k !)⁻¹ * (x - y) ^ k)) t y<GOAL>((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y - ((x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y = ((x - y) ^ (k + 1) / ((↑k + 1) * ↑k !)) • iteratedDerivWithin (k + 2) f s y + (-(x - y) ^ k / ↑k !) • iteratedDerivWithin (k + 1) f s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>s : Set β<VAR>inst✝ : MeasurableSpace β<VAR>hs : MeasurableSet s<GOAL>(p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toMeasure s
<VAR>L : Language<VAR>α : Type w<VAR>V : Type w'<VAR>n : ℕ<VAR>G : SimpleGraph V<VAR>x✝¹ x✝ : V<GOAL>(FirstOrder.Language.simpleGraphOfStructure V).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>h : covolume (↥Γ.op) G ν = μ univ<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>h : covolume (↥Γ.op) G ν = μ univ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>h : covolume (↥Γ.op) G ν = μ univ<VAR>s : Set G<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>s : Set G<VAR>h : ν s = μ univ<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>s : Set G<VAR>h : ν s = μ univ<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<VAR>meas_s_ne_zero : ¬ν s = 0<GOAL>QuotientMeasureEqMeasurePreimage ν μ
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>s : Set G<VAR>h : ν s = μ univ<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<VAR>meas_s_ne_zero : ¬ν s = 0<GOAL>μ univ ≠ 0
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>s : Set G<VAR>h : ν s = μ univ<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<VAR>meas_s_ne_zero : ¬ν s = 0<GOAL>μ univ = ν (QuotientGroup.mk ⁻¹' univ ∩ s)
<VAR>G : Type u_1<VAR>inst✝¹⁵ : Group G<VAR>inst✝¹⁴ : MeasurableSpace G<VAR>inst✝¹³ : TopologicalSpace G<VAR>inst✝¹² : TopologicalGroup G<VAR>inst✝¹¹ : BorelSpace G<VAR>inst✝¹⁰ : PolishSpace G<VAR>Γ : Subgroup G<VAR>inst✝⁹ : Countable ↥Γ<VAR>inst✝⁸ : Γ.Normal<VAR>inst✝⁷ : T2Space (G ⧸ Γ)<VAR>inst✝⁶ : SecondCountableTopology (G ⧸ Γ)<VAR>μ : Measure (G ⧸ Γ)<VAR>ν : Measure G<VAR>inst✝⁵ : ν.IsMulLeftInvariant<VAR>inst✝⁴ : ν.IsMulRightInvariant<VAR>inst✝³ : SigmaFinite ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hasFun : HasFundamentalDomain (↥Γ.op) G ν<VAR>s : Set G<VAR>h : ν s = μ univ<VAR>fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν<VAR>finiteCovol : μ univ < ⊤<VAR>meas_s_ne_zero : ¬ν s = 0<GOAL>μ univ ≠ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<GOAL>s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<GOAL>s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.33498, u_2} D<VAR>E : Type u_3<VAR>inst✝⁶ : Category.{?u.33505, u_3} E<VAR>M : Type u_4<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : HasShift E M<VAR>X Y Z T : C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (a : M), (shiftFunctor C a).Additive<VAR>a b c : M<VAR>α : ShiftedHom X Y a<VAR>β₁ β₂ : ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n j : ℕ<VAR>hj : j < p ^ n<GOAL>p ^ (n - v p ⟨j + 1, ⋯⟩) ∣ (p ^ n).choose (j + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n j : ℕ<VAR>hj : j < p ^ n<GOAL>↑(n - v p ⟨j + 1, ⋯⟩) ≤ multiplicity p ((p ^ n).choose (j + 1))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n j : ℕ<VAR>hj : j < p ^ n<GOAL>↑(n - v p ⟨j + 1, ⋯⟩) ≤ ↑(n - (multiplicity p j.succ).get ⋯)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r : R<VAR>hr : r ≠ 0<VAR>I : ↑{I | I ∈ normalizedFactors (span {r})}<GOAL>multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r : R<VAR>hr : r ≠ 0<VAR>I : ↑{I | I ∈ normalizedFactors (span {r})}<VAR>x : ↑{d | d ∈ normalizedFactors r}<VAR>hx : (normalizedFactorsEquivSpanNormalizedFactors hr) x = I<GOAL>multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r : R<VAR>hr : r ≠ 0<VAR>I : ↑{I | I ∈ normalizedFactors (span {r})}<VAR>a : R<VAR>ha : a ∈ {d | d ∈ normalizedFactors r}<VAR>hx : (normalizedFactorsEquivSpanNormalizedFactors hr) ⟨a, ha⟩ = I<GOAL>multiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r = multiplicity (↑I) (span {r})
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>inst✝ : S.HasHomology<GOAL>S.homology ≅ S.opcycles
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>inst✝ : S.HasHomology<VAR>this : IsIso S.homologyι<GOAL>S.homology ≅ S.opcycles