ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>inst✝ : HasColimit (e.functor ⋙ F)<VAR>this : HasColimit (e.inverse ⋙ e.functor ⋙ F)<GOAL>HasColimit F
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>m✝ : ↥↑(maxTrivSubmodule R L M)<GOAL>↑((maxTrivEquiv LieModuleEquiv.refl) m✝) = ↑(LieModuleEquiv.refl m✝)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : NullMeasurableSet s μ<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : ContinuousAdd 𝕜<VAR>A : Set E<VAR>w : E<VAR>l₁ : E →L[𝕜] 𝕜<VAR>hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>l₂ : E →L[𝕜] 𝕜<VAR>hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<VAR>hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<GOAL>∃ l, {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x} = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : ContinuousAdd 𝕜<VAR>A : Set E<VAR>w : E<VAR>l₁ : E →L[𝕜] 𝕜<VAR>hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>l₂ : E →L[𝕜] 𝕜<VAR>hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<VAR>hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<GOAL>{x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x} ⊆ {x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : ContinuousAdd 𝕜<VAR>A : Set E<VAR>w : E<VAR>l₁ : E →L[𝕜] 𝕜<VAR>hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>hwB : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x}<VAR>l₂ : E →L[𝕜] 𝕜<VAR>hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<VAR>hwC : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}<GOAL>{x | x ∈ A ∧ ∀ y ∈ A, (l₁ + l₂) y ≤ (l₁ + l₂) x} ⊆ {x | x ∈ A ∧ ∀ y ∈ A, l₁ y ≤ l₁ x} ∩ {x | x ∈ A ∧ ∀ y ∈ A, l₂ y ≤ l₂ x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x x✝ : E<GOAL>(sSup ∅) x✝ = ⊥ x✝
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p q : Seminorm 𝕜 E<VAR>x x✝ : E<GOAL>0 = ⊥ x✝
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<VAR>h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<VAR>h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<VAR>x : α<VAR>hx : ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<GOAL>∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<VAR>h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<VAR>x : α<VAR>l : E<VAR>hx : Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<GOAL>∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<VAR>h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<VAR>x : α<VAR>l : E<VAR>hx : Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<VAR>h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x<GOAL>∃ l, Tendsto (fun n => f n x) atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm' (f n - f m) p μ < B N<VAR>h_summable : ∀ᵐ (x : α) ∂μ, Summable fun i => f (i + 1) x - f i x<VAR>h : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) atTop (𝓝 l)<VAR>x : α<VAR>l : E<VAR>hx : Tendsto (fun n => f n x - f 0 x) atTop (𝓝 l)<VAR>h_rw_sum : (fun n => ∑ i ∈ Finset.range n, (f (i + 1) x - f i x)) = fun n => f n x - f 0 x<VAR>hf_rw : (fun n => f n x) = fun n => f n x - f 0 x + f 0 x<GOAL>∃ l, Tendsto (fun n => f n x - f 0 x + f 0 x) atTop (𝓝 l)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>f ≫ (unop Y✝).rightOpLeftOpIso.hom.op = (unop X✝).rightOpLeftOpIso.hom.op ≫ Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.left), right := f.unop.right, w := ⋯ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>f.unop.op ≫ (unop Y✝).rightOpLeftOpIso.hom.op = (unop X✝).rightOpLeftOpIso.hom.op ≫ Quiver.Hom.op { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>((unop Y✝).rightOpLeftOpIso.hom ≫ f.unop).op = ({ left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ } ≫ (unop X✝).rightOpLeftOpIso.hom).op
<VAR>α : Type u_1<VAR>l✝ : List α<VAR>p q : α → Bool<VAR>l : List α<GOAL>countP (fun a => p ↑a) l.attach = countP p l
<VAR>m n✝ n : ℕ<VAR>b : Bool<VAR>hn : n = 0 → b = true<GOAL>(bit b n).bits = b :: n.bits
<VAR>m n✝ n : ℕ<VAR>b : Bool<VAR>hn : n = 0 → b = true<GOAL>[false] = [] ∨ (n = 0 → b = true)
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : 𝓢(ℝ, F)<VAR>x : ℝ<GOAL>|x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>k n : ℕ<VAR>f : 𝓢(ℝ, F)<VAR>x : ℝ<VAR>this : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f<GOAL>|x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : AddCommMonoid S<VAR>f : ℕ → R → S<VAR>h : ∀ (n : ℕ), f n 0 = 0<VAR>n : ℕ<VAR>toFinsupp✝ : AddMonoidAlgebra R ℕ<VAR>w : { toFinsupp := toFinsupp✝ }.natDegree < n<GOAL>{ toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : AddCommMonoid S<VAR>f : ℕ → R → S<VAR>h : ∀ (n : ℕ), f n 0 = 0<VAR>n : ℕ<VAR>toFinsupp✝ : AddMonoidAlgebra R ℕ<VAR>w : { toFinsupp := toFinsupp✝ }.natDegree < n<VAR>this : { toFinsupp := toFinsupp✝ }.support ⊆ range n<GOAL>{ toFinsupp := toFinsupp✝ }.sum f = ∑ a ∈ range n, f a ({ toFinsupp := toFinsupp✝ }.coeff a)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : AddCommMonoid S<VAR>f : ℕ → R → S<VAR>h : ∀ (n : ℕ), f n 0 = 0<VAR>n : ℕ<VAR>toFinsupp✝ : AddMonoidAlgebra R ℕ<VAR>w : { toFinsupp := toFinsupp✝ }.natDegree < n<VAR>this : toFinsupp✝.support ⊆ range n<GOAL>∑ x ∈ toFinsupp✝.support, f x (toFinsupp✝ x) = ∑ x ∈ range n, f x (toFinsupp✝ x)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝ : Category.{u_3, u_2} A<VAR>G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj : G ⊣ sheafToPresheaf J A<GOAL>J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁸ : UniformSpace α<VAR>inst✝⁷ : AddGroup α<VAR>inst✝⁶ : UniformAddGroup α<VAR>inst✝⁵ : UniformSpace β<VAR>inst✝⁴ : AddGroup β<VAR>inst✝³ : UniformAddGroup β<VAR>γ : Type u_5<VAR>inst✝² : AddCommGroup γ<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<GOAL>(f + g).completion ⋯ = f.completion hf + g.completion hg
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁸ : UniformSpace α<VAR>inst✝⁷ : AddGroup α<VAR>inst✝⁶ : UniformAddGroup α<VAR>inst✝⁵ : UniformSpace β<VAR>inst✝⁴ : AddGroup β<VAR>inst✝³ : UniformAddGroup β<VAR>γ : Type u_5<VAR>inst✝² : AddCommGroup γ<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<VAR>hfg : Continuous fun x => f x + g x<GOAL>(f + g).completion ⋯ = f.completion hf + g.completion hg
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁸ : UniformSpace α<VAR>inst✝⁷ : AddGroup α<VAR>inst✝⁶ : UniformAddGroup α<VAR>inst✝⁵ : UniformSpace β<VAR>inst✝⁴ : AddGroup β<VAR>inst✝³ : UniformAddGroup β<VAR>γ : Type u_5<VAR>inst✝² : AddCommGroup γ<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<VAR>hfg : Continuous fun x => f x + g x<VAR>x : Completion α<GOAL>((f + g).completion ⋯) x = (f.completion hf + g.completion hg) x
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁸ : UniformSpace α<VAR>inst✝⁷ : AddGroup α<VAR>inst✝⁶ : UniformAddGroup α<VAR>inst✝⁵ : UniformSpace β<VAR>inst✝⁴ : AddGroup β<VAR>inst✝³ : UniformAddGroup β<VAR>γ : Type u_5<VAR>inst✝² : AddCommGroup γ<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<VAR>hfg : Continuous fun x => f x + g x<VAR>x : Completion α<GOAL>IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁸ : UniformSpace α<VAR>inst✝⁷ : AddGroup α<VAR>inst✝⁶ : UniformAddGroup α<VAR>inst✝⁵ : UniformSpace β<VAR>inst✝⁴ : AddGroup β<VAR>inst✝³ : UniformAddGroup β<VAR>γ : Type u_5<VAR>inst✝² : AddCommGroup γ<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : UniformAddGroup γ<VAR>f g : α →+ γ<VAR>hf : Continuous ⇑f<VAR>hg : Continuous ⇑g<VAR>hfg : Continuous fun x => f x + g x<VAR>x : Completion α<GOAL>∀ (a : α), ((f + g).completion ⋯) (↑α a) = (f.completion hf + g.completion hg) (↑α a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>a x : R<GOAL>x ∈ (p - C a).roots ↔ p ≠ C a ∧ eval x p = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>s : Set α<GOAL>s.ncard ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>s : Set α<GOAL>⋯.toFinset.card ≤ 1
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>α₂ : Sort u_3<VAR>β₂ : Sort u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<VAR>f : α₁ → β₁<VAR>x : α₁<GOAL>(fun f => ⇑e₂.symm ∘ f ∘ ⇑e₁) ((fun f => ⇑e₂ ∘ f ∘ ⇑e₁.symm) f) x = f x
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>α₂ : Sort u_3<VAR>β₂ : Sort u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<VAR>f : α₂ → β₂<VAR>x : α₂<GOAL>(fun f => ⇑e₂ ∘ f ∘ ⇑e₁.symm) ((fun f => ⇑e₂.symm ∘ f ∘ ⇑e₁) f) x = f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝² : DivisionRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<GOAL>Module.rank R M < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<GOAL>⨆ ι, #↑↑ι < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<GOAL>⨆ ι, #↑↑ι < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>S : Finset M<VAR>hS : span R ↑S = ⊤<VAR>i : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>#↑↑i ≤ ↑S.card
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝ : NoZeroSMulDivisors ℤ M<GOAL>InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (range ⇑P.coroot)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))<GOAL>InjOn (⇑((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip)) (range ⇑P.coroot)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : _root_.Finite ι<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ : ι<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>this : InjOn (⇑(span R (range ⇑P.root)).subtype.dualMap) (range (⇑P.toLin.flip ∘ ⇑P.coroot))<VAR>i j : ι<VAR>hij : ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot i) = ((span R (range ⇑P.root)).subtype.dualMap ∘ₗ P.toLin.flip) (P.coroot j)<GOAL>P.coroot i = P.coroot j
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : IntervalIntegrable f volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c - x)) volume (c - a) (c - b)
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<GOAL>ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<GOAL>∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op (ℱ.val.map f₁.op (x g₁ hg₁)) = ℱ.val.map f.op (ℱ.val.map f₂.op (x g₂ hg₂))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<GOAL>ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁)) = ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<VAR>V₁ : C<VAR>iVW : V₁ ⟶ W<VAR>iV₁Y₁ : V₁ ⟶ Y₁<VAR>e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁<GOAL>ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))) = ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<VAR>V₁ : C<VAR>iVW : V₁ ⟶ W<VAR>iV₁Y₁ : V₁ ⟶ Y₁<VAR>e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁<VAR>V₂ : C<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂Y₂ : V₂ ⟶ Y₂<VAR>e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂<GOAL>ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁)))) = ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂))))