ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>u : V<VAR>v : V'<GOAL>G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<GOAL>IsGLB S (sInf S)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<VAR>h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'<GOAL>IsGLB S (sInf S)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<VAR>h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'<GOAL>IsGLB (SetLike.coe '' S) ↑(sInf S)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>S : Set (LieSubalgebra R L)<VAR>h : ∀ (K K' : LieSubalgebra R L), ↑K ≤ ↑K' ↔ K ≤ K'<GOAL>IsGLB (SetLike.coe '' S) (⋂ s ∈ S, ↑s)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>z w : N<GOAL>∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>z w : N<VAR>a : M × ↥S<VAR>ha : z * f.toMap ↑a.2 = f.toMap a.1<GOAL>∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>z w : N<VAR>a : M × ↥S<VAR>ha : z * f.toMap ↑a.2 = f.toMap a.1<VAR>b : M × ↥S<VAR>hb : w * f.toMap ↑b.2 = f.toMap b.1<GOAL>∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<GOAL>Q.diagonal f ↔ P.diagonal f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>Q.diagonal f ↔ P.diagonal f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>hf : Q.diagonal f<GOAL>P.diagonal f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this : Q.IsLocal := isLocal_affineProperty P<VAR>hf : Q.diagonal (pullback.snd f (𝟙 Y))<GOAL>P.diagonal f
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsAffine Y<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>hf : Q.diagonal (pullback.snd f (𝟙 Y))<VAR>𝒰 : (pullback f (𝟙 Y)).OpenCover := X.affineCover.pushforwardIso (inv (pullback.fst f (𝟙 Y)))<VAR>this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)<GOAL>P.diagonal f
<VAR>R : Type u<VAR>a b : R<VAR>m n✝¹ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n n✝ : ℕ<GOAL>(p.update n 0).coeff n✝ = (erase n p).coeff n✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t✝ : Set X<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>t : Set Y<VAR>hg : HolderOnWith Cg rg g t<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderOnWith Cf rf f s<VAR>hst : MapsTo f s t<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<GOAL>edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑(Cg * Cf ^ ↑rg) * edist x y ^ ↑(rg * rf)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f✝ : X → Y<VAR>s t✝ : Set X<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>t : Set Y<VAR>hg : HolderOnWith Cg rg g t<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderOnWith Cf rf f s<VAR>hst : MapsTo f s t<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<GOAL>edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * (↑Cf * edist x y ^ ↑rf) ^ ↑rg
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : Subobject Z<GOAL>(pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>t : MonoOver Z<GOAL>(pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>ha : 0 < a<GOAL>a < a * b ↔ 1 < b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.725197) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>this : 0 ≤ cfc id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x<GOAL>0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ 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>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>hf : AEStronglyMeasurable f (κ a)<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
<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>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>hf : AEStronglyMeasurable f ((κ.fst ⊗ₖ κ.condKernel) a)<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂κ.condKernel (a, x)) (κ.fst a)
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<GOAL>x ∈ I ∨ xᶜ ∈ I
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<GOAL>x ⊓ xᶜ ∈ I
<VAR>P : Type u_1<VAR>inst✝ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>hI : I.IsPrime<GOAL>⊥ ∈ I
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s t : Set X<VAR>hu : t ⊆ insert y s<GOAL>insert x s ∈ 𝓝[t] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>s t : Set X<VAR>hu : t ⊆ insert x s<GOAL>insert x s ∈ 𝓝[t] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s t : Set X<VAR>hu : t ⊆ insert y s<VAR>h : x ≠ y<GOAL>insert x s ∈ 𝓝[t] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s t : Set X<VAR>hu : t ⊆ insert y s<VAR>h : x ≠ y<GOAL>insert x s ∈ 𝓝[insert y s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>s t : Set X<VAR>hu : t ⊆ insert y s<VAR>h : x ≠ y<GOAL>insert x s ∈ 𝓝[s] x
<VAR>p : Prop<VAR>α : Sort u_1<VAR>inst✝ : Nonempty α<VAR>P : α → Prop<VAR>f : p → α<VAR>a : p<VAR>h : P (f a)<GOAL>P (sometimes f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LindelofSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsLindelof (range f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : LindelofSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsLindelof (f '' univ)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>All P (if l.size + r.size ≤ 1 then l.node' x r else if r.size > delta * l.size then l.rotateL x r else if l.size > delta * r.size then l.rotateR x r else l.node' x r) ↔ All P l ∧ P x ∧ All P r
<VAR>S : Type u'<VAR>T : Type u''<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>p : SubMulAction R M<VAR>m : ↥p<VAR>x✝ : R<GOAL>x✝ ∈ MulAction.stabilizerSubmonoid R m ↔ x✝ ∈ MulAction.stabilizerSubmonoid R ↑m
<VAR>n m : ℕ<GOAL>n.dist m = m.dist n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ = √(re ⟪((adjoint A).comp A) x, x⟫_𝕜)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f✝ g : α → M<VAR>a : α<VAR>r : M<VAR>s : Set α<VAR>f : α → M<GOAL>r ∈ range (s.mulIndicator f) ↔ r = 1 ∧ s ≠ univ ∨ r ∈ f '' s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x 0 = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.neg (u • P) = u • W'.neg P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>![(u • P) x, u ^ 3 * W'.negY P, (u • P) z] = u • W'.neg P
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.87350, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>hg : S.g = 0<GOAL>S.opcycles ≅ S.rightHomology
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.87350, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>hg : S.g = 0<VAR>this : IsIso S.rightHomologyι<GOAL>S.opcycles ≅ S.rightHomology
<VAR>z : ℂ<GOAL>z⁻¹.re = z.re / normSq z
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l l' : Filter α<GOAL>l' ∈ closure {l} ↔ l' ∈ Ici l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α ≃o β<VAR>s t : UpperSet α<VAR>a : α<VAR>b : β<GOAL>b ∈ (map f) s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α ≃o β<VAR>s t : UpperSet α<VAR>a : α<VAR>b : β<GOAL>b ∈ (map f.symm).symm s ↔ f.symm b ∈ s
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<GOAL>{K | |discr ↥↑K| ≤ ↑N}.Finite
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>N : ℕ<VAR>hK : |discr K| ≤ ↑N<GOAL>{K | |discr ↥↑K| ≤ ↑N} ⊆ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N} ∪ {K | {w | w.IsComplex}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cocone F.unop<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeUnop c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j<GOAL>m = (fun s => (hc.desc (coconeUnopOfCone s)).op) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>F : Jᵒᵖ ⥤ Cᵒᵖ<VAR>c : Cocone F.unop<VAR>hc : IsColimit c<VAR>s : Cone F<VAR>m : s.pt ⟶ (coneOfCoconeUnop c).pt<VAR>w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j<VAR>j : J<GOAL>(c.ι.app j ≫ m.unop).op = (c.ι.app j ≫ ((fun s => (hc.desc (coconeUnopOfCone s)).op) s).unop).op
<VAR>P : Type u_1<VAR>inst✝¹ : Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>inst✝ : Encodable ι<VAR>𝒟 : ι → Cofinal P<GOAL>Monotone (sequenceOfCofinals p 𝒟)
<VAR>P : Type u_1<VAR>inst✝¹ : Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>inst✝ : Encodable ι<VAR>𝒟 : ι → Cofinal P<GOAL>∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
<VAR>x n m : ℕ<GOAL>x ∣ x.gcd n * x.gcd m ↔ x ∣ n * m
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>j : F<VAR>inst✝ : DecidableEq F<VAR>h3 : NeZero 3<GOAL>ofJ 0 = ofJ0 F
<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>a✝ a'✝ : α<VAR>b✝ : M<VAR>a a' : α<VAR>b : M<GOAL>a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa✝ : Measure α<VAR>μb✝ : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>e : α ≃ᵐ β<VAR>μa : Measure α<VAR>μb : Measure β<VAR>h : MeasurePreserving (⇑e) μa μb<GOAL>map (⇑e.symm) μb = μa
<VAR>n : ℕ+<VAR>hn : n ≠ 1<GOAL>∃ p, p.Prime ∧ p ∣ n
<VAR>n : ℕ+<VAR>hn : n ≠ 1<VAR>p : ℕ<VAR>hp : Nat.Prime p ∧ p ∣ ↑n<GOAL>∃ p, p.Prime ∧ p ∣ n
<VAR>n : ℕ+<VAR>hn : n ≠ 1<VAR>p : ℕ<VAR>hp : Nat.Prime p ∧ p ∣ ↑n<GOAL>Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n
<VAR>n : ℕ+<VAR>hn : n ≠ 1<VAR>p : ℕ<VAR>hp : Nat.Prime p ∧ p ∣ ↑n<GOAL>Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑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 η<GOAL>((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η
<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>h_le : κ ≤ κ + η<GOAL>((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η
<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>h_le : κ ≤ κ + η<GOAL>(((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) + (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ + η
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>(((κ + η).withDensity fun a x => ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) + (κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) = κ + η
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>(((κ + η).withDensity fun a x => 1 - ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) + (κ + η).withDensity fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) = κ + η
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>((κ + η).withDensity fun a x => 1) = κ + η
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>Measurable (Function.uncurry fun a x => 1)
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>Measurable (Function.uncurry fun a x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))
<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>h_le : κ ≤ κ + η<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>∀ (a : α), (fun x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᶠ[ae ((κ + η) a)] fun x => 1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>G : C<VAR>inst✝ : ∀ (A : C), HasProduct fun x => G<GOAL>IsCoseparator G ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>G : C<VAR>inst✝ : ∀ (A : C), HasProduct fun x => G<GOAL>(∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M₁<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid N₁<VAR>inst✝⁶ : AddCommMonoid N₂<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R N₁<VAR>inst✝¹ : Module R N₂<VAR>inst✝ : Module R P<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<VAR>m₂ m₂' : M₂<GOAL>(Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f g : CauchyFilter α<VAR>a b : α<VAR>ha : ↑f ≤ 𝓝 a<VAR>hb : ↑g ≤ 𝓝 b<GOAL>Inseparable a b ↔ Inseparable f g
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f g : CauchyFilter α<VAR>a b : α<VAR>ha : Tendsto id (↑f) (𝓝 a)<VAR>hb : Tendsto id (↑g) (𝓝 b)<GOAL>Inseparable a b ↔ Inseparable f g
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f g : CauchyFilter α<VAR>a b : α<VAR>ha : Tendsto id (↑f) (𝓝 a)<VAR>hb : Tendsto id (↑g) (𝓝 b)<GOAL>Tendsto (fun x => ((id ∘ Prod.fst) x, (id ∘ Prod.snd) x)) (↑f ×ˢ ↑g) (𝓤 α) ↔ ↑f ×ˢ ↑g ≤ 𝓤 α
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>a : α<VAR>s : Set α<VAR>inst✝ : Decidable (a ∈ s)<GOAL>∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>f : α → E<VAR>a : α<VAR>s : Set α<VAR>inst✝ : Decidable (a ∈ s)<GOAL>(∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0
<VAR>C : Type u_2<VAR>inst✝⁶ : Category.{u_1, u_2} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝⁴ : S₁.HasHomology<VAR>inst✝³ : S₂.HasHomology<VAR>inst✝² : S₃.HasHomology<VAR>inst✝¹ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝ : QuasiIso φ<GOAL>QuasiIso (opMap φ)
<VAR>C : Type u_2<VAR>inst✝⁶ : Category.{u_1, u_2} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝⁴ : S₁.HasHomology<VAR>inst✝³ : S₂.HasHomology<VAR>inst✝² : S₃.HasHomology<VAR>inst✝¹ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝ : QuasiIso φ<GOAL>QuasiIso φ
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<VAR>h : i ≠ j<GOAL>𝟙 M i j = 0