ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<GOAL>dimH (f ⁻¹' s) ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f ⁻¹' s) = ⊤<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f ⁻¹' s) = ⊤<VAR>this : μH[↑d] (f ⁻¹' s) ≤ ↑K ^ ↑d * μH[↑d] s<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f ⁻¹' s) = ⊤<VAR>this : ↑K ^ ↑d * μH[↑d] s = ⊤<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>hf : AntilipschitzWith K f<VAR>s : Set Y<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f ⁻¹' s) = ⊤<VAR>this : μH[↑d] s ≠ ⊤<GOAL>↑K ^ ↑d * μH[↑d] s ≠ ⊤
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>T : Triangle (CochainComplex C ℤ)<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(homologyFunctor C (up ℤ) 0).homologySequenceδ ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h = (homologyFunctorFactors C (up ℤ) n₀).hom.app T.obj₃ ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app T.obj₁
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)
<VAR>α : Type u<VAR>inst✝¹ : LinearOrderedCommGroup α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<GOAL>∃ a, 1 < a
<VAR>α : Type u<VAR>inst✝¹ : LinearOrderedCommGroup α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<VAR>y : α<VAR>hy : y ≠ 1<GOAL>∃ a, 1 < a
<VAR>α : Type u<VAR>inst✝¹ : LinearOrderedCommGroup α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<VAR>y : α<VAR>hy : y ≠ 1<VAR>h : y < 1<GOAL>∃ a, 1 < a
<VAR>α : Type u<VAR>inst✝¹ : LinearOrderedCommGroup α<VAR>a b c : α<VAR>inst✝ : Nontrivial α<VAR>y : α<VAR>hy : y ≠ 1<VAR>h : 1 < y<GOAL>∃ a, 1 < a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>x⋆ * x = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>‖x‖ * ‖x‖ = 0 ↔ x = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>i : σ<VAR>h : Finsupp.single i 1 = 0<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ convexBodySum K B<GOAL>-x ∈ convexBodySum K B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ convexBodySum K B<GOAL>convexBodySumFun x ≤ B
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E ≃ₐ[F] K<GOAL>finInsepDegree F E = finInsepDegree F K
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r : X<VAR>s : ↥S<VAR>r' : X<VAR>s' : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s = ra * ↑s'<VAR>ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)<GOAL>r /ₒ s + r' /ₒ s' = r' /ₒ s' + r /ₒ s
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r : X<VAR>s : ↥S<VAR>r' : X<VAR>s' : ↥S<VAR>ra : R<VAR>sa : ↥S<VAR>ha : ↑sa * ↑s = ra * ↑s'<VAR>ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)<GOAL>(ra • r' + sa • r) /ₒ (sa * s) = (ra • r' + ↑sa • r) /ₒ ⟨ra * ↑s', ⋯⟩
<VAR>ι : Type u<VAR>s✝ s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0<VAR>hp : 1 < p<GOAL>∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>ι : Type u<VAR>s✝ s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0<VAR>hp : 1 < p<GOAL>∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)
<VAR>ι : Type u<VAR>s✝ s : Finset ι<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>w f : ι → ℝ≥0<VAR>hp : 1 < p<GOAL>(∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) = (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>(hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<VAR>j : Discrete WalkingPair<GOAL>(inl ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j = (inl ≫ desc b.inl b.inr) ≫ b.toCone.π.app j
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<VAR>j : Discrete WalkingPair<GOAL>(inr ≫ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv) ≫ b.toCone.π.app j = (inr ≫ desc b.inl b.inr) ≫ b.toCone.π.app j
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } = inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } = inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } = inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>b : BinaryBicone X Y<VAR>hb : b.IsBilimit<GOAL>inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } = inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w : ReducedWord G A B<VAR>g : G<VAR>hg : of g = ReducedWord.prod φ w<GOAL>w.toList = []
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w : ReducedWord G A B<VAR>g : G<VAR>hg : of g = ReducedWord.prod φ w<VAR>w' : ReducedWord G A B := let __src := ReducedWord.empty G A B; { head := g, toList := __src.toList, chain := ⋯ }<GOAL>w.toList = []
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>w : ReducedWord G A B<VAR>g : G<VAR>hg : of g = ReducedWord.prod φ w<VAR>w' : ReducedWord G A B := let __src := ReducedWord.empty G A B; { head := g, toList := __src.toList, chain := ⋯ }<VAR>this : ReducedWord.prod φ w = ReducedWord.prod φ w'<GOAL>w.toList = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>f : ι → ι'<VAR>hf : Injective f<VAR>m : ι → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum (Function.extend f m 0)) s = (sum m) s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<GOAL>b.sumCoords (b i) = 1
<VAR>n m l : ℕ<GOAL>∀ (a : ℕ), a ∉ Ico n m ∩ Ico m l
<VAR>n m l a : ℕ<GOAL>a ∉ Ico n m ∩ Ico m l
<VAR>n m l a : ℕ<GOAL>n ≤ a → a < m → m ≤ a → l ≤ a
<VAR>n m l a : ℕ<VAR>a✝ : n ≤ a<VAR>h₂ : a < m<VAR>h₃ : m ≤ a<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>map f (think ⟨s, al⟩) = (map f ⟨s, al⟩).think
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>↑(map f (think ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).think
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) (Stream'.cons none s) = Stream'.cons none (Stream'.map (fun o => Option.rec none (fun val => some (f val)) o) s)
<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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᶠ[ae (μ.restrict t)] 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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f ≤ᶠ[ae (μ.restrict t)] 0 ∧ 0 ≤ᶠ[ae (μ.restrict t)] f
<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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f ≤ᶠ[ae (μ.restrict t)] 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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>0 ≤ᶠ[ae (μ.restrict t)] -f
<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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>0 ≤ ∫ (x : α) in s, (-f) x ∂μ
<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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>0 ≤ ∫ (x : α) in s, -f x ∂μ
<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✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>∫ (a : α) in s, f a ∂μ ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>t : NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>⇑(toSpec 𝒜 f).val.base ⁻¹' ↑(sbo HomogeneousLocalization.mk t) = ↑((Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (pbo ↑t.num))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>t : NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>⇑(toSpec 𝒜 f).val.base = ProjIsoSpecTopComponent.ToSpec.toFun f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<GOAL>(Computable₂ fun a n => Option.map (f a) (decode n)) ↔ Computable₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<VAR>x✝¹ : α<VAR>x✝ : ℕ<GOAL>Option.map (f x✝¹) (decode x✝) = (decode x✝).bind (Option.some ∘ f x✝¹)
<VAR>x y✝ z✝ : ZFSet<VAR>H : ∀ y ∈ x, y.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<VAR>z : ZFSet<VAR>hz : z ∈ y<GOAL>z ∈ ⋃₀ x
<VAR>x y✝ z✝ : ZFSet<VAR>H : ∀ y ∈ x, y.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<VAR>z : ZFSet<VAR>hz : z ∈ y<VAR>w : ZFSet<VAR>hw : w ∈ x<VAR>hw' : y ∈ w<GOAL>z ∈ ⋃₀ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set α<GOAL>∃ a, f ⁻¹' a = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set α<GOAL>f ⁻¹' (f '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<VAR>h : m ≤ n<GOAL>a ^ m * a ^ (n - m) = a ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x‖) (Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>Integrable (fun x => ‖∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x‖) (Measure.map (fun a => (X a, Y a)) μ).fst
<VAR>x✝ y✝ x y : ℝ<VAR>h : x < y<GOAL>rexp x < rexp y
<VAR>x✝ y✝ x y : ℝ<VAR>h : x < y<GOAL>rexp x < rexp (y - x) * rexp x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsAntisymm α r<VAR>hs : Chain r s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsAntisymm α r<VAR>hs : ∀ a ∈ s, ∀ b ∈ s, r a b<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a = b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : DecidableEq β<VAR>i : β → γ<VAR>j : γ → β<VAR>h : Function.LeftInverse j i<VAR>a : β<GOAL>a ∈ Finset.image j {i a}
<VAR>α : Type u<VAR>l : List ℕ<VAR>n : ℕ<GOAL>(∃ s ∈ l.ranges, n ∈ s) ↔ n < Nat.sum l
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : InfSet α<VAR>inst✝¹ : InfSet β<VAR>inst✝ : sInfHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Φ 1 = X
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε✝ δ : 𝕜<VAR>u✝ v✝ u v : Finset α<VAR>ε : 𝕜<GOAL>(u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ⊔ b ⊔ c = c ⊔ b ⊔ a
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M✝ N✝ P Q : Submodule R A<VAR>m n : A<VAR>M N : Submodule R A<GOAL>(map₂ (LinearMap.mul R A) M N).toAddSubmonoid = ⨆ s, AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M✝ N✝ P Q : Submodule R A<VAR>m n : A<VAR>M N : Submodule R A<GOAL>⨆ i, (map ((LinearMap.mul R A) ↑i) N).toAddSubmonoid = ⨆ s, AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>Tendsto (fun x => b ^ x) atBot atTop
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>Tendsto (fun x => rexp (log b * x)) atBot atTop
<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b < 1<GOAL>log b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : InjOn f s<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard ≤ t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : InjOn f s<VAR>ht : autoParam t.Finite _auto✝<VAR>hle : s.encard ≤ t.encard<GOAL>s.ncard ≤ t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>f✝ : α → β<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : InjOn f s<VAR>ht : autoParam t.Finite _auto✝<VAR>hle : s.encard ≤ t.encard<GOAL>↑s.ncard ≤ ↑t.ncard
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : Arrow.mk φ ≅ Arrow.mk φ'<VAR>inst✝³ : ∀ (i : ι), K.HasHomology i<VAR>inst✝² : ∀ (i : ι), L.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), K'.HasHomology i<VAR>inst✝ : ∀ (i : ι), L'.HasHomology i<GOAL>QuasiIso φ ↔ QuasiIso φ'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : Arrow.mk φ ≅ Arrow.mk φ'<VAR>inst✝³ : ∀ (i : ι), K.HasHomology i<VAR>inst✝² : ∀ (i : ι), L.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), K'.HasHomology i<VAR>inst✝ : ∀ (i : ι), L'.HasHomology i<GOAL>QuasiIso ((let_fun this := e.inv.left; this) ≫ φ) ↔ QuasiIso (φ' ≫ let_fun this := e.inv.right; this)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : K' ⟶ L'<VAR>e : Arrow.mk φ ≅ Arrow.mk φ'<VAR>inst✝³ : ∀ (i : ι), K.HasHomology i<VAR>inst✝² : ∀ (i : ι), L.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), K'.HasHomology i<VAR>inst✝ : ∀ (i : ι), L'.HasHomology i<GOAL>QuasiIso ((Arrow.mk φ').hom ≫ e.inv.right) ↔ QuasiIso (φ' ≫ let_fun this := e.inv.right; this)
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>term (f ⍟ g) s 0 = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>term (f ⍟ g) s n = ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : MeasurableSub₂ E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasurableSet {x | f x = g x}
<VAR>α✝ : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : Div G<VAR>m✝ : MeasurableSpace α<VAR>f✝ g✝ : α → G<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>E : Type u_4<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : AddGroup E<VAR>inst✝¹ : MeasurableSingletonClass E<VAR>inst✝ : MeasurableSub₂ E<VAR>f g : α → E<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>{x | f x = g x} = {x | (f - g) x = 0}