ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>y : R<VAR>hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range<VAR>hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<GOAL>C y ∈ I
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R[X]<VAR>i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>y : R<VAR>hx' : ((Quotient.mk I).comp C) y ∈ ((Quotient.mk I).comp C).range<VAR>hx : C ⟨((Quotient.mk I).comp C) y, hx'⟩ ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I<GOAL>C (i y) ∈ map (mapRingHom i) I
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : σ → τ<VAR>inst✝ : DecidableEq τ<VAR>h : Injective f<GOAL>((rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : σ → τ<VAR>inst✝ : DecidableEq τ<VAR>h : Injective f<GOAL>support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<VAR>n : ℕ<GOAL>(N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op [n]) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))<GOAL>(N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>P : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>eq₁ : (N₂Γ₂.inv.app (N₂.obj P)).f.f n = PInfty.f n ≫ P.p.app (op [n]) ≫ ((Γ₀.splitting (N₂.obj P).X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))<VAR>eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op [n])<GOAL>(N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<VAR>h : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)<GOAL>∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<VAR>h : ∀ (i j : Fin n), i < j → (f ∘ ⇑σ) i ≤ (f ∘ ⇑σ) j<GOAL>f ∘ ⇑σ = f ∘ ⇑(sort f)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : Z ⟶ Y<VAR>g : Z ⟶ X<VAR>H : f ≫ α.inv = g<GOAL>f = g ≫ α.hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>(singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j = f ≫ (singleObjCyclesSelfIso c j B).inv
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' G'' : G.Subgraph<VAR>s s' : Set V<GOAL>G'.induce s' ≤ G'.induce (s ∪ s')
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X : T<VAR>A B : Under X<VAR>f : A ⟶ B<GOAL>A.hom ≫ f.right = B.hom
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X : T<VAR>A B : Under X<VAR>f : A ⟶ B<VAR>this : (Functor.fromPUnit X).map f.left ≫ B.hom = A.hom ≫ (𝟭 T).map f.right<GOAL>A.hom ≫ f.right = B.hom
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
<VAR>α✝ : Type u<VAR>inst✝⁵ : Group α✝<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : CovariantClass α✝ α✝ (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α✝<VAR>α : Type u_1<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a / b ≤ b / a ↔ a ≤ b
<VAR>α✝ : Type u<VAR>inst✝⁵ : Group α✝<VAR>inst✝⁴ : LinearOrder α✝<VAR>inst✝³ : CovariantClass α✝ α✝ (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c : α✝<VAR>α : Type u_1<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a / b ≤ a⁻¹ * b ↔ a ≤ b
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X A B : C<VAR>f : A ⟶ X<VAR>g : B ⟶ X<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>h : F.map f a = F.map g b<GOAL>((Types.pullbackIsoPullback (F.map f) (F.map g)).inv ≫ (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (pullback.fst f g)) ⟨(a, b), h⟩ = a
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>e : f ≅ g<GOAL>e.hom.right ≫ e.inv.right = 𝟙 f.right
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : IsProbabilityMeasure μ'<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : IsProbabilityMeasure μ'<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<VAR>this : CompactSpace G<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : IsProbabilityMeasure μ'<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<VAR>this : CompactSpace G<VAR>A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : IsProbabilityMeasure μ'<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<VAR>this : CompactSpace G<VAR>A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s<VAR>Z : μ' univ = μ'.haarScalarFactor μ • μ univ<GOAL>μ' = μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : IsProbabilityMeasure μ'<VAR>inst✝¹ : μ.IsHaarMeasure<VAR>inst✝ : μ'.IsHaarMeasure<VAR>this : CompactSpace G<VAR>A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s<VAR>Z : 1 = μ'.haarScalarFactor μ<GOAL>μ' = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>↑(hf.stieltjesFunction a) x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>r : ℚ<VAR>hrx : x < ↑r<GOAL>↑(hf.stieltjesFunction a) x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>r : ℚ<VAR>hrx : x < ↑r<GOAL>⨅ r, ↑(hf.stieltjesFunction a) ↑↑r ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>r : ℚ<VAR>hrx : x < ↑r<GOAL>⨅ r, f a ↑r ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>r : ℚ<VAR>hrx : x < ↑r<GOAL>BddBelow (range fun r => f a ↑r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>r : ℚ<VAR>hrx : x < ↑r<GOAL>{ r' // x < ↑r' }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>⨅ b, ∫⁻ (a_1 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) ↑↑b) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>∀ (b : { r' // x < ↑r' }), ∫⁻ (a_1 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) ↑↑b) ∂ν a ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>Directed (fun x x_1 => x ≥ x_1) fun r b => ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<VAR>q : { r' // x < ↑r' }<GOAL>Measurable fun b => ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>⨅ b, (κ a) (s ×ˢ Iic ↑↑b) = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>(κ a) (⋂ i, s ×ˢ Iic ↑↑i) = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>∀ (i : { r' // x < ↑r' }), MeasurableSet (s ×ˢ Iic ↑↑i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>Directed (fun x x_1 => x ⊇ x_1) fun b => s ×ˢ Iic ↑↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hρ_zero : ¬(ν a).restrict s = 0<VAR>h : ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a<VAR>h_nonempty : Nonempty { r' // x < ↑r' }<GOAL>∃ i, (κ a) (s ×ˢ Iic ↑↑i) ≠ ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : lcm a b = 0<GOAL>a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<VAR>h : lcm a b = 0<VAR>this : Associated (a * b) 0<GOAL>a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b : α<GOAL>a = 0 ∨ b = 0 → lcm a b = 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>orderOf 1 = p ^ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a✝ b✝ : G<VAR>hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}<VAR>hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}<GOAL>∃ m, (a✝ * b✝) ^ p ^ m = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a✝ b✝ : G<VAR>hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}<VAR>hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}<VAR>m : ℕ<VAR>hm : a✝ ^ p ^ m = 1<GOAL>∃ m, (a✝ * b✝) ^ p ^ m = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a✝ b✝ : G<VAR>hg₁ : a✝ ∈ {g | ∃ n, orderOf g = p ^ n}<VAR>hg₂ : b✝ ∈ {g | ∃ n, orderOf g = p ^ n}<VAR>m : ℕ<VAR>hm : a✝ ^ p ^ m = 1<VAR>n : ℕ<VAR>hn : b✝ ^ p ^ n = 1<GOAL>∃ m, (a✝ * b✝) ^ p ^ m = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>a : R<VAR>p : Module.Dual R M × M<GOAL>(a • p).1 (a • p).2 = (a * a) • p.1 p.2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>p q : Module.Dual R M × M<GOAL>(p + q).1 (p + q).2 = p.1 p.2 + q.1 q.2 + ((LinearMap.dualProd R M) p) q
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : s ≪ᵥ μ.toENNRealVectorMeasure<GOAL>μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ<GOAL>μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : s.totalVariation ≪ μ.toENNRealVectorMeasure.ennrealToMeasure<GOAL>μ.toENNRealVectorMeasure.ennrealToMeasure = μ
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)<GOAL>abscissaOfAbsConv f ≤ ↑x + 1
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)<VAR>H : ↑x + 1 < abscissaOfAbsConv f<GOAL>False
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)<VAR>H : ↑x + 1 < abscissaOfAbsConv f<VAR>y : ℝ<VAR>hy₁ : ↑x + 1 < ↑y<VAR>hy₂ : ↑y < abscissaOfAbsConv f<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semigroup β<VAR>f : α → β<VAR>x : α<VAR>y : FreeSemigroup α<GOAL>(lift f) (of x * y) = f x * (lift f) y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<GOAL>IsClosed s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<GOAL>IsClosed s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<GOAL>closure s ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : x ∈ closure s<GOAL>x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<GOAL>x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<VAR>y : α<VAR>hy : y ∈ ball x V₁<VAR>hy' : y ∈ s<GOAL>x = y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<VAR>y : α<VAR>hy : y ∈ ball x V₁<VAR>hy' : y ∈ s<GOAL>∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (x, y) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<VAR>y : α<VAR>hy : y ∈ ball x V₁<VAR>hy' : y ∈ s<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>a✝ : SymmetricRel V<GOAL>(x, y) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<VAR>y : α<VAR>hy : y ∈ ball x V₁<VAR>hy' : y ∈ s<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>a✝ : SymmetricRel V<VAR>z : α<VAR>hz : z ∈ ball x (V₁ ∩ V)<VAR>hz' : z ∈ s<GOAL>(x, y) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>s : Set α<VAR>hs : s.Pairwise fun x y => (x, y) ∉ V₀<VAR>V₁ : Set (α × α)<VAR>V₁_in : V₁ ∈ 𝓤 α<VAR>V₁_symm : SymmetricRel V₁<VAR>h_comp : V₁ ○ V₁ ⊆ V₀<VAR>x : α<VAR>hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>a✝ : SymmetricRel V<VAR>z : α<VAR>hz : z ∈ ball x (V₁ ∩ V)<VAR>hz' : z ∈ s<VAR>hy : z ∈ ball x V₁<VAR>hy' : z ∈ s<GOAL>(x, z) ∈ V
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : Group G<VAR>inst✝² : PseudoMetricSpace G<VAR>inst✝¹ : IsometricSMul G G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>nndist (a / b) (a / c) = nndist b c
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<GOAL>a / c * b / a ≤ b / c
<VAR>a b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>b c : ℕ<GOAL>0 / c * b / 0 ≤ b / c
<VAR>a✝ b✝ c✝ d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b c : ℕ<VAR>ha : a > 0<GOAL>a / c * b / a ≤ b / c