ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu su xu‖ = ‖iteratedFDerivWithin 𝕜 i g s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu su xu‖ = ‖iteratedFDerivWithin 𝕜 i g s x‖<VAR>NBu : ‖iteratedFDerivWithin 𝕜 n (fun y => (Bu (fu y)) (gu y)) su xu‖ = ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu su xu‖ = ‖iteratedFDerivWithin 𝕜 i g s x‖<VAR>NBu : ‖iteratedFDerivWithin 𝕜 n (fun y => (Bu (fu y)) (gu y)) su xu‖ = ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖<VAR>this : ‖iteratedFDerivWithin 𝕜 n (fun y => (Bu (fu y)) (gu y)) su xu‖ ≤ ‖Bu‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i fu su xu‖ * ‖iteratedFDerivWithin 𝕜 (n - i) gu su xu‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<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>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu su xu‖ = ‖iteratedFDerivWithin 𝕜 i g s x‖<VAR>NBu : ‖iteratedFDerivWithin 𝕜 n (fun y => (Bu (fu y)) (gu y)) su xu‖ = ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖<VAR>this : ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖Bu‖ * ∑ x_1 ∈ Finset.range (n + 1), ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>μ : YoungDiagram<VAR>i : ℕ<GOAL>μ.rowLen i = (μ.row i).card
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>S : Set (Set X)<VAR>hS : S.Countable<GOAL>dimH (⋃₀ S) = ⨆ s ∈ S, dimH s
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : Ring K<VAR>inst✝⁴ : StrongRankCondition K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>W : Submodule K V<VAR>inst✝¹ : Module.Free K ↥W<VAR>inst✝ : Module.Finite K ↥W<GOAL>finrank K ↥W ≤ 1 ↔ W.IsPrincipal
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : LeftCancelMonoid G<VAR>x✝ y a : G<VAR>m n✝ : ℕ<VAR>x : G<VAR>hx : IsOfFinOrder x<VAR>n : ℕ<VAR>hn : ∃ m, x ^ m = x ^ n<GOAL>(finEquivPowers x hx).symm ⟨x ^ n, hn⟩ = ⟨n % orderOf x, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(B ^ m / B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>m n : ℕ<GOAL>↑(B⁻¹ ^ m / B⁻¹ ^ n).card ≤ (↑(A * B⁻¹).card / ↑A.card) ^ (m + n) * ↑A.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : α ≃ β<VAR>e' : β ≃ γ<GOAL>(e.trans e').toPartialEquiv.source = (e.toPartialEquiv.trans e'.toPartialEquiv).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>n : ℕ<VAR>hns : n ≤ s.ncard<GOAL>∃ t ⊆ s, t.ncard = n
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>this : univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>((κ.singularPart η) a) univ = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J × K ⥤ C<VAR>inst✝² : HasLimitsOfShape J C<VAR>inst✝¹ : HasColimitsOfShape K C<VAR>G : J ⥤ K ⥤ C<VAR>inst✝ : HasLimit G<VAR>j : J<VAR>k : K<GOAL>colimit.ι (limit G) k ≫ (colimMap (limitIsoSwapCompLim G).hom ≫ colimitLimitToLimitColimit (uncurry.obj G) ≫ limMap (whiskerRight (currying.unitIso.inv.app G) colim)) ≫ limit.π (G ⋙ colim) j = colimit.ι (limit G) k ≫ colimMap (limit.π G j)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₁, u₁} J<VAR>inst✝⁴ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J × K ⥤ C<VAR>inst✝² : HasLimitsOfShape J C<VAR>inst✝¹ : HasColimitsOfShape K C<VAR>G : J ⥤ K ⥤ C<VAR>inst✝ : HasLimit G<VAR>j : J<VAR>k : K<GOAL>(limitObjIsoLimitCompEvaluation G k).hom ≫ limit.π (G.flip.obj k) j ≫ colimit.ι (G.obj j) k = (limit.π G j).app k ≫ colimit.ι (G.obj j) k
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : FinitaryPreExtensive C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>inhabited_h : Inhabited ι<VAR>inst✝ : ⊥.IsCountablyGenerated<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) ⊥ (𝓝 l)<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) ⊥ (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<VAR>hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<VAR>hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x<VAR>h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<VAR>hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x<VAR>h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x<VAR>f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some<VAR>hf_lim : ∀ (x : α), Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x))<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<VAR>hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x<VAR>h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x<VAR>f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some<VAR>hf_lim : ∀ (x : α), Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x))<VAR>h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>ι : Type u_3<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Nonempty ι<VAR>μ : Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)<VAR>inhabited_h : Inhabited ι<VAR>hL : L.NeBot<VAR>p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)<VAR>hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x<VAR>h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x<VAR>f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some<VAR>hf_lim : ∀ (x : α), Tendsto (fun n => aeSeq hf p n x) L (𝓝 (f_lim x))<VAR>h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))<VAR>h_f_lim_meas : Measurable f_lim<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>a o : Ordinal.{u}<VAR>ha : a.IsLimit<VAR>g : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hg : a.IsFundamentalSequence o g<GOAL>(f a).IsFundamentalSequence o fun b hb => f (g b hb)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>a o : Ordinal.{u}<VAR>ha : a.IsLimit<VAR>g : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hg : a.IsFundamentalSequence o g<GOAL>o ≤ (f a).cof.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<VAR>a o : Ordinal.{u}<VAR>ha : a.IsLimit<VAR>g : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hg : a.IsFundamentalSequence o g<GOAL>(o.blsub fun b hb => f (g b hb)) = f a
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc' : c ≠ ⊤<GOAL>a * c / (b * c) = a / b
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<GOAL>IsPrimePow n ↔ n.primeFactors.card = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : R[X][Y]<VAR>q : R[X]<VAR>r : R<GOAL>eval (f r) (eval (map f q) (map (mapRingHom f) p)) = f (eval r (eval q p))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a + b - (a + c) = b - c
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>x ∈ ball y ε ↔ y ∈ ball x ε
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>P : Type u_2<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R P<VAR>M : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<GOAL>Projective R P ↔ ∃ s, Finsupp.total P P R id ∘ₗ s = LinearMap.id