ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<GOAL>limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) ⊥ (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) ⊥ (F i)) _auto✝<GOAL>limsup (fun a => s.sup fun i => F i a) ⊥ = s.sup fun i => limsup (F i) ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h✝ : f.NeBot<GOAL>limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>h✝ : f.NeBot<VAR>h₁ : autoParam (∀ i ∈ ∅, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ ∅, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<GOAL>limsup (fun a => ∅.sup fun i => F i a) f = ∅.sup fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h✝ : f.NeBot<VAR>s_nemp : s.Nonempty<GOAL>limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h✝ : f.NeBot<VAR>s_nemp : s.Nonempty<GOAL>limsup (fun a => s.sup fun i => F i a) f = limsup (fun a => s.sup' s_nemp fun i => F i a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x x_1 => x ≤ x_1) f (F i)) _auto✝<VAR>h✝ : f.NeBot<VAR>s_nemp : s.Nonempty<VAR>a : α<GOAL>(s.sup fun i => F i a) = s.sup' s_nemp fun i => F i a
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq α<VAR>h : t.Nonempty<GOAL>image2 (fun x x_1 => x) ↑s ↑t = ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p q : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>((monomial n) a).aroots S = n • {0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>n : ℕ<VAR>i : Fin n<VAR>v : Fin n.succ → M<GOAL>∏ j ∈ Ioi i.succ, v j = ∏ j ∈ Ioi i, v j.succ
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : ↑G'.verts<VAR>inst✝¹ : Fintype ↑(G'.coe.neighborSet v)<VAR>inst✝ : Fintype ↑(G'.neighborSet ↑v)<GOAL>G'.coe.degree v = G'.degree ↑v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : ↑G'.verts<VAR>inst✝¹ : Fintype ↑(G'.coe.neighborSet v)<VAR>inst✝ : Fintype ↑(G'.neighborSet ↑v)<GOAL>Fintype.card ↑(G'.coe.neighborSet v) = G'.degree ↑v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹³ : CommRing R₁<VAR>inst✝¹² : AddCommGroup M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁷ : AddCommMonoid M'✝<VAR>inst✝⁶ : AddCommMonoid M''<VAR>inst✝⁵ : Module R M'✝<VAR>inst✝⁴ : Module R M''<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>B' : BilinForm R M'<VAR>f f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝¹ : AddCommGroup M₁'<VAR>inst✝ : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>h : B₁.IsAdjointPair B₁' f₁ g₁<VAR>h' : B₁.IsAdjointPair B₁' f₁' g₁'<VAR>x : M₁<VAR>y : M₁'<GOAL>(B₁' ((f₁ - f₁') x)) y = (B₁ x) ((g₁ - g₁') y)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>W X Y Z : Cᵒᵖ<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>p : CommSq f g h i<GOAL>i.unop ≫ g.unop = h.unop ≫ f.unop
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b✝ c : α<VAR>h : IsUnit c<VAR>a b : α<GOAL>a * c / (b * c) = a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f g : α → β<GOAL>(range fun x => if p x then f x else g x) ⊆ range f ∪ range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f g : α → β<GOAL>∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<GOAL>s ∪ r ⊆ s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<GOAL>MapsTo f (s ∪ r) t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<GOAL>InjOn f (s ∪ r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<VAR>y : β<VAR>hyt' : y ∈ t'<GOAL>y ∈ f '' (s ∪ r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t : Set β<VAR>f : α → β<VAR>t' : Set β<VAR>h : BijOn f s t<VAR>hss₁ : s ⊆ s₁<VAR>htt' : t ⊆ t'<VAR>ht' : SurjOn f s₁ t'<VAR>r : Set α<VAR>hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t<VAR>hbij : BijOn f r ((f '' s₁ ∩ t') \ t)<VAR>y : β<VAR>hyt' : y ∈ t'<GOAL>y ∈ t ∪ f '' s₁ ∩ t'
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : s(v, w) ∈ G.edgeSet<VAR>d : G.Dart := { toProd := (v, w), adj := h }<GOAL>(filter (fun d => d.edge = s(v, w)) univ).card = 2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : s(v, w) ∈ G.edgeSet<VAR>d : G.Dart := { toProd := (v, w), adj := h }<GOAL>2 = {d, d.symm}.card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : s(v, w) ∈ G.edgeSet<VAR>d : G.Dart := { toProd := (v, w), adj := h }<GOAL>d ∉ {d.symm}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : s(v, w) ∈ G.edgeSet<VAR>d : G.Dart := { toProd := (v, w), adj := h }<GOAL>¬d = d.symm
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂✝ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E✝ : Type u_4<VAR>Eₗ : Type u_5<VAR>F✝ : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0<GOAL>(∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hf : AEFinStronglyMeasurable f μ<VAR>hg : AEFinStronglyMeasurable g μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hf : AEFinStronglyMeasurable f μ<VAR>hg : AEFinStronglyMeasurable g μ<GOAL>f - g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hf : AEFinStronglyMeasurable f μ<VAR>hg : AEFinStronglyMeasurable g μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<GOAL>f - g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>hf : AEFinStronglyMeasurable f μ<VAR>hg : AEFinStronglyMeasurable g μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<VAR>hfg_int : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (f - g) s μ<GOAL>f - g =ᶠ[ae μ] 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ i : ι<VAR>x : β i<GOAL>erase i (single i x) = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : Pairwise (Disjoint on fun i => (M i).E)<VAR>B : Set α<GOAL>(Matroid.disjointSigma M h).Base B ↔ (∀ (i : ι), (M i).Base (B ∩ (M i).E)) ∧ B ⊆ ⋃ i, (M i).E
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B✝ A B : Matrix n n α<GOAL>(A * B)⁻¹ = B⁻¹ * A⁻¹
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B✝ A B : Matrix n n α<GOAL>Ring.inverse (A * B).det • (A * B).adjugate = Ring.inverse B.det • B.adjugate * Ring.inverse A.det • A.adjugate
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : Integrable g μ<VAR>v : E<GOAL>Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : Integrable g μ<VAR>v : E<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun a => n⁻¹ • (f (a + n • v) - f a) * g a) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : Integrable g μ<VAR>v : E<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ ↑C * ‖v‖ * ‖g a‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : Integrable g μ<VAR>v : E<GOAL>Integrable (fun x => ↑C * ‖v‖ * ‖g x‖) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>hg : Integrable g μ<VAR>v : E<GOAL>∀ᵐ (a : E) ∂μ, Tendsto (fun n => n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<GOAL>∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp (↑ε * z) • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε ∈ Iio 0<GOAL>‖cexp (↑ε * z) • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f {z | 0 < z.re}<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<GOAL>‖g z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<VAR>hd : DiffContOnCl ℂ g {z | 0 < z.re}<GOAL>‖g z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<VAR>hd : DiffContOnCl ℂ g {z | 0 < z.re}<VAR>hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖<GOAL>‖g z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<VAR>hd : DiffContOnCl ℂ g {z | 0 < z.re}<VAR>hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖<GOAL>∃ c < 2, ∃ B, g =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<VAR>hd : DiffContOnCl ℂ g {z | 0 < z.re}<VAR>hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖<GOAL>Tendsto (fun x => g ↑x) atTop (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => ‖f ↑x‖<VAR>him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C<VAR>hz : 0 ≤ z.re<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>g : ℂ → E := fun z => cexp (↑ε * z) • f z<VAR>hd : DiffContOnCl ℂ g {z | 0 < z.re}<VAR>hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖<VAR>y : ℝ<GOAL>‖g (↑y * I)‖ ≤ C
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>S₁ S₂ : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥S₂<VAR>hle : S₁ ≤ S₂<VAR>hd : finrank K ↥S₂ ≤ finrank K ↥S₁<GOAL>S₁ = S₂
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>S₁ S₂ : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥S₂<VAR>hle : S₁ ≤ S₂<VAR>hd : finrank K ↥S₂ ≤ finrank K ↥(comap S₂.subtype S₁)<GOAL>S₁ = S₂
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E →ₗ[ℝ] E<VAR>hf : LinearMap.det f ≠ 0<VAR>s : Set E<GOAL>(map (⇑f) μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s