ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p ∧ p < ⊤<VAR>f : (i : α) → E i<GOAL>(if p = 0 then {i | ¬f i = 0}.Finite else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ p.toReal) ↔ Summable fun i => ‖f i‖ ^ p.toReal
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<GOAL>ord I i < o
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬ord I i < o<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬ord I i < o<GOAL>eval C l ∈ Submodule.span ℤ (eval C '' {m | m < l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬ord I i < o<GOAL>eval C l = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬ord I i < o<VAR>x : ↑C<GOAL>(eval C l) x = 0 x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>h' : ¬ord I i < o<VAR>x : ↑C<GOAL>(∀ i ∈ ↑l, ↑x i = true) → False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o : Ordinal.{u}<VAR>h : isGood C l<VAR>hsC : contained C o<VAR>i : I<VAR>hi : i ∈ ↑l<VAR>x : ↑C<VAR>h' : (∀ i ∈ ↑l, ↑x i = true) ∧ ¬False<GOAL>ord I i < o
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : Semiring L<VAR>inst✝ : Nontrivial L<VAR>f : K →+* L<VAR>p : ℕ<GOAL>CharP K p ↔ CharP L p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun x => f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>this : UniformContinuous fun x => f x / (g x)⁻¹<GOAL>UniformContinuous fun x => f x * g x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : P.obj (op B)<VAR>ij : I × I<GOAL>Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ firstMap P X π) x) = Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ secondMap P X π) x)
<VAR>n p a k : ℕ<VAR>hp : Prime p<GOAL>a ^ k = p ↔ a = p ∧ k = 1
<VAR>n p a k : ℕ<VAR>hp : Prime p<VAR>h : a ^ k = p<GOAL>a = p ∧ k = 1
<VAR>n p a k : ℕ<VAR>hp : Prime (a ^ k)<VAR>h : a ^ k = p<GOAL>a = p ∧ k = 1
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<VAR>t : X → Y := s ∘ f ∘ stoneCechUnit<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<VAR>t : X → Y := s ∘ f ∘ stoneCechUnit<VAR>ht : Continuous t<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<VAR>t : X → Y := s ∘ f ∘ stoneCechUnit<VAR>ht : Continuous t<VAR>h : StoneCech X → Y := stoneCechExtend ht<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<VAR>t : X → Y := s ∘ f ∘ stoneCechUnit<VAR>ht : Continuous t<VAR>h : StoneCech X → Y := stoneCechExtend ht<VAR>hh : Continuous h<GOAL>∃ h, Continuous h ∧ g ∘ h = f
<VAR>X : Type u<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : DiscreteTopology X<VAR>Y Z : Type u<VAR>_tsY : TopologicalSpace Y<VAR>_tsZ : TopologicalSpace Z<VAR>_csY : CompactSpace Y<VAR>_t2Y : T2Space Y<VAR>_csZ✝ : CompactSpace Z<VAR>_csZ : T2Space Z<VAR>f : StoneCech X → Z<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>g_sur : Surjective g<VAR>s : Z → Y := fun z => Classical.choose ⋯<VAR>hs : g ∘ s = id<VAR>t : X → Y := s ∘ f ∘ stoneCechUnit<VAR>ht : Continuous t<VAR>h : StoneCech X → Y := stoneCechExtend ht<VAR>hh : Continuous h<GOAL>(g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>j : JordanDecomposition α<VAR>h : s = j.toSignedMeasure<GOAL>s.toJordanDecomposition = j
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f q<VAR>hpq : q ≤ p<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f 0<VAR>hpq : 0 ≤ 0<GOAL>Memℓp f 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f 0<VAR>hpq : 0 ≤ ⊤<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>f : (i : α) → E i<VAR>hp : 0 < p.toReal<VAR>hfq : Memℓp f 0<VAR>hpq : 0 ≤ p<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f ⊤<VAR>hpq : ⊤ ≤ ⊤<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>q : ℝ≥0∞<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f q<VAR>hq : 0 < q.toReal<VAR>hpq : q ≤ ⊤<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q✝ : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f q<VAR>hpq : q ≤ p<VAR>hq : 0 < q.toReal<VAR>left✝ : 0 < p.toReal<VAR>hpq' : q.toReal ≤ p.toReal<GOAL>Memℓp f p
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsAlgClosed K<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : Nontrivial V<VAR>f : End K V<GOAL>∃ c, f.HasEigenvalue c
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsAlgClosed K<VAR>inst✝¹ : FiniteDimensional K V<VAR>inst✝ : Nontrivial V<VAR>f : End K V<GOAL>∃ c, c ∈ spectrum K f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono g<GOAL>Mono t.fst
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono g<VAR>W : C<VAR>h k : W ⟶ t.pt<VAR>i : h ≫ t.fst = k ≫ t.fst<GOAL>h ≫ t.snd = k ≫ t.snd
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W✝ X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<VAR>inst✝ : Mono g<VAR>W : C<VAR>h k : W ⟶ t.pt<VAR>i : h ≫ t.fst = k ≫ t.fst<GOAL>h ≫ t.fst ≫ f = k ≫ t.fst ≫ f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : F<VAR>hf : range f = ⊤<VAR>p p' : Submodule R₂ M₂<VAR>H : comap f p ≤ comap f p'<VAR>x : M₂<VAR>hx : x ∈ p<GOAL>x ∈ p'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : F<VAR>hf : range f = ⊤<VAR>p p' : Submodule R₂ M₂<VAR>H : comap f p ≤ comap f p'<VAR>y : M<VAR>hx : f y ∈ p<GOAL>f y ∈ p'
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>D ⊆ A ↓∩ ↑E ↔ D ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
<VAR>q a✝ b c a : ℚ<GOAL>0 ≤ a ∨ 0 ≤ -a
<VAR>q a✝ b c a : ℚ<GOAL>0 ≤ a.num ∨ a.num ≤ 0
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>hf' : eval a (derivative f) ≠ 0<GOAL>IsCoprime (X - C a) (f /ₘ (X - C a))
<VAR>f : StieltjesFunction<VAR>a : ℝ<GOAL>f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>u : ℕ → ℝ<VAR>u_mono : StrictMono u<VAR>u_lt_a : ∀ (n : ℕ), u n < a<VAR>u_lim : Tendsto u atTop (𝓝 a)<GOAL>f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>u : ℕ → ℝ<VAR>u_mono : StrictMono u<VAR>u_lt_a : ∀ (n : ℕ), u n < a<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : {a} = ⋂ n, Ioc (u n) a<GOAL>f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>u : ℕ → ℝ<VAR>u_mono : StrictMono u<VAR>u_lt_a : ∀ (n : ℕ), u n < a<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : {a} = ⋂ n, Ioc (u n) a<VAR>L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))<GOAL>f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
<VAR>f : StieltjesFunction<VAR>a : ℝ<VAR>u : ℕ → ℝ<VAR>u_mono : StrictMono u<VAR>u_lt_a : ∀ (n : ℕ), u n < a<VAR>u_lim : Tendsto u atTop (𝓝 a)<VAR>A : {a} = ⋂ n, Ioc (u n) a<VAR>L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a}))<VAR>L2 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (↑f a - leftLim (↑f) a)))<GOAL>f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<GOAL>(spectrum R A).Finite
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field R<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n R<GOAL>(spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝ : Add α<VAR>a₀ a₁ a₂ b₀ b₁ b₂ : α<GOAL>![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<GOAL>(span 𝕜 (Set.range fun i => b.repr.symm (lp.single 2 i 1))).topologicalClosure = ⊤
<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 : C<GOAL>((single C c j).obj A).homologyι j ≫ (singleObjOpcyclesSelfIso c j A).inv = (singleObjHomologySelfIso c j A).hom
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y L : A<GOAL>(baseChange W B).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map (↑f) ((baseChange W A).toAffine.addPolynomial x y L)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y L : A<GOAL>(baseChange W B).toAffine.addPolynomial (f x) (f y) (f L) = (baseChange W B).toAffine.addPolynomial (↑f x) (↑f y) (↑f L)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ : X ≃ₜ Y<VAR>e' : Y ≃ₜ Z<VAR>e : X ≃ₜ Y<VAR>f : PartialHomeomorph Y Z<VAR>f' : PartialHomeomorph Z Z'<GOAL>(e.transPartialHomeomorph f).trans f' = e.transPartialHomeomorph (f.trans f')
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>D₃ : Type u₆<VAR>inst✝⁹ : Category.{v₁, u₁} C₁<VAR>inst✝⁸ : Category.{v₂, u₂} C₂<VAR>inst✝⁷ : Category.{v₃, u₃} C₃<VAR>inst✝⁶ : Category.{v₄, u₄} D₁<VAR>inst✝⁵ : Category.{v₅, u₅} D₂<VAR>inst✝⁴ : Category.{v₆, u₆} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G : D₁ ⥤ D₂<VAR>inst✝¹ : CatCommSq Φ.functor L₁ L₂ G<VAR>inst✝ : G.IsEquivalence<GOAL>(Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>D₃ : Type u₆<VAR>inst✝⁹ : Category.{v₁, u₁} C₁<VAR>inst✝⁸ : Category.{v₂, u₂} C₂<VAR>inst✝⁷ : Category.{v₃, u₃} C₃<VAR>inst✝⁶ : Category.{v₄, u₄} D₁<VAR>inst✝⁵ : Category.{v₅, u₅} D₂<VAR>inst✝⁴ : Category.{v₆, u₆} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G : D₁ ⥤ D₂<VAR>inst✝¹ : CatCommSq Φ.functor L₁ L₂ G<VAR>inst✝ : G.IsEquivalence<GOAL>G.IsEquivalence
<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>x y : F<GOAL>⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<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>x y : F<VAR>this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ<GOAL>⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<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>x y : F<VAR>this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ<GOAL>⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>x y : E<GOAL>dist x⁻¹ y = dist x y⁻¹
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f_dom : Submodule R E<VAR>f g : ↥f_dom →ₗ[R] F<VAR>h' : ∀ ⦃x : ↥{ domain := f_dom, toFun := f }.domain⦄ ⦃y : ↥{ domain := f_dom, toFun := g }.domain⦄, ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := g } y<GOAL>{ domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f_dom : Submodule R E<VAR>f : ↥f_dom →ₗ[R] F<VAR>h' : ∀ ⦃x y : ↥{ domain := f_dom, toFun := f }.domain⦄, ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := f } y<GOAL>{ domain := f_dom, toFun := f } = { domain := f_dom, toFun := f }
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>f : α → β<GOAL>map f s = 0 ↔ s = 0
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.236298}<VAR>α : Type u_1<VAR>l : List α<VAR>h : ↑l.length < #α<GOAL>∃ z, z ∉ l
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.236298}<VAR>α : Type u_1<VAR>l : List α<VAR>h : ∀ (z : α), z ∈ l<GOAL>#α ≤ ↑l.length
<VAR>n i : ℕ<VAR>h : n < 2 ^ i<GOAL>n.testBit i = false
<VAR>x y✝ z : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>y : ℝ<VAR>n : ℕ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>s t : (CostructuredArrow yoneda A)ᵒᵖ<VAR>f : t ⟶ s<VAR>x : F.obj t<GOAL>counitForward F (unop s) (F.map f x) = (counitForward F (unop t) x).map₂ f.unop.left ⋯
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>s t : (CostructuredArrow yoneda A)ᵒᵖ<VAR>f : t ⟶ s<VAR>x : F.obj t<GOAL>F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) = YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X : C<VAR>s t : (CostructuredArrow yoneda A)ᵒᵖ<VAR>f : t ⟶ s<VAR>x : F.obj t<VAR>this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯<GOAL>F.map (eqToHom ⋯) (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) = YonedaCollection.snd (counitForward F (unop s) (F.map f x)).val
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : M' →ₗ[R] M''<VAR>hl : l ∘ₗ f = g<GOAL>LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm = l
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : M' →ₗ[R] M''<VAR>hl : l ∘ₗ f = g<GOAL>(l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : M' →ₗ[R] M''<VAR>hl : l ∘ₗ f = g<GOAL>l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f