ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<GOAL>eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<VAR>hμ : ¬μ = 0<VAR>hc : ¬c = 0<GOAL>eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<VAR>hμ : ¬μ = 0<VAR>hc : ¬c = 0<GOAL>↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<VAR>hμ : ¬μ = 0<VAR>hc : ¬c = 0<VAR>hμ_top : ¬μ Set.univ = ⊤<GOAL>↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal) < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<VAR>hμ : ¬μ = 0<VAR>hc : ¬c = 0<VAR>hμ_top : ¬μ Set.univ = ⊤<GOAL>↑‖c‖₊ < ⊤ ∧ μ Set.univ ^ (1 / p.toReal) < ⊤ ∨ ↑‖c‖₊ = 0 ∨ μ Set.univ ^ (1 / p.toReal) = 0 ↔ c = 0 ∨ μ Set.univ < ⊤
<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>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hp : 0 < p.toReal<VAR>hμ : ¬μ = 0<VAR>hc : ¬c = 0<VAR>hμ_top : ¬μ Set.univ = ⊤<GOAL>μ Set.univ ^ p.toReal⁻¹ < ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x ≤ g^[n] x ↔ f x ≤ g x
<VAR>α : Type u<VAR>l : List α<GOAL>l.enum.unzip = (range l.length, l)
<VAR>n m m' : ℕ<VAR>h : m ^^^ n = m' ^^^ n<GOAL>m = m'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>i : ℕ<VAR>w : i < l.length<VAR>h : optParam (0 < l.length) ⋯<GOAL>l[i] ≤ maximum_of_length_pos h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>i : ℕ<VAR>w : i < l.length<VAR>h : optParam (0 < l.length) ⋯<GOAL>l[i] ∈ l
<VAR>x✝ y✝ z x y : ℝ<GOAL>|x ^ y| ≤ |x| ^ y
<VAR>x✝ y✝ z x y : ℝ<VAR>hx : 0 ≤ x<GOAL>|x ^ y| ≤ |x| ^ y
<VAR>x✝ y✝ z x y : ℝ<VAR>hx : x < 0<GOAL>|x ^ y| ≤ |x| ^ y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Closeds α<GOAL>IsAtom s ↔ ∃ x, s = singleton x
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>h : ∞ ∈ s<GOAL>IsOpen s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen (some ⁻¹' s)
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : StronglyMeasurable f<GOAL>HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ (y : β), ‖f (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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : StronglyMeasurable f<GOAL>∫⁻ (x : α), ∫⁻ (y : β), ↑‖f (x, y)‖₊ ∂ν ∂μ < ⊤ ↔ (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ↑‖f (x, a)‖₊ ∂ν < ⊤) ∧ ∫⁻ (a : α), ↑‖∫ (y : β), ‖f (a, 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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : StronglyMeasurable f<VAR>this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖<GOAL>∫⁻ (x : α), ∫⁻ (y : β), ↑‖f (x, y)‖₊ ∂ν ∂μ < ⊤ ↔ (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ↑‖f (x, a)‖₊ ∂ν < ⊤) ∧ ∫⁻ (a : α), ↑‖∫ (y : β), ‖f (a, 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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : StronglyMeasurable f<VAR>this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖<GOAL>∫⁻ (x : α), ∫⁻ (y : β), ↑‖f (x, y)‖₊ ∂ν ∂μ < ⊤ ↔ (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ↑‖f (x, a)‖₊ ∂ν < ⊤) ∧ ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ↑‖f (a, a_1)‖₊ ∂ν).toReal ∂μ < ⊤
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : StronglyMeasurable f<VAR>this✝ : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖<VAR>this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))<GOAL>∫⁻ (x : α), ∫⁻ (y : β), ↑‖f (x, y)‖₊ ∂ν ∂μ < ⊤ ↔ (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ↑‖f (x, a)‖₊ ∂ν < ⊤) ∧ ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ↑‖f (a, a_1)‖₊ ∂ν).toReal ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a : α<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a b : α<VAR>h : inl b < inl a<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a : α<VAR>b : β<VAR>h : inr b < inl a<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a : β<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a : β<VAR>b : α<VAR>h : inl b < inr a<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : NoMinOrder (α ⊕ β)<VAR>a b : β<VAR>h : inr b < inr a<GOAL>∃ b, b < a
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F G : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>inst✝ : HasLimit G<VAR>c : Cone F<VAR>α : F ⟶ G<VAR>j✝ : J<GOAL>(lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F G : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>inst✝ : HasLimit G<VAR>c : Cone F<VAR>α : F ⟶ G<VAR>j✝ : J<GOAL>c.π.app j✝ ≫ α.app j✝ = ((Cones.postcompose α).obj c).π.app j✝
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : ¬Integrable I l f vol<GOAL>integral I l (-f) vol = -integral I l f vol
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>ι : Sort u_2<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>x : α<VAR>h : (𝓝 x).HasBasis p s<GOAL>(v.filterAt x).HasBasis p fun i => {t | t ∈ v.setsAt x ∧ t ⊆ s i}
<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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
<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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = P.fromLeftDerivedZero' F ≫ F.map (𝟙 X)<GOAL>(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
<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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = P.fromLeftDerivedZero' F ≫ F.map (𝟙 X)<VAR>h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv = (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))<GOAL>(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
<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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv = (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))<VAR>h₁ : HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = P.fromLeftDerivedZero' F<GOAL>(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
<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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv = (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))<VAR>h₁ : HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = P.fromLeftDerivedZero' F<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F = (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution X).complex).homologyι 0 ≫ (projectiveResolution X).fromLeftDerivedZero' F
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s t u v : Set α<GOAL>AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a✝ : Nontrivial M₀<GOAL>inverse 0 = 0
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε<GOAL>levyProkhorovEDist μ ν ≤ δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε<GOAL>∀ (ε : ℝ≥0), 0 < ε → δ < ⊤ → levyProkhorovEDist μ ν ≤ δ + ↑ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>a✝ : δ < ⊤<VAR>ε_top : ¬↑ε = ⊤<GOAL>levyProkhorovEDist μ ν ≤ δ + ↑ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>a✝ : δ < ⊤<VAR>ε_top : ¬↑ε = ⊤<GOAL>δ + ↑ε ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>δ : ℝ≥0∞<VAR>h : ∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>a✝ : δ < ⊤<VAR>ε_top : ¬↑ε = ⊤<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<GOAL>μ B ≤ ν (thickening (δ + ↑ε).toReal B) + (δ + ↑ε) ∧ ν B ≤ μ (thickening (δ + ↑ε).toReal B) + (δ + ↑ε)
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>2 * n = n + n
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>↑2 * -[n+1] = -[n+1] + -[n+1]
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>-↑n.succ + -↑n.succ = -[n+1] + -[n+1]
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>s : Multiset α<VAR>x y z : α<GOAL>(fun x x_1 => x * x_1) x ((fun x x_1 => x * x_1) y z) = (fun x x_1 => x * x_1) y ((fun x x_1 => x * x_1) x z)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s✝ s t : Set (Sym2 V)<VAR>h : s ⊆ t<VAR>v w : V<GOAL>(fromEdgeSet s).Adj v w → (fromEdgeSet t).Adj v w
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s✝ s t : Set (Sym2 V)<VAR>h : s ⊆ t<VAR>v w : V<GOAL>s(v, w) ∈ s → ¬v = w → s(v, w) ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>m : α → β<VAR>h : Injective m<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>m ⁻¹' (m '' s) ⊆ s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>U V : Opens M<VAR>h : U ≤ V<VAR>x : M<VAR>hx : x ∈ U<GOAL>ContMDiffAt I I n (inclusion h) ⟨x, hx⟩
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>U V : Opens M<VAR>h : U ≤ V<VAR>x : M<VAR>hx : x ∈ U<GOAL>∀ (y : H), ContDiffWithinAtProp I I n id univ y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>U V : Opens M<VAR>h : U ≤ V<VAR>x : M<VAR>hx : x ∈ U<VAR>y : H<GOAL>ContDiffWithinAtProp I I n id univ y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>U V : Opens M<VAR>h : U ≤ V<VAR>x : M<VAR>hx : x ∈ U<VAR>y : H<GOAL>ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (univ ∩ range ↑I) (↑I y)