ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<VAR>g' : α → β := invFun g<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<VAR>g' : α → β := invFun g<VAR>g'g : LeftInverse g' g<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<VAR>g' : α → β := invFun g<VAR>g'g : LeftInverse g' g<VAR>hg'ns : g' '' sᶜ = (f '' s)ᶜ<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<VAR>g' : α → β := invFun g<VAR>g'g : LeftInverse g' g<VAR>hg'ns : g' '' sᶜ = (f '' s)ᶜ<VAR>h : α → β := s.piecewise f g'<GOAL>∃ h, Bijective h
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : Injective g<VAR>hβ : Nonempty β<VAR>F : Set α →o Set α := { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }<VAR>s : Set α := OrderHom.lfp F<VAR>hs : (g '' (f '' s)ᶜ)ᶜ = s<VAR>hns : g '' (f '' s)ᶜ = sᶜ<VAR>g' : α → β := invFun g<VAR>g'g : LeftInverse g' g<VAR>hg'ns : g' '' sᶜ = (f '' s)ᶜ<VAR>h : α → β := s.piecewise f g'<VAR>this : Surjective h<GOAL>∃ h, Bijective h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α ≃ β<VAR>a✝ : β<GOAL>(equivMapDomain f 0) a✝ = 0 a✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup G<VAR>n : ℕ<VAR>f : ℕ → G<VAR>h : ((fun x => x⁻¹) ∘ fun k => f (k + 1) / f k) = fun k => f k / f (k + 1)<GOAL>(map (fun k => f (k + 1) / f k) (range n)).prod = f n / f 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>u v : E<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>li : E →ₗᵢ[ℝ] F<GOAL>angle ((c • li.toContinuousLinearMap) u) ((c • li.toContinuousLinearMap) v) = angle u v
<VAR>a b c d m n : ℤ<VAR>n✝ : ℕ<VAR>h : 0 < n✝ + 1<GOAL>↑(n✝ + 1 - 1) = ↑(n✝ + 1) - 1
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<GOAL>Function.Injective ⇑(galActionHom p E)
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<GOAL>∀ (a : p.Gal), (galActionHom p E) a = 1 → a = 1
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : p.Gal<VAR>hϕ : (galActionHom p E) ϕ = 1<VAR>x : p.SplittingField<VAR>hx : x ∈ p.rootSet p.SplittingField<GOAL>ϕ x = 1 x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : p.Gal<VAR>hϕ : (galActionHom p E) ϕ = 1<VAR>x : p.SplittingField<VAR>hx : x ∈ p.rootSet p.SplittingField<VAR>key : ((galActionHom p E) ϕ) ((rootsEquivRoots p E) ⟨x, hx⟩) = 1 ((rootsEquivRoots p E) ⟨x, hx⟩)<GOAL>ϕ x = 1 x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : p.Gal<VAR>hϕ : (galActionHom p E) ϕ = 1<VAR>x : p.SplittingField<VAR>hx : x ∈ p.rootSet p.SplittingField<VAR>key : (rootsEquivRoots p E) (ϕ • (rootsEquivRoots p E).symm ((rootsEquivRoots p E) ⟨x, hx⟩)) = (rootsEquivRoots p E) ⟨x, hx⟩<GOAL>ϕ x = 1 x
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>ϕ : p.Gal<VAR>hϕ : (galActionHom p E) ϕ = 1<VAR>x : p.SplittingField<VAR>hx : x ∈ p.rootSet p.SplittingField<VAR>key : (rootsEquivRoots p E) (ϕ • ⟨x, hx⟩) = (rootsEquivRoots p E) ⟨x, hx⟩<GOAL>ϕ x = 1 x
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>γ : Type u_3<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>f : α → γ<VAR>cont_f : Continuous f<VAR>x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct<VAR>x✝ : UniformSpace pkg.space := pkg.uniformStruct<VAR>h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))<GOAL>⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>γ : Type u_3<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>f : α → γ<VAR>cont_f : Continuous f<VAR>x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct<VAR>x✝ : UniformSpace pkg.space := pkg.uniformStruct<VAR>h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))<VAR>this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x<GOAL>⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>γ : Type u_3<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>f : α → γ<VAR>cont_f : Continuous f<VAR>x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct<VAR>x✝ : UniformSpace pkg.space := pkg.uniformStruct<VAR>h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))<VAR>this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x<GOAL>Continuous (⋯.extend f)
<VAR>α : Type u_1<VAR>inst✝³ : UniformSpace α<VAR>pkg : AbstractCompletion α<VAR>β : Type u_2<VAR>inst✝² : UniformSpace β<VAR>pkg' : AbstractCompletion α<VAR>γ : Type u_3<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T3Space γ<VAR>f : α → γ<VAR>cont_f : Continuous f<VAR>x✝¹ : UniformSpace pkg'.space := pkg'.uniformStruct<VAR>x✝ : UniformSpace pkg.space := pkg.uniformStruct<VAR>h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))<VAR>this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x<GOAL>∀ (b : pkg.space), ∃ c, Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>𝕜 : Type u_4<VAR>B : I → Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : (i : I) → NormedRing (B i)<VAR>inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)<VAR>inst✝ : ∀ (i : I), NormOneClass (B i)<VAR>k : 𝕜<GOAL>Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>𝕜 : Type u_4<VAR>B : I → Type u_5<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : (i : I) → NormedRing (B i)<VAR>inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)<VAR>inst✝ : ∀ (i : I), NormOneClass (B i)<VAR>k : 𝕜<GOAL>Memℓp (k • 1) ⊤
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝⁴ : SmallCategory J<VAR>inst✝³ : FinCategory J<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → α<GOAL>Finset.univ.sup (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.sup f
<VAR>α : Type u<VAR>J : Type w<VAR>inst✝⁴ : SmallCategory J<VAR>inst✝³ : FinCategory J<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>f : ι → α<GOAL>Finset.univ.sup f = Fintype.elems.sup f
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α (last n)<VAR>q✝ : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.castSucc<VAR>i✝ : Fin n<VAR>y : α i✝.castSucc<VAR>z : α (last n)<VAR>β : Type u_1<VAR>q : Fin (n + 2) → β<VAR>i : Fin n<GOAL>tail (init q) i = init (tail q) i
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>g : ?m.758269<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(baseChange W B).toAffine.Equation (f x) (f y) ↔ (baseChange W A).toAffine.Equation x y
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>g : ?m.758269<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(baseChange W B).toAffine.Equation (f x) (f y) ↔ (baseChange W B).toAffine.Equation (f.toRingHom x) (f.toRingHom y)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>ℳ : ι → Submodule R M<VAR>inst✝² : Decomposition ℳ<VAR>N : Type u_5<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>f g : M →ₗ[R] N<VAR>h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype<VAR>i : ι<GOAL>(f ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i => ↥(ℳ i)) i = (g ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i => ↥(ℳ i)) i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q : ℚ<GOAL>∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q : ℚ<VAR>x : α<VAR>hx : 0 < x<GOAL>∀ a ∈ cutMap β (x * x), a ≤ (inducedAddHom α β) x * (inducedAddHom α β) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q : ℚ<VAR>x : α<VAR>hx : 0 < x<GOAL>∀ w < (inducedAddHom α β) x * (inducedAddHom α β) x, ∃ a ∈ cutMap β (x * x), w < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsProbabilityMeasure μ<VAR>p : α → Prop<VAR>f : β → α<VAR>hs : NullMeasurableSet s μ<GOAL>μ sᶜ = 0 ↔ μ s = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>ι : Sort u_4<VAR>U : Submodule 𝕜 E<VAR>V : ι → Submodule 𝕜 E<GOAL>(∀ (i : ι), V i ⟂ U) ↔ ∀ (i : ι), U ⟂ V i
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] =ᶠ[ae (μ.restrict s)] 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<GOAL>μ[f|m] =ᶠ[ae (μ.restrict s)] 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>μ[f|m] =ᶠ[ae (μ.restrict s)] 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → (μ.restrict s) s_1 < ⊤ → IntegrableOn (μ[f|m]) s_1 (μ.restrict s)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → (μ.restrict s) s_1 < ⊤ → IntegrableOn 0 s_1 (μ.restrict s)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → (μ.restrict s) s_1 < ⊤ → ∫ (x : α) in s_1, (μ[f|m]) x ∂μ.restrict s = ∫ (x : α) in s_1, 0 x ∂μ.restrict s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>AEStronglyMeasurable' m (μ[f|m]) (μ.restrict s)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>μ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : f =ᶠ[ae (μ.restrict s)] 0<VAR>hm : m ≤ m0<VAR>hμm this✝ : SigmaFinite (μ.trim hm)<VAR>this : SigmaFinite ((μ.restrict s).trim hm)<VAR>hf_int : Integrable f μ<GOAL>AEStronglyMeasurable' m 0 (μ.restrict s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a⌋₊ = 0 ↔ a < 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a⌋₊ < 1 ↔ a < ↑1
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : CharP R n<VAR>inst✝ : Fintype R<VAR>h : Fintype.card R = n<GOAL>Bijective ⇑(castHom ⋯ R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : CharP R n<VAR>inst✝ : Fintype R<VAR>h : Fintype.card R = n<VAR>this : NeZero n<GOAL>Bijective ⇑(castHom ⋯ R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : CharP R n<VAR>inst✝ : Fintype R<VAR>h : Fintype.card R = n<VAR>this : NeZero n<GOAL>Injective ⇑(castHom ⋯ R)
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<VAR>hz : z < 0<GOAL>1 ≤ x ^ z
<VAR>z : ℝ<VAR>hz : z < 0<VAR>x : ℝ≥0<VAR>hx1 : 0 < ↑x<VAR>hx2 : ↑x ≤ 1<GOAL>1 ≤ ↑x ^ z
<VAR>z : ℝ<VAR>hz : z < 0<VAR>x : ℝ≥0<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<GOAL>1 ≤ ↑x ^ z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 ≤ a<VAR>hc : 0 < c<VAR>h : c ≤ b<GOAL>a / b ≤ a / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 ≤ a<VAR>hc : 0 < c<VAR>h : c ≤ b<GOAL>a * b⁻¹ ≤ a * c⁻¹
<VAR>n : ℕ<GOAL>↑n = ↑n /. 1
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>P' : C<VAR>inl' : X ⟶ P'<VAR>inr' : Y ⟶ P'<VAR>h : IsPushout f g inl inr<VAR>h' : IsPushout f g inl' inr'<GOAL>inl' ≫ (isoIsPushout X Y h h').inv = inl
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₁ ⟶ X₀<VAR>d₁ : X₂ ⟶ X₁<VAR>s : d₁ ≫ d₀ = 0<VAR>succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0<GOAL>(if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C✝ C' C'' C : VariableChange R<GOAL>C.comp id = C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>interior (f.extend I).target ⊆ interior (range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>↑I.symm ⁻¹' f.target ∩ interior (range ↑I) ⊆ interior (range ↑I)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<GOAL>∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<VAR>a b : ZMod p<VAR>hx : a ^ 2 + b ^ 2 = ↑x<GOAL>∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<VAR>a b : ZMod p<VAR>hx : a ^ 2 + b ^ 2 = ↑x<GOAL>↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<VAR>a b : ZMod p<VAR>hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x<GOAL>↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<VAR>a b : ZMod p<VAR>hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x<GOAL>|a.valMinAbs| ^ 2 + |b.valMinAbs| ^ 2 ≡ x [ZMOD ↑p]
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝ : Fact (Prime p)<VAR>x : ℤ<VAR>a b : ZMod p<VAR>hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x<GOAL>↑(a.valMinAbs ^ 2 + b.valMinAbs ^ 2) = ↑x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>g : G<VAR>h : g ∈ H.normalizer<VAR>n : G<GOAL>n * g ∈ H ↔ g * n ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>g : G<VAR>h : ∀ (n : G), n * g ∈ H ↔ g * n ∈ H<VAR>n : G<GOAL>n ∈ H ↔ g * n * g⁻¹ ∈ H
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>S.Exact ↔ imageSubobject S.f = kernelSubobject S.g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>IsIso (imageToKernel S.f S.g ⋯) ↔ imageSubobject S.f = kernelSubobject S.g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>hdeg : 1 < f.natDegree<GOAL>h.basis ⟨1, hdeg⟩ = h.root
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hy : 0 < y<GOAL>x < logb b y ↔ y < b ^ x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<VAR>c : ℕ := f.support.card<VAR>hc : c = f.support.card<VAR>h₁ : c = 0<GOAL>f.eraseLead.support.card + 1 = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f ≠ 0<VAR>c : ℕ := f.support.card<VAR>hc : c = f.support.card<VAR>n✝ : ℕ<VAR>h₁ : c = n✝ + 1<GOAL>f.eraseLead.support.card + 1 = n✝ + 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>p₁ p₂ x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>SameRay R (t • (x -ᵥ p₁) +ᵥ p₂ -ᵥ p₂) (x -ᵥ p₁)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>p₁ p₂ x : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : 0 ≤ t<GOAL>SameRay R (t • (x -ᵥ p₁)) (x -ᵥ p₁)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>p✝ : ?m.46544<VAR>u v : V<VAR>H : SimpleGraph V<VAR>p : G.Walk u v<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<VAR>pp : p.IsPath<GOAL>(p.transfer H hp).IsPath
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.reverse.prev x ⋯ = l.next x hx
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<GOAL>l.reverse.prev (l.nthLe k hk) ⋯ = l.next (l.nthLe k hk) hx