ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I = spanSingleton R⁰ ((algebraMap R K) (choose ⋯))⁻¹ * ↑(choose ⋯)<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I = spanSingleton R⁰ ((algebraMap R K) (choose ⋯))⁻¹ * ↑(choose ⋯)<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ count K v I = ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I = spanSingleton R⁰ ((algebraMap R K) (choose ⋯))⁻¹ * ↑(choose ⋯)<GOAL>∀ (x : HeightOneSpectrum R), ↑x.asIdeal ^ count K x I = ↑x.asIdeal ^ (↑((Associates.mk x.asIdeal).count (Associates.mk (choose ⋯)).factors) - ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I = spanSingleton R⁰ ((algebraMap R K) (choose ⋯))⁻¹ * ↑(choose ⋯)<VAR>w : HeightOneSpectrum R<GOAL>count K w I = ↑((Associates.mk w.asIdeal).count (Associates.mk (choose ⋯)).factors) - ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp1 : p % 4 = 1<VAR>hq1 : q ≠ 2<GOAL>IsSquare ↑q ↔ IsSquare ↑p
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp1 : p % 4 = 1<VAR>hq1 : q ≠ 2<VAR>h : p = q<GOAL>IsSquare ↑q ↔ IsSquare ↑p
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp1 : p % 4 = 1<VAR>hq1 : q ≠ 2<VAR>h : p ≠ q<GOAL>IsSquare ↑q ↔ IsSquare ↑p
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < (zipWith f l l').length<GOAL>i < l'.length
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>f : α → β → γ<VAR>i : ℕ<VAR>l : List α<VAR>l' : List β<VAR>h : i < min l.length l'.length<GOAL>i < l'.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝² : CountableInterFilter l<VAR>f g : α → β<VAR>inst✝¹ : Nonempty α<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ a, {a} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝² : CountableInterFilter l<VAR>f g : α → β<VAR>inst✝¹ : Nonempty α<VAR>p : Set α → Prop<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>inst✝ : HasCountableSeparatingOn α p ∅<VAR>hs : ∅ ∈ l<GOAL>∃ a, {a} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝² : CountableInterFilter l<VAR>f g : α → β<VAR>inst✝¹ : Nonempty α<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>hne : s.Nonempty<GOAL>∃ a, {a} ∈ l
<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 [MOD p]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : NormedSpace ℝ E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>hne : f x ≠ g x<GOAL>DifferentiableAt ℝ (fun y => ‖f y - g y‖) x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<GOAL>Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>h : Tendsto (fun x => c * x ^ n) atTop atTop<GOAL>n ≠ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>h : Tendsto (fun x => c * x ^ n) atTop atTop<GOAL>0 < c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : Filter α<VAR>s : Set α<VAR>h : f ⊓ 𝓟 sᶜ = ⊥<GOAL>s ∈ f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>A : Set (Ideal R)<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>(∀ J ∈ A, RingHom.ker f ≤ J) → map f (sInf A) = sInf (map f '' A)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>A : Set (Ideal R)<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>h : ∀ J ∈ A, RingHom.ker f ≤ J<GOAL>∀ b ∈ map f '' A, map f (sInf A) ≤ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>A : Set (Ideal R)<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>h : ∀ J ∈ A, RingHom.ker f ≤ J<GOAL>sInf (map f '' A) ≤ map f (sInf A)
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>x✝¹ x✝ : ℕ<VAR>num✝ : ℤ<VAR>denom✝ : ℕ<VAR>inv✝ : Invertible ↑denom✝<VAR>eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝<GOAL>OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝
<VAR>i j : ℤ<VAR>H : j ∣ i<GOAL>i.gcd j = j.natAbs
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>h₀ : x 0 < y 0<VAR>hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)<GOAL>x 0 < y 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f : α → α<VAR>x y : ℕ → α<VAR>hf : Monotone f<VAR>h₀ : x 0 < y 0<VAR>n✝ : ℕ<VAR>hx : ∀ (k : ℕ), k < n✝ + 1 → x (k + 1) < f (x k)<VAR>hy : ∀ (k : ℕ), k < n✝ + 1 → f (y k) ≤ y (k + 1)<GOAL>x (n✝ + 1) < y (n✝ + 1)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>s : Set G<VAR>g : G<VAR>S : Set G<VAR>hS : closure S = ⊤<GOAL>center G = ⨅ g, centralizer ↑(zpowers ↑g)
<VAR>a b m n : ℕ+<VAR>cop : m.Coprime n<VAR>am : a ∣ m<VAR>bn : b ∣ n<GOAL>a = m.gcd (a * b)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>f : CauSeq K norm<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>|(fun n => re (↑f n)) j - (fun n => re (↑f n)) i| ≤ ‖↑f j - ↑f i‖
<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>s : ι → ℕ<VAR>x : ℕ<GOAL>(∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>f : R ≃+* S<VAR>K : NonUnitalSubsemiring R<VAR>x : S<GOAL>x ∈ map (↑f) K ↔ f.symm x ∈ K
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>l : Filter α<GOAL>(rmap s (rmap r l)).sets = (rmap (r.comp s) l).sets
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>ι : Type u_7<VAR>s : ι → Set α<VAR>x : α →₀ M<GOAL>x ∈ supported M R (⋂ i, s i) ↔ x ∈ ⨅ i, supported M R (s i)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : Fintype (ConjClasses G)<VAR>inst✝¹ : Fintype G<VAR>inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier<GOAL>∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : Fintype (ConjClasses G)<VAR>inst✝¹ : Fintype G<VAR>inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier<GOAL>(x : ConjClasses G) × ↑x.carrier ≃ G
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: β)<VAR>x : β<GOAL>M.dest (P F) (corecF g x) = (TypeVec.id ::: corecF g) <$$> repr (g x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g✝ : ι → α<VAR>g : ι → β<VAR>b : β<VAR>hg : Tendsto g p (𝓝 b)<VAR>p' : Filter α<GOAL>TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>hI : I.FG<GOAL>(reesAlgebra I).FG
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hnon : (σ a).Nonempty<VAR>a✝ : Nontrivial A<GOAL>σ ((aeval a) p) = (fun k => eval k p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hnon : (σ a).Nonempty<VAR>a✝ : Nontrivial A<VAR>h : p.degree ≤ 0<GOAL>σ ((aeval a) p) = (fun k => eval k p) '' σ a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : IsAlgClosed 𝕜<VAR>a : A<VAR>p : 𝕜[X]<VAR>hnon : (σ a).Nonempty<VAR>a✝ : Nontrivial A<VAR>h : p.degree ≤ 0<GOAL>σ ((aeval a) (C (p.coeff 0))) = (fun k => eval k (C (p.coeff 0))) '' σ a
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<GOAL>HasGradientWithinAt f f' univ x ↔ HasGradientAt f f' x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<GOAL>HasFDerivWithinAt f ((toDual 𝕜 F) f') univ x ↔ HasFDerivAt f ((toDual 𝕜 F) f') x
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>l : Multiset { a // Irreducible a }<GOAL>BfactorSetMem ⟨p, hp⟩ ↑l ↔ Mem ⟨p, hp⟩ l
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>Function.Injective ⇑(algebraMap Fq[X] ↥(ringOfIntegers Fq F))
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>hinj : Function.Injective ⇑(algebraMap Fq[X] F)<GOAL>Function.Injective ⇑(algebraMap Fq[X] ↥(ringOfIntegers Fq F))
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>hinj : Function.Injective ⇑(algebraMap Fq[X] F)<GOAL>∀ (a : Fq[X]), (algebraMap Fq[X] ↥(ringOfIntegers Fq F)) a = 0 → a = 0
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>hinj : Function.Injective ⇑(algebraMap Fq[X] F)<VAR>p : Fq[X]<VAR>hp : (algebraMap Fq[X] ↥(ringOfIntegers Fq F)) p = 0<GOAL>p = 0
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>hinj : Function.Injective ⇑(algebraMap Fq[X] F)<VAR>p : Fq[X]<VAR>hp : ↑((algebraMap Fq[X] ↥(ringOfIntegers Fq F)) p) = 0<GOAL>p = 0
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<VAR>hinj : ∀ (a : Fq[X]), (algebraMap Fq[X] F) a = 0 → a = 0<VAR>p : Fq[X]<VAR>hp : ↑((algebraMap Fq[X] ↥(ringOfIntegers Fq F)) p) = 0<GOAL>p = 0
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>gluedLift 𝒰 f g s ≫ p1 𝒰 f g = s.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>(𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g = (𝒰.pullbackCover s.fst).fromGlued ≫ s.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<GOAL>∀ (b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R), Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g = Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ s.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g = Multicoequalizer.π (𝒰.pullbackCover s.fst).gluedCover.diagram b ≫ (𝒰.pullbackCover s.fst).fromGlued ≫ s.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>((𝒰.pullbackCover s.fst).map b ≫ (𝒰.pullbackCover s.fst).glueMorphisms (fun i => ((pullbackSymmetry s.fst (𝒰.map i)).hom ≫ pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯) ≫ (gluing 𝒰 f g).ι i) ⋯) ≫ p1 𝒰 f g = (𝒰.pullbackCover s.fst).map b ≫ s.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>b : (𝒰.pullbackCover s.fst).gluedCover.diagram.R<GOAL>(((pullbackSymmetry s.fst (𝒰.map b)).hom ≫ pullback.map (𝒰.map b) s.fst (𝒰.map b ≫ f) g (𝟙 (𝒰.obj b)) s.snd f ⋯ ⋯) ≫ (gluing 𝒰 f g).ι b) ≫ p1 𝒰 f g = (𝒰.pullbackCover s.fst).map b ≫ s.fst
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝ : CharZero R<VAR>n m : ℕ<VAR>hnm : cyclotomic n R = cyclotomic m R<GOAL>n = m
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharZero R<VAR>m : ℕ<VAR>hnm : cyclotomic 0 R = cyclotomic m R<GOAL>0 = m
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝ : CharZero R<VAR>n m : ℕ<VAR>hnm : cyclotomic n R = cyclotomic m R<VAR>hzero : n ≠ 0<GOAL>n = m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>ι : Sort u_4<VAR>p : ι → Subsemigroup M<GOAL>⨆ i, p i = closure (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : LinearOrderedCommRing S<VAR>n : Type u_3<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (i j : n), abv (A i j) ≤ x<VAR>σ : Perm n<VAR>x✝ : σ ∈ univ<GOAL>abv (Perm.sign σ • ∏ i : n, A (σ i) i) = ∏ i : n, abv (A (σ i) i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : LinearOrderedCommRing S<VAR>n : Type u_3<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (i j : n), abv (A i j) ≤ x<VAR>x✝¹ : Perm n<VAR>x✝ : x✝¹ ∈ univ<GOAL>∏ _i : n, x = x ^ Fintype.card n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : LinearOrderedCommRing S<VAR>n : Type u_3<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (i j : n), abv (A i j) ≤ x<GOAL>∑ _σ : Perm n, x ^ Fintype.card n = (Fintype.card n).factorial • x ^ Fintype.card n
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>cosZeta a s = (expZeta a s + expZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>Tendsto (fun n => f x - f 1 - x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f x - f 1))
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>∀ᶠ (b : ℕ) in atTop, (fun n => f x - f 1 - x * (log (↑n + 1) - log ↑n)) b ≤ logGammaSeq x b
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>∀ᶠ (b : ℕ) in atTop, logGammaSeq x b ≤ f x - f 1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ W X Y Z : C<VAR>inst✝¹ : HasBinaryCoproduct W Y<VAR>inst✝ : HasBinaryCoproduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>desc (g ≫ inl) (g' ≫ inr) = map g g'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ W X Y Z : C<VAR>inst✝¹ : HasBinaryCoproduct W Y<VAR>inst✝ : HasBinaryCoproduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>map g g' ≫ desc inl inr = map g g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<GOAL>∀ᵐ (x : γ) ∂κ.fst a, Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>x : γ<VAR>hx : κ.densityProcess κ.fst n a x univ = 1<GOAL>Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>inst✝ : IsFiniteKernel κ<VAR>n : ℕ<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>x : γ<VAR>hx : κ.densityProcess κ.fst n a x univ = 1<GOAL>Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<GOAL>(mkMetric' m) (s ∪ t) = (mkMetric' m) s + (mkMetric' m) t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<GOAL>(fun r => (mkMetric'.pre m r) (s ∪ t)) =ᶠ[𝓝[>] 0] fun x => (mkMetric'.pre m x) s + (mkMetric'.pre m x) t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<GOAL>(fun r => (mkMetric'.pre m r) (s ∪ t)) =ᶠ[𝓝[>] 0] fun x => (mkMetric'.pre m x) s + (mkMetric'.pre m x) t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<GOAL>∀ a ∈ Ioo 0 r, (mkMetric'.pre m a) (s ∪ t) = (mkMetric'.pre m a) s + (mkMetric'.pre m a) t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>ε : ℝ≥0∞<VAR>left✝ : 0 < ε<VAR>εr : ε < r<GOAL>(mkMetric'.pre m ε) (s ∪ t) = (mkMetric'.pre m ε) s + (mkMetric'.pre m ε) t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>ε : ℝ≥0∞<VAR>left✝ : 0 < ε<VAR>εr : ε < r<GOAL>∀ (u : Set X), (s ∩ u).Nonempty → (t ∩ u).Nonempty → extend (fun s x => m s) u = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>ε : ℝ≥0∞<VAR>left✝ : 0 < ε<VAR>εr : ε < r<VAR>u : Set X<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu : x ∈ u<VAR>y : X<VAR>hyt : y ∈ t<VAR>hyu : y ∈ u<GOAL>extend (fun s x => m s) u = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : Set X → ℝ≥0∞<VAR>s t : Set X<VAR>r : ℝ≥0∞<VAR>r0 : 0 < r<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>ε : ℝ≥0∞<VAR>left✝ : 0 < ε<VAR>εr : ε < r<VAR>u : Set X<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu : x ∈ u<VAR>y : X<VAR>hyt : y ∈ t<VAR>hyu : y ∈ u<VAR>this : ε < diam u<GOAL>extend (fun s x => m s) u = ⊤
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y✝ : α i.succ<VAR>z x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<VAR>s : {i : Fin n.succ} → α i → α i → Prop<GOAL>Pi.Lex (fun x x_1 => x < x_1) s (cons x₀ x) (cons y₀ y) ↔ s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i => s) x y
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y✝ : α i.succ<VAR>z x₀ y₀ : α 0<VAR>x y : (i : Fin n) → α i.succ<VAR>s : {i : Fin n.succ} → α i → α i → Prop<GOAL>(((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨ ∃ i, ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧ s (x i) (y i)) ↔ s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ j < i, x j = y j) ∧ s (x i) (y i)
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidablePred fun x => c ≤ x<VAR>hca : c ≤ a<GOAL>filter (fun x => c ≤ x) (Ico a b) = Ico a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.prod ⊤ = comap Prod.fst f