ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t K : Set X<VAR>l : Filter Y<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l<VAR>x : X<VAR>hx : x ∈ K<GOAL>∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<GOAL>add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>h₁ : 𝟙 X' ≫ add W eX eY f₁ f₂ = add W eX' eY (𝟙 X' ≫ f₁) (𝟙 X' ≫ f₂)<GOAL>add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>h₁ : 𝟙 X' ≫ add W eX eY f₁ f₂ = add W eX' eY (𝟙 X' ≫ f₁) (𝟙 X' ≫ f₂)<VAR>h₂ : add W eX' eY f₁ f₂ ≫ 𝟙 Y' = add W eX' eY' (f₁ ≫ 𝟙 Y') (f₂ ≫ 𝟙 Y')<GOAL>add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>h₂ : add W eX' eY f₁ f₂ ≫ 𝟙 Y' = add W eX' eY' (f₁ ≫ 𝟙 Y') (f₂ ≫ 𝟙 Y')<VAR>h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂<GOAL>add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂<VAR>h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂<GOAL>add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) ρ<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)<GOAL>∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>m : β → γ<VAR>hh : Monotone h<GOAL>f.lift (map m ∘ 𝓟 ∘ h) = f.lift' (image m ∘ h)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>Xs Ys : ι → Set α<VAR>A : Set ι<VAR>h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)<GOAL>M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<GOAL>IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<GOAL>∀ u ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}, IsOpen u
<VAR>X✝ Y Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f) g<VAR>X : Scheme<GOAL>∀ (a : ↑↑X.toPresheafedSpace) (u : Set ↑↑X.toPresheafedSpace), a ∈ u → IsOpen u → ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}, a ∈ v ∧ v ⊆ u
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ : α<VAR>z a : ℤ<GOAL>a ≤ ⌊↑z⌋ ↔ a ≤ z
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>(∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) (as.get i)) ↔ ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) (bs.get i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<VAR>e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ := fun i => QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯<GOAL>(∀ (i : Fin as.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) as) • ⊤) (as.get i)) ↔ ∀ (i : Fin bs.length), IsSMulRegular (M₂ ⧸ Ideal.ofList (List.take (↑i) bs) • ⊤) (bs.get i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<VAR>e' : (i : ℕ) → M ⧸ Ideal.ofList (List.take i as) • ⊤ ≃+ M₂ ⧸ Ideal.ofList (List.take i bs) • ⊤ := fun i => QuotientAddGroup.congr (Ideal.ofList (List.take i as) • ⊤).toAddSubgroup (Ideal.ofList (List.take i bs) • ⊤).toAddSubgroup e ⋯<VAR>x✝ : Fin as.length<GOAL>∀ (x : M ⧸ Ideal.ofList (List.take (↑x✝) as) • ⊤), (e' ↑x✝).toEquiv (as.get x✝ • x) = bs.get ((finCongr ⋯) x✝) • (e' ↑x✝).toEquiv x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<GOAL>a ⊔ b ∈ s
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j ≤ i<GOAL>↑(i.cycleRange j) = if j = i then 0 else ↑j + 1
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j ≤ i<GOAL>↑(if j = i then 0 else j + 1) = if j = i then 0 else ↑j + 1
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j ≤ i<VAR>h' : ¬j = i<GOAL>↑(j + 1) = ↑j + 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x x₀ : M<VAR>y₀ : M'<GOAL>mfderiv I (I.prod I') (fun x => (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x x₀ : M<VAR>y₀ : M'<GOAL>(mfderiv I I id x₀).prod (mfderiv I I' (fun x => y₀) x₀) = ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
<VAR>a : Ordinal.{u}<GOAL>∀ (b : Ordinal.{u}), deriv (fun x => a + x) b = a * ω + b
<VAR>a : Ordinal.{u}<GOAL>deriv (fun x => a + x) 0 = a * ω + 0 ∧ ∀ (a_1 : Ordinal.{u}), deriv (fun x => a + x) a_1 = a * ω + a_1 → deriv (fun x => a + x) (succ a_1) = a * ω + succ a_1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>Valid' o₁ (l.balanceR x r) o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>hl : Valid' o₁ l ↑x<VAR>hr : Valid' (↑x) r o₂<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>Valid' o₂ (r.dual.balanceL x l.dual) o₁
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>X ⊆ M.closure X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hs : MeasurableSet s<VAR>hfi : Integrable f μ<GOAL>∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<GOAL>(trinomial k m n u v w).coeff k = u
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<GOAL>commProb (Product []) = 1
<VAR>α : Sort u_1<VAR>x y z : α<VAR>h : x = y<GOAL>z = x ↔ z = y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>s : Multiset { a // Irreducible a }<GOAL>p.count ↑s = Multiset.count ⟨p, hp⟩ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Ring T<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S T<VAR>inst✝⁵ : Algebra R T<VAR>inst✝⁴ : IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i j : m<VAR>k k' : n<VAR>h : k ≠ k'<GOAL>(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>x : E<GOAL>AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hs : IsOpen s<GOAL>ContDiffOn 𝕜 ⊤ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderiv 𝕜 f y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hs : IsOpen s<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderivWithin 𝕜 f s y) s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderiv 𝕜 f y) s
<VAR>m : ℤ<VAR>n k : ℕ<GOAL>↑m * 2 ^ n * powHalf (n + k) = ↑m * powHalf k
<VAR>m : ℤ<VAR>n k : ℕ<GOAL>↑m * (2 ^ n * powHalf (n + k)) = ↑m * powHalf k
<VAR>m : ℤ<VAR>n k : ℕ<GOAL>2 ^ n * powHalf (n + k) = powHalf k
<VAR>R : Type u<VAR>L : Type v<VAR>M : 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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<VAR>x : M<GOAL>x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
<VAR>R : Type u<VAR>L : Type v<VAR>M : 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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<VAR>x : M<GOAL>(∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝³ : AddMonoid α<VAR>inst✝² : Neg β<VAR>inst✝¹ : Group γ<VAR>inst✝ : DistribMulAction γ α<VAR>h : Antiperiodic f c<VAR>a : γ<VAR>x : α<GOAL>(fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : SMul 𝕜 α<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>g✝ : β → α<VAR>g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfg : EqOn f g s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>g (a • x + b • y) < a • g x + b • g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>⨆ n, (eapprox f n).lintegral (Measure.map g μ) = ⨆ n, (eapprox (f ∘ g) n).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>n : ℕ<GOAL>(eapprox f n).lintegral (Measure.map g μ) = (eapprox (f ∘ g) n).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>n : ℕ<GOAL>eapprox (f ∘ g) n = (eapprox f n).comp g hg
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>n : ℕ<VAR>x : α<GOAL>↑(eapprox (f ∘ g) n) x = ↑((eapprox f n).comp g hg) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>h : Continuous f<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>h : ContinuousOn f univ<GOAL>ContinuousOn f s
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ closure U<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ frontier U ∨ z ∈ U<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>hd : DiffContOnCl ℂ f U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hL : AntilipschitzWith (nndist z w)⁻¹ e<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hL : AntilipschitzWith (nndist z w)⁻¹ e<VAR>hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)<GOAL>‖f z‖ ≤ C
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hL : AntilipschitzWith (nndist z w)⁻¹ e<VAR>hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)<VAR>h₀ : 0 ∈ e ⁻¹' U<GOAL>‖f z‖ ≤ C