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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<GOAL>ContDiffAt 𝕜 n inverse ↑e
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<GOAL>ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<VAR>h₁ : ContDiff 𝕜 n O₁<GOAL>ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<VAR>h₁ : ContDiff 𝕜 n O₁<VAR>h₂ : ContDiff 𝕜 n O₂<GOAL>ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<VAR>h₁ : ContDiff 𝕜 n O₁<VAR>h₂ : ContDiff 𝕜 n O₂<GOAL>ContDiffAt 𝕜 n Ring.inverse (O₂ ↑e)
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>this : inverse = O₁ ∘ Ring.inverse ∘ O₂<VAR>h₁ : ContDiff 𝕜 n O₁<VAR>h₂ : ContDiff 𝕜 n O₂<GOAL>O₂ ↑e = ↑1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>r : ℝ<VAR>ha : 0 ≤ r<VAR>f : ι → ℝ<GOAL>(⨅ i, f i) * r = ⨅ i, f i * r
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝ : Epi q<VAR>comm : p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<GOAL>⟦Over.mk (a'' ≫ f)⟧ = ⟦Over.mk 0⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝ : Epi q<VAR>comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<VAR>Z : C<VAR>g : P ⟶ Z<VAR>hh : pseudoApply g ⟦a'⟧ = 0<GOAL>pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g ⟦a⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝¹ : Epi q<VAR>comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<VAR>Z : C<VAR>g : P ⟶ Z<VAR>hh : pseudoApply g ⟦a'⟧ = 0<VAR>X : C<VAR>p' : X ⟶ ((fun g_1 => app g g_1) a').left<VAR>q' : X ⟶ (Over.mk 0).left<VAR>ep' : Epi p'<VAR>w✝ : Epi q'<VAR>comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom<GOAL>pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g ⟦a⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝¹ : Epi q<VAR>comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<VAR>Z : C<VAR>g : P ⟶ Z<VAR>hh : pseudoApply g ⟦a'⟧ = 0<VAR>X : C<VAR>p' : X ⟶ ((fun g_1 => app g g_1) a').left<VAR>q' : X ⟶ (Over.mk 0).left<VAR>ep' : Epi p'<VAR>w✝ : Epi q'<VAR>comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom<VAR>this : a'.hom ≫ g = 0<GOAL>pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g ⟦a⟧
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝¹ : Epi q<VAR>comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<VAR>Z : C<VAR>g : P ⟶ Z<VAR>hh : pseudoApply g ⟦a'⟧ = 0<VAR>X : C<VAR>p' : X ⟶ ((fun g_1 => app g g_1) a').left<VAR>q' : X ⟶ (Over.mk 0).left<VAR>ep' : Epi p'<VAR>w✝ : Epi q'<VAR>comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom<VAR>this : a'.hom ≫ g = 0<GOAL>(fun g_1 => app g g_1) (Over.mk a'') ≈ (fun g_1 => app g g_1) a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : Pseudoelement P<VAR>a a' : Over P<VAR>h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>R : C<VAR>p : R ⟶ ((fun g => app f g) a).left<VAR>q : R ⟶ ((fun g => app f g) a').left<VAR>ep : Epi p<VAR>w✝¹ : Epi q<VAR>comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom<VAR>a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom<VAR>Z : C<VAR>g : P ⟶ Z<VAR>hh : pseudoApply g ⟦a'⟧ = 0<VAR>X : C<VAR>p' : X ⟶ ((fun g_1 => app g g_1) a').left<VAR>q' : X ⟶ (Over.mk 0).left<VAR>ep' : Epi p'<VAR>w✝ : Epi q'<VAR>comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom<VAR>this : a'.hom ≫ g = 0<GOAL>app g (Over.mk a'') ≈ app g a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s t : Finset α<VAR>hts : t ≤ s<GOAL>s ∈ ↑(Finset.memberSubfamily a 𝒜) → t ∈ ↑(Finset.memberSubfamily a 𝒜)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a : α<VAR>h : IsLowerSet ↑𝒜<VAR>s t : Finset α<VAR>hts : t ≤ s<GOAL>insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⋃ n, Ioc a ↑n = Ioi a \ {⊤}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Mono f<VAR>abar abar' : Pseudoelement P<GOAL>pseudoApply f abar = pseudoApply f abar' → abar = abar'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Mono f<VAR>abar abar' : Pseudoelement P<VAR>a a' : Over P<VAR>ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<GOAL>⟦a⟧ = ⟦a'⟧
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Mono f<VAR>abar abar' : Pseudoelement P<VAR>a a' : Over P<VAR>ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<GOAL>a ≈ a'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Mono f<VAR>abar abar' : Pseudoelement P<VAR>a a' : Over P<VAR>ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧<GOAL>a ≈ a'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Mono f<VAR>abar abar' : Pseudoelement P<VAR>a a' : Over P<VAR>ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧<VAR>this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧<VAR>R : C<VAR>p : R ⟶ (Over.mk (a.hom ≫ f)).left<VAR>q : R ⟶ (Over.mk (a'.hom ≫ f)).left<VAR>ep : Epi p<VAR>Eq : Epi q<VAR>comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom<GOAL>a ≈ a'
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsAlgClosed k<VAR>f : R →+* k<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<GOAL>(map f p).degree ≠ 0
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : IsAlgClosed k<VAR>f : R →+* k<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.degree ≠ 0<VAR>x : k<VAR>hx : (map f p).IsRoot x<GOAL>eval₂ f x p = 0
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>hx : x ∈ e.source<GOAL>LiftPropAt Q (↑e) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>hx : x ∈ e.source<GOAL>Q (↑(PartialHomeomorph.refl H) ∘ ↑e ∘ ↑e.symm) (↑e.symm ⁻¹' univ) (↑e x)
<VAR>q✝ q : ℚ<GOAL>-q = -q.num /. ↑q.den
<VAR>n : ℕ<GOAL>∑ m ∈ filter (fun x => x ∣ n) (range n.succ), φ m = n
<VAR>n : ℕ<GOAL>∑ m ∈ filter (fun x => x ∣ n) (range n.succ), φ m = n.divisors.sum φ
<VAR>n : ℕ<GOAL>(∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) = ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>x✝ a✝ : α<GOAL>a✝ ∈ (f x✝).bind ⇑f.symm ↔ a✝ ∈ (ofSet {a | (f a).isSome = true}) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<VAR>x✝ a✝ : α<GOAL>(∃ a, f x✝ = some a ∧ f a✝ = some a) ↔ a✝ = x✝ ∧ a✝ ∈ {a | ∃ a_1, f a = some a_1}
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>d : σ →₀ ℕ<GOAL>d.degree = 0 ↔ d = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X<VAR>S R : Sieve X<VAR>h : S.arrows (𝟙 X)<VAR>Y : C<VAR>f : Y ⟶ X<VAR>x✝ : ⊤.arrows f<GOAL>S.arrows f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>hf : ¬f = 0<GOAL>f.natDegree = f.reverse.natDegree + f.natTrailingDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>hf : ¬f = 0<GOAL>f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>hf : ¬f = 0<GOAL>f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>c : R<GOAL>derivative ((X - C c) ^ 2) = C 2 * (X - C c)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b a : k<VAR>hb : 0 < b<GOAL>a < b + ↑⌊a / b⌋ * b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>k : Type u_4<VAR>inst✝¹ : LinearOrderedField k<VAR>inst✝ : FloorRing k<VAR>b a : k<VAR>hb : 0 < b<GOAL>a / b < ↑⌊a / b⌋ + 1
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<GOAL>IntegrableOn (fun x => x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<VAR>hib : 0 < b ^ (-p⁻¹)<GOAL>IntegrableOn (fun x => x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<VAR>hib : 0 < b ^ (-p⁻¹)<GOAL>IntegrableOn (fun x => (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<VAR>hib : 0 < b ^ (-p⁻¹)<GOAL>Integrable (fun x => x ^ s * rexp (-x ^ p)) (volume.restrict (Ioi 0))
<VAR>p s b : ℝ<VAR>hs : -1 < s<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<VAR>hib : 0 < b ^ (-p⁻¹)<GOAL>IntegrableOn (fun x => x ^ s * rexp (-x ^ p)) (Ioi 0) volume
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>γ : Type u₁<VAR>inst✝ : AddCommMonoid γ<VAR>i : ι<VAR>f : γ →+ β i<GOAL>fromAddMonoid ((of (fun i => γ →+ β i) i) f) = (of β i).comp f
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>γ : Type u₁<VAR>inst✝ : AddCommMonoid γ<VAR>i : ι<VAR>f : γ →+ β i<GOAL>(AddMonoidHom.compHom (of β i)) f = (of β i).comp f
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n✝ n : ℕ<VAR>a✝ : Pair K<GOAL>a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ (of v).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n✝ n : ℕ<VAR>a✝ : Pair K<GOAL>a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ Option.map (Pair.map Rat.cast) ((of q).s.get? n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂dirac a = f a
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>s : Set A<GOAL>span R s ^ 0 = span R (s ^ 0)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>s : Set A<VAR>n : ℕ<GOAL>span R s ^ (n + 1) = span R (s ^ (n + 1))
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>coeff d ((homogeneousComponent n) φ) = if d.degree = n then coeff d φ else 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>coeff d ((homogeneousComponent n) φ) = if (weight 1) d = n then coeff d φ else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ↑↑↑((condexpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (a : α) in s, (↑↑↑((condexpL2 E' 𝕜 hm) f) - ↑↑f) a ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>Integrable (↑↑↑((condexpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∀ (c : E'), ∫ (x : α) in s, ⟪c, (↑↑↑((condexpL2 E' 𝕜 hm) f) - ↑↑f) x⟫_𝕜 ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E'<GOAL>∫ (x : α) in s, ⟪c, (↑↑↑((condexpL2 E' 𝕜 hm) f) - ↑↑f) x⟫_𝕜 ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E'<GOAL>∫ (x : α) in s, ⟪c, ↑↑↑((condexpL2 E' 𝕜 hm) f) x⟫_𝕜 - ⟪c, ↑↑f x⟫_𝕜 ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E'<GOAL>∫ (a : α) in s, ⟪c, ↑↑↑((condexpL2 E' 𝕜 hm) f) a⟫_𝕜 ∂μ - ∫ (a : α) in s, ⟪c, ↑↑f a⟫_𝕜 ∂μ = 0