ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>{ f := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.g, g := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.f, k := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.k, ε := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.ε⁻¹, f₀ := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.g₀, g₀ := { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.f₀, hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ } = { f := ofReal' ∘ evenKernel 0, g := ofReal' ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair.proof_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<GOAL>↑(⨅ i, f i) = a ⊓ ⨅ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>s : Set α<VAR>inst✝ : CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Iic a)<VAR>f : ι → ↑(Iic a)<VAR>p : ι → Prop<GOAL>a ⊓ sInf (Subtype.val '' range fun i => f i) = a ⊓ ⨅ i, ↑(f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : CommSemiring P<VAR>inst✝⁴ : CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<VAR>x : S<GOAL>x ∈ RingHom.ker (map Q g ⋯) ↔ x ∈ Ideal.map (algebraMap R S) (RingHom.ker g)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : CommSemiring P<VAR>inst✝⁴ : CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<VAR>x : R<VAR>s : ↥M<GOAL>mk' S x s ∈ RingHom.ker (map Q g ⋯) ↔ mk' S x s ∈ Ideal.map (algebraMap R S) (RingHom.ker g)
<VAR>l : List ℕ<VAR>a m n : ℕ<GOAL>0 < n.greatestFib ↔ 0 < n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h : IntegrableOn f s μ<VAR>hs : MeasurableSet s<GOAL>IntegrableOn f s (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h : IntegrableOn f s μ<VAR>hs : MeasurableSet s<GOAL>Integrable f (μ.restrict (s ∩ t))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>IsAffineOpen (X.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>IsAffineOpen (PrimeSpectrum.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : Spec Γ(X, U) = Spec (CommRingCat.of ↑Γ(X, U))<GOAL>PrimeSpectrum.basicOpen f = Scheme.Hom.opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U)) (Localization.Away f))))
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<GOAL>n.factorization p = (Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n)).card
<VAR>α✝ : Type u₁<VAR>C : Type u₂<VAR>inst✝ : Category.{v₂, u₂} C<VAR>α : Type u₁<VAR>β : Type u₂<VAR>h : Discrete α ≌ Discrete β<VAR>a : α<GOAL>(as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a
<VAR>α✝ : Type u₁<VAR>C : Type u₂<VAR>inst✝ : Category.{v₂, u₂} C<VAR>α : Type u₁<VAR>β : Type u₂<VAR>h : Discrete α ≌ Discrete β<VAR>a : β<GOAL>(as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<VAR>h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)<GOAL>↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = ↑(index (↑K₁) U) / ↑(index (↑K₀) U) + ↑(index (↑K₂) U) / ↑(index (↑K₀) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<VAR>h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)<GOAL>↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>K₁ K₂ : Compacts G<VAR>hU : (interior U).Nonempty<VAR>h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)<GOAL>↑(index (↑(K₁ ⊔ K₂)) U) = ↑(index (↑K₁) U) + ↑(index (↑K₂) U)
<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✝⁷ : OrderedRing 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>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<GOAL>Wbtw R x y z ∧ Wbtw R x z y ↔ y = z
<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✝⁷ : OrderedRing 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>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<GOAL>Wbtw R z y x ∧ Wbtw R y z x ↔ z = y
<VAR>p q✝ q : ℚ≥0<GOAL>↑(↑q.num / ↑q.den) = ↑q
<VAR>p q✝ q : ℚ≥0<GOAL>↑(↑q).num / ↑q.den = ↑q
<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>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>e : M → N<VAR>he0 : e 0 = 0<VAR>f : ι →₀ M<VAR>he : Injective e<VAR>a✝ : ι<GOAL>a✝ ∈ (mapRange e he0 f).support ↔ a✝ ∈ f.support
<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>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>e : M → N<VAR>he0 : e 0 = 0<VAR>f : ι →₀ M<VAR>he : Injective e<VAR>a✝ : ι<GOAL>¬e (f a✝) = 0 ↔ ¬f a✝ = 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<VAR>this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖<GOAL>Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<VAR>this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖<VAR>n : ℕ<GOAL>‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Subring S<VAR>x : R × S<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>g : β → γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : LeftOrdContinuous f<VAR>n : ℕ<GOAL>LeftOrdContinuous f^[n]
<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>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x✝ : M<GOAL>((f.lift hg).comp f.toMap) x✝ = g x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>h : μ ≪ ν<GOAL>μ.singularPart ν = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>h : μ ≪ ν<GOAL>μ.singularPart ν ⟂ₘ μ.singularPart ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>i j : Fin s.card<GOAL>(s.orderEmbOfFin ⋯) i = (s.orderEmbOfFin ⋯) j ↔ ↑i = ↑j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>od : Prop<VAR>o p : od → α<VAR>H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom<VAR>H2 : ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom), { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂<GOAL>{ Dom := od, get := o } = { Dom := od, get := p }
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule<VAR>x : L<GOAL>(ad R L) (D x) ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule<VAR>x : L<GOAL>⁅x, D⁆ ∈ (killingForm R (LieDerivation R L L)).orthogonal (LinearMap.range ↑(ad R L))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<GOAL>HasProd (fun x => 1) 1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y<VAR>y : α<GOAL>p y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y✝ z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y<VAR>y : α<VAR>R : ℝ<VAR>hR : R > dist y x<VAR>h : ∀ z ∈ ball x R, p z<GOAL>p y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>m : Sym2 α<GOAL>(∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>m : Sym2 α<GOAL>Sym2.diag a ∈ s.sym2 ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>hκ : IsSFiniteKernel κ<GOAL>((κ ⊗ₖ η) a) Set.univ ≤ (κ a) Set.univ * IsFiniteKernel.bound η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>hκ : IsSFiniteKernel κ<GOAL>∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ Set.univ} ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>hκ : IsSFiniteKernel κ<GOAL>∫⁻ (b : β), (η (a, b)) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>hκ : IsSFiniteKernel κ<VAR>Cη : ℝ≥0∞ := IsFiniteKernel.bound η<GOAL>∫⁻ (b : β), (η (a, b)) Set.univ ∂κ a ≤ (κ a) Set.univ * IsFiniteKernel.bound η
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>h : ∞ ∉ s<GOAL>IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.84561, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>hf : S.f = 0<GOAL>S.opcycles ≅ S.X₂
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.84561, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>hf : S.f = 0<VAR>this : IsIso S.pOpcycles<GOAL>S.opcycles ≅ S.X₂
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsFilteredOrEmpty J<GOAL>FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsFilteredOrEmpty J<VAR>h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)<GOAL>FinallySmall J
<VAR>J : Type u<VAR>inst✝¹ : Category.{v, u} J<VAR>inst✝ : IsFilteredOrEmpty J<VAR>s : Set J<VAR>hs : Small.{v, u} ↑s<VAR>hs' : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)<GOAL>FinallySmall J
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback (G.map f) (G.map g)<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>G.map h ≫ G.map f = G.map k ≫ G.map g
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback (G.map f) (G.map g)<VAR>W : C<VAR>h : W ⟶ X<VAR>k : W ⟶ Y<VAR>w : h ≫ f = k ≫ g<GOAL>G.map (pullback.lift h k w) ≫ pullbackComparison G f g = pullback.lift (G.map h) (G.map k) ⋯
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<GOAL>IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝¹ : DivisionRing α<VAR>inst✝ : CharZero α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<VAR>this : Invertible ↑n.succ<GOAL>IsRat (↑(Int.ofNat n.succ) * ⅟↑d)⁻¹ (Int.ofNat d) n.succ
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map prod.fst ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map prod.fst ((PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ((Types.binaryProductIso ↑(F.obj X) ↑(F.obj Y)).inv (x, y))) = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>((Types.binaryProductIso ↑(F.obj X) ↑(F.obj Y)).inv ≫ (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y).inv ≫ (F ⋙ FintypeCat.incl).map prod.fst) (x, y) = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>a / b ≤ 1 ↔ b ≤ a
<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✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<VAR>h : 0 < n<GOAL>orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1
<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✝ : Monoid G<VAR>a b x y : G<VAR>n✝ m n : ℕ<VAR>h : 0 < n<GOAL>(if h : 1 ∈ periodicPts fun x_1 => x * x_1 then Nat.find h else 0) = n ↔ IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ m < n, 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
<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✝⁷ : OrderedRing 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>inst✝ : NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R w x z<VAR>h₂ : Sbtw R x y z<GOAL>Sbtw R w y z
<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✝⁷ : OrderedRing 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>inst✝ : NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R z x w<VAR>h₂ : Sbtw R x y z<GOAL>Sbtw R w y z
<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✝⁷ : OrderedRing 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>inst✝ : NoZeroSMulDivisors R V<VAR>w x y z : P<VAR>h₁ : Wbtw R z x w<VAR>h₂ : Sbtw R z y x<GOAL>Sbtw R z y w
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<GOAL>lp.single p i (-a) = -lp.single p i a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<VAR>j : α<GOAL>↑(lp.single p i (-a)) j = ↑(-lp.single p i a) j
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>inst✝¹ : IsLocalization M S<VAR>R' : Type u_4<VAR>inst✝ : CommRing R'<VAR>g : S →+* R'<VAR>p : S[X]<VAR>x : R'<VAR>hx : eval₂ g x p = 0<VAR>b : ↥M<VAR>hb : Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p<GOAL>eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ✝ : Type w₃<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>γ : Type w'<VAR>ε : β ≃ γ<VAR>f : γ → C<VAR>inst✝¹ : HasCoproduct f<VAR>inst✝ : HasCoproduct (f ∘ ⇑ε)<VAR>b : β<GOAL>ι f (ε b) ≫ (reindex ε f).inv = ι (f ∘ ⇑ε) b
<VAR>a x : ℝ<GOAL>↑(oddKernel (↑a) x) = cexp (-↑π * ↑a ^ 2 * ↑x) * (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i : ι<GOAL>(hli.repr ⟨v i, ⋯⟩) i = 1
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : PosNum<GOAL>↑↑n = ↑n
<VAR>b p : ℕ<VAR>w : 0 < b<GOAL>↑(b ^ p - 1) = ↑b ^ p - 1
<VAR>b p : ℕ<VAR>w : 0 < b<VAR>this : 1 ≤ b ^ p<GOAL>↑(b ^ p - 1) = ↑b ^ p - 1
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>x✝ y✝ z✝ : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ≥0∞<VAR>z : α × β<GOAL>z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : StrongEpiMonoFactorisation f<VAR>F' : MonoFactorisation f<VAR>hF' : IsImage F'<GOAL>StrongEpi F'.e
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F : StrongEpiMonoFactorisation f<VAR>F' : MonoFactorisation f<VAR>hF' : IsImage F'<GOAL>StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m✝ : ℤ<VAR>z : Cochain F G n<VAR>m : ℤ<VAR>hnm : n + 1 = m<VAR>h : δ n m z = 0<GOAL>z ∈ cocycle F G n
<VAR>α : Type u_1<VAR>β : ?m.7267<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<GOAL>IsTopologicalBasis (lowerBasis α)
<VAR>α : Type u_1<VAR>β : ?m.7267<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<GOAL>lowerBasis α = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
<VAR>α : Type u_1<VAR>β : ?m.7267<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<GOAL>{s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : atBot.IsCountablyGenerated<VAR>μ : Measure α<VAR>a : α<VAR>this : Nonempty α<VAR>h_mono : Antitone fun x => μ (Ioc x a)<GOAL>Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (Iic a)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : atBot.IsCountablyGenerated<VAR>μ : Measure α<VAR>a : α<VAR>this : Nonempty α<VAR>h_mono : Antitone fun x => μ (Ioc x a)<GOAL>μ (Iic a) = ⨆ i, μ (Ioc i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : atBot.IsCountablyGenerated<VAR>μ : Measure α<VAR>a : α<VAR>this : Nonempty α<VAR>h_mono : Antitone fun x => μ (Ioc x a)<VAR>xs : ℕ → α<VAR>hxs_mono : Antitone xs<VAR>hxs_tendsto : Tendsto xs atTop atBot<GOAL>μ (Iic a) = ⨆ i, μ (Ioc i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : atBot.IsCountablyGenerated<VAR>μ : Measure α<VAR>a : α<VAR>this : Nonempty α<VAR>h_mono : Antitone fun x => μ (Ioc x a)<VAR>xs : ℕ → α<VAR>hxs_mono : Antitone xs<VAR>hxs_tendsto : Tendsto xs atTop atBot<VAR>h_Iic : Iic a = ⋃ n, Ioc (xs n) a<GOAL>μ (Iic a) = ⨆ i, μ (Ioc i a)