ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.rightDerivedToHomotopyCategory α).app X) = ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫ HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫ HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) n ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv = (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (P.isoRightDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝³ : L.IsLocalization W<VAR>A : Type w<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : HasShift C A<VAR>inst✝ : W.IsCompatibleWithShift A<VAR>a : A<VAR>x✝¹ x✝ : C<VAR>f : x✝¹ ⟶ x✝<VAR>hf : W f<GOAL>W ((shiftFunctor C a).map f)
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.Nodup<VAR>i j : ℕ<GOAL>l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
<VAR>α : Type u<VAR>i j : ℕ<VAR>hl : [].Nodup<GOAL>[].rotate i = [].rotate j ↔ i % [].length = j % [].length ∨ [] = []
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.Nodup<VAR>i j : ℕ<VAR>hn : l ≠ []<GOAL>l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<GOAL>sSup S = conGen (sSup (DFunLike.coe '' S))
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<GOAL>(conGen fun x y => ∃ c ∈ S, c x y) = conGen (⨆ a ∈ S, ⇑a)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<VAR>x y : M<GOAL>(∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : Ring α<VAR>inst✝³ : AddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>-s • t = -(s • t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : Ring α<VAR>inst✝³ : AddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>image (fun x => -x) s • t = image (fun x => -x) (s • t)
<VAR>C : Type u₁<VAR>inst✝¹³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₂, u₂} D<VAR>K : GrothendieckTopology D<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>A : Type u₃<VAR>inst✝¹¹ : Category.{v₃, u₃} A<VAR>inst✝¹⁰ : EssentiallySmall.{w, v₁, u₁} C<VAR>B : Type u_1<VAR>inst✝⁹ : Category.{?u.115187, u_1} B<VAR>F : A ⥤ B<VAR>inst✝⁸ : HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A<VAR>inst✝⁷ : ((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F<VAR>inst✝⁶ : G.IsCoverDense J<VAR>inst✝⁵ : G.IsContinuous K J<VAR>inst✝⁴ : G.Full<VAR>inst✝³ : (G.sheafPushforwardContinuous A K J).EssSurj<VAR>inst✝² : G.IsCocontinuous K J<VAR>hG : CoverPreserving K J G<VAR>inst✝¹ : ConcreteCategory A<VAR>inst✝ : K.WEqualsLocallyBijective A<VAR>X✝ Y✝ : Cᵒᵖ ⥤ A<VAR>f : X✝ ⟶ Y✝<GOAL>J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).length = (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m✝ n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n m : ℕ<VAR>x✝¹ : m < ((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).length<VAR>x✝ : m < (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).length<GOAL>((List.map (fun n => f^[n] x) (List.range (minimalPeriod f x))).rotate n).get ⟨m, x✝¹⟩ = (List.map (fun n_1 => f^[n_1] (f^[n] x)) (List.range (minimalPeriod f (f^[n] x)))).get ⟨m, x✝⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>span 𝕜 (Set.range (gramSchmidtNormed 𝕜 f)) = span 𝕜 (Set.range (gramSchmidt 𝕜 f))
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁹ : Semiring R✝<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>P : Type u_3<VAR>inst✝⁶ : AddCommMonoid P<VAR>inst✝⁵ : Module R✝ P<VAR>f : M✝ →ₗ[R✝] P<VAR>R : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>I : Submodule R N<VAR>x : ↥I ⊗[R] M<GOAL>∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (rTensor M (inclusion hle)) y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<VAR>ht : t ∈ measurableCylinders α<GOAL>s ∩ t ∈ measurableCylinders α
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : ∃ s_1 S, MeasurableSet S ∧ s = cylinder s_1 S<VAR>ht : ∃ s S, MeasurableSet S ∧ t = cylinder s S<GOAL>∃ s_1 S, MeasurableSet S ∧ s ∩ t = cylinder s_1 S
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set (Completion α × Completion α)<GOAL>s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set (Completion α × Completion α)<GOAL>s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.1 p.2 < ↑i}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set (Completion α × Completion α)<GOAL>Directed (fun x x_1 => x ≥ x_1) fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<VAR>n : ℕ<GOAL>(X ^ n * p).reverse = p.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>t u : Set α<GOAL>u ∈ l ⊔ 𝓟 t ↔ ∃ i, p i ∧ s i ∪ t ⊆ u
<VAR>α : Type u_1<VAR>a : Array α<VAR>n : Nat<GOAL>(a.shrink n).size = min a.size n
<VAR>α : Type u_1<VAR>a : Array α<VAR>n : Nat<GOAL>a.size - (a.size - n) = min a.size n
<VAR>m n✝ a✝ b✝ c d b a n : ℕ<VAR>h : a * b ≡ 1 [MOD n]<GOAL>a.Coprime n
<VAR>m n✝ a✝ b✝ c d b a n : ℕ<VAR>h : a * b ≡ 1 [MOD n]<VAR>g : ℕ<VAR>hh : n = a.gcd n * g<GOAL>a.Coprime n
<VAR>m n✝ a✝ b✝ c d b a n : ℕ<VAR>h : a * b ≡ 1 [MOD n]<VAR>g : ℕ<VAR>hh : n = a.gcd n * g<GOAL>1 ≡ 0 [MOD a.gcd n]
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>inst✝ : CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x<VAR>hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x<VAR>hu' : IntervalIntegrable u' volume a b<VAR>hv' : IntervalIntegrable v' volume a b<GOAL>∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>i✝ x✝ : m<GOAL>(toLinearMapRight' 1 ∘ₗ single i✝) 1 x✝ = (LinearMap.id ∘ₗ single i✝) 1 x✝
<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 : E →ₗ.[R] F<VAR>S : Submodule R E<VAR>x : ↥(S ⊓ f.domain)<VAR>y : ↥f.domain<VAR>h : ↑x = ↑y<VAR>this : (Submodule.inclusion ⋯) x = y<GOAL>↑(f.domRestrict S) x = ↑f ((Submodule.inclusion ⋯) x)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>v : ι → M<VAR>hv : LinearIndependent R v<VAR>w : ι → Rˣ<GOAL>LinearIndependent R (w • v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → Rˣ<GOAL>∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → Rˣ<VAR>s : Finset ι<VAR>g : ι → R<VAR>hgs : ∀ i ∉ s, g i = 0<VAR>hsum : ∑ i ∈ s, g i • (w • v) i = 0<VAR>i : ι<GOAL>g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → Rˣ<VAR>s : Finset ι<VAR>g : ι → R<VAR>hgs : ∀ i ∉ s, g i = 0<VAR>hsum : ∑ i ∈ s, g i • (w • v) i = 0<VAR>i : ι<GOAL>g i * ↑(w i) = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(∫⁻ (x : β), ↑‖g x‖₊ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ↑‖(g ∘ f) x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>hp_zero : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(∫⁻ (a : α), ↑‖g (f a)‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ↑‖(g ∘ f) x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>B : Matrix m p R<GOAL>A * Aᴴ * B = 0 ↔ Aᴴ * B = 0
<VAR>n : ℕ<VAR>c : Composition n<GOAL>c.boundary (Fin.last c.length) = Fin.last n
<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✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.SSameSide x y}
<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✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : ↑s = ∅<GOAL>IsPreconnected {y | s.SSameSide x y}
<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✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsPreconnected {y | s.SSameSide x y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<GOAL>UniformContinuousOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<GOAL>∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)<GOAL>∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<VAR>ε : ℝ≥0∞<VAR>εpos : ε > 0<VAR>this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)<VAR>δ : ℝ≥0∞<VAR>δ0 : 0 < δ<VAR>H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}<GOAL>∃ δ > 0, ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>hf : SuperpolynomialDecay l k f<VAR>z : ℤ<GOAL>SuperpolynomialDecay l k fun a => k a ^ z * f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)<VAR>z : ℤ<GOAL>∀ (z_1 : ℤ), Tendsto (fun a => k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)<VAR>z z' : ℤ<VAR>x : α<VAR>hx : k x ≠ 0<GOAL>k x ^ (z' + z) * f x = (fun a => k a ^ z' * (k a ^ z * f a)) x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>hx : f x ∈ Submodule.span R ↑s<VAR>y : ↥S := commonDenomOfFinset S f s<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>hx : f x ∈ Submodule.span R ↑s<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>hx : f x ∈ Submodule.span R ↑s<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : Submodule.span R (↑y • ↑s) = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>hx : f x ∈ Submodule.span R ↑s<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>hx : S.subtype y • f x ∈ y • Submodule.span R ↑s<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>hx : f (S.subtype y • x) ∈ Submodule.map f (Submodule.span R ↑(finsetIntegerMultiple S f s))<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<VAR>a : ↥S<VAR>ha : a • x' = a • S.subtype y • x<GOAL>∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)