ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<VAR>f2 : X →ᵇ ℝ≥0<VAR>f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2<VAR>f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<VAR>f2 : X →ᵇ ℝ≥0<VAR>f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2<VAR>f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x<GOAL>Λ (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<VAR>f2 : X →ᵇ ℝ≥0<VAR>f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2<VAR>f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x<GOAL>Λ f1 + Λ f2 < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<VAR>f2 : X →ᵇ ℝ≥0<VAR>f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2<VAR>f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x<GOAL>rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<GOAL>K ⊔ Kᗮ = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<GOAL>Kᗮ = Kᗮ ⊓ ⊤
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>i : ι<GOAL>(e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>i : ι<GOAL>(-1 * ∏ x ∈ Finset.univ \ {i}, 1 x)⁻¹ • e.orientation = -e.orientation
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (x * z + y)<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsCoprime x (y + x * z)<GOAL>IsCoprime x y
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaOdd a s = (hurwitzZeta a s - hurwitzZeta (-a) s) / 2
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑r = 1 ↔ r = 1
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C).card * B.card ≤ (A / B).card * (B * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C⁻¹).card * B.card ≤ (A / B).card * (B / C⁻¹).card
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>choose (r + s) k = ∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>(fun x => k.factorial • x) (choose (r + s) k) = (fun x => k.factorial • x) (∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>k.factorial • choose (r + s) k = k.factorial • ∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) = ∑ x ∈ antidiagonal k, k.factorial • (choose r x.1 * choose s x.2)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<GOAL>∀ x ∈ antidiagonal k, ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) = k.factorial • (choose r x.1 * choose s x.2)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<VAR>x : ℕ × ℕ<VAR>hx : x ∈ antidiagonal k<GOAL>↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) = k.factorial • (choose r x.1 * choose s x.2)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : BinomialRing R<VAR>r s : R<VAR>k : ℕ<VAR>h : Commute r s<VAR>x : ℕ × ℕ<VAR>hx : x ∈ antidiagonal k<GOAL>↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) = ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : P<VAR>direction : Submodule k V<VAR>v : V<GOAL>v ∈ (mk' p direction).direction ↔ v ∈ direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : P<VAR>direction : Submodule k V<VAR>v : V<GOAL>(∃ p1 ∈ mk' p direction, ∃ p2 ∈ mk' p direction, v = p1 -ᵥ p2) ↔ v ∈ direction
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>R' : Set α<VAR>M : Matroid α<VAR>h : R ⊆ R'<GOAL>M ↾ R ≤r M ↾ R'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>R' : Set α<VAR>M : Matroid α<VAR>h : R ⊆ R'<GOAL>M ↾ R' ↾ R ≤r M ↾ R'
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>HasStrictFDerivAt (implicitFunctionOfComplemented f f' hf hf' hker (f a)) (LinearMap.ker f').subtypeL 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>0 = (implicitFunctionDataOfComplemented f f' hf hf' hker).rightFun (implicitFunctionDataOfComplemented f f' hf hf' hker).pt
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>(implicitFunctionDataOfComplemented f f' hf hf' hker).rightDeriv.comp (LinearMap.ker f').subtypeL = ContinuousLinearMap.id 𝕜 ↥(LinearMap.ker f')
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<GOAL>(implicitFunctionDataOfComplemented f f' hf hf' hker).leftDeriv.comp (LinearMap.ker f').subtypeL = 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>(match p x with | true => x :: takeWhile p l.reverse | false => []).reverse = if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>H : D ⥤ E<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)<GOAL>HEq ((F ⋙ H).map f) ((G ⋙ H).map f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<GOAL>(algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<VAR>hx : IsIntegral K x<GOAL>(algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (gen K x)) = ((minpoly K x).aroots F).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : CommRing S<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝³ : Fintype ι<VAR>F : Type u_6<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K F<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<VAR>hx : IsIntegral K x<GOAL>Splits (algebraMap K F) (minpoly K x)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y : Set α<VAR>hX : M.Dep X<VAR>R : Set α<VAR>hXE : autoParam (X ⊆ (M ↾ R).E) _auto✝<GOAL>(M ↾ R).Dep X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y : ℝ≥0∞<VAR>h : ∀ a < 1, a * x ≤ y<VAR>this : Tendsto (fun x_1 => x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))<GOAL>x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y : ℝ≥0∞<VAR>h : ∀ a < 1, a * x ≤ y<VAR>this : Tendsto (fun x_1 => x_1 * x) (𝓝[<] 1) (𝓝 x)<GOAL>x ≤ y
<VAR>α : Type u<VAR>l : List α<VAR>n k : ℕ<VAR>h : k < (l.rotate n).length<GOAL>(l.rotate n)[k] = l[(k + n) % l.length]
<VAR>α : Type u<VAR>l : List α<VAR>n k : ℕ<VAR>h : k < (l.rotate n).length<GOAL>k < l.length
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullback f g).OpenCover
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>∀ (i : 𝒰X.J × 𝒰Y.J), pullback.map (𝒰X.map i.1 ≫ f) (𝒰Y.map i.2 ≫ g) f g (𝒰X.map i.1) (𝒰Y.map i.2) (𝟙 Z) ⋯ ⋯ = (Iso.refl ((fun ij => pullback (𝒰X.map ij.1 ≫ f) (𝒰Y.map ij.2 ≫ g)) i)).hom ≫ ((openCoverOfLeft 𝒰X f g).bind fun x => openCoverOfRight 𝒰Y (𝒰X.map x ≫ f) g).map ((Equiv.sigmaEquivProd 𝒰X.J 𝒰Y.J).symm i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f✝ : X ⟶ Z<VAR>g✝ : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f✝) g✝<VAR>s : PullbackCone f✝ g✝<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰X.J<VAR>j : 𝒰Y.J<GOAL>pullback.map (𝒰X.map (i, j).1 ≫ f) (𝒰Y.map (i, j).2 ≫ g) f g (𝒰X.map (i, j).1) (𝒰Y.map (i, j).2) (𝟙 Z) ⋯ ⋯ = (Iso.refl ((fun ij => pullback (𝒰X.map ij.1 ≫ f) (𝒰Y.map ij.2 ≫ g)) (i, j))).hom ≫ ((openCoverOfLeft 𝒰X f g).bind fun x => openCoverOfRight 𝒰Y (𝒰X.map x ≫ f) g).map ((Equiv.sigmaEquivProd 𝒰X.J 𝒰Y.J).symm (i, j))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<GOAL>IsZero Y ↔ f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsSplitEpi f<GOAL>𝟙 Y = 0 ↔ f = 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>s : R<GOAL>(xgcd 0 s).1 = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.41001, u_1} C<VAR>inst✝⁶ : Category.{?u.41005, u_2} D<VAR>inst✝⁵ : Category.{?u.41009, u_3} E<VAR>inst✝⁴ : Category.{?u.41013, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>iso : (a : A) → F.functor a ≅ G.functor a<VAR>comm : ∀ (n a a' : A) (ha' : n + a = a'), (F.shiftIso n a a' ha').hom ≫ (iso a).hom = whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom<VAR>n a a' : A<VAR>ha' : n + a = a'<GOAL>(G.shiftIso n a a' ha').hom ≫ (iso a).inv = whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<GOAL>∀ (a_1 : α) (s : Multiset α), (s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a) → ((a_1 ::ₘ s).lcm ∣ a ↔ ∀ b ∈ a_1 ::ₘ s, b ∣ a)
<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>μ : Measure α<VAR>ν : Measure β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : generateFrom C = inst✝⁶<VAR>hD : generateFrom D = inst✝⁴<VAR>h2C : IsPiSystem C<VAR>h2D : IsPiSystem D<VAR>h3C : μ.FiniteSpanningSetsIn C<VAR>h3D : ν.FiniteSpanningSetsIn D<VAR>μν : Measure (α × β)<VAR>h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t<GOAL>μ.prod ν = μν
<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>μ : Measure α<VAR>ν : Measure β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : generateFrom C = inst✝⁶<VAR>hD : generateFrom D = inst✝⁴<VAR>h2C : IsPiSystem C<VAR>h2D : IsPiSystem D<VAR>h3C : μ.FiniteSpanningSetsIn C<VAR>h3D : ν.FiniteSpanningSetsIn D<VAR>μν : Measure (α × β)<VAR>h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t<GOAL>∀ s ∈ image2 (fun x x_1 => x ×ˢ x_1) C D, (μ.prod ν) s = μν 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>μ : Measure α<VAR>ν : Measure β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : generateFrom C = inst✝⁶<VAR>hD : generateFrom D = inst✝⁴<VAR>h2C : IsPiSystem C<VAR>h2D : IsPiSystem D<VAR>h3C : μ.FiniteSpanningSetsIn C<VAR>h3D : ν.FiniteSpanningSetsIn D<VAR>μν : Measure (α × β)<VAR>h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t<VAR>s : Set α<VAR>hs : s ∈ C<VAR>t : Set β<VAR>ht : t ∈ D<GOAL>(μ.prod ν) ((fun x x_1 => x ×ˢ x_1) s t) = μν ((fun x x_1 => x ×ˢ x_1) s t)
<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>μ : Measure α<VAR>ν : Measure β<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : generateFrom C = inst✝⁶<VAR>hD : generateFrom D = inst✝⁴<VAR>h2C : IsPiSystem C<VAR>h2D : IsPiSystem D<VAR>h3C : μ.FiniteSpanningSetsIn C<VAR>h3D : ν.FiniteSpanningSetsIn D<VAR>μν : Measure (α × β)<VAR>h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t<VAR>s : Set α<VAR>hs : s ∈ C<VAR>t : Set β<VAR>ht : t ∈ D<VAR>this : SigmaFinite ν<GOAL>(μ.prod ν) ((fun x x_1 => x ×ˢ x_1) s t) = μν ((fun x x_1 => x ×ˢ x_1) s t)
<VAR>α : Type u<VAR>n : α → Filter α<VAR>ι : α → Sort u_1<VAR>p : (a : α) → ι a → Prop<VAR>s : (a : α) → ι a → Set α<VAR>hb : ∀ (a : α), (n a).HasBasis (p a) (s a)<VAR>hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i<VAR>hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x<VAR>a : α<VAR>t : TopologicalSpace α := TopologicalSpace.mkOfNhds n<GOAL>𝓝 a = n a
<VAR>α : Type u<VAR>n : α → Filter α<VAR>ι : α → Sort u_1<VAR>p : (a : α) → ι a → Prop<VAR>s : (a : α) → ι a → Set α<VAR>hb : ∀ (a : α), (n a).HasBasis (p a) (s a)<VAR>hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i<VAR>hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x<VAR>a : α<VAR>t : TopologicalSpace α := TopologicalSpace.mkOfNhds n<GOAL>𝓝 a ≤ n a
<VAR>α : Type u<VAR>n : α → Filter α<VAR>ι : α → Sort u_1<VAR>p : (a : α) → ι a → Prop<VAR>s : (a : α) → ι a → Set α<VAR>hb : ∀ (a : α), (n a).HasBasis (p a) (s a)<VAR>hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i<VAR>hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x<VAR>a : α<VAR>t : TopologicalSpace α := TopologicalSpace.mkOfNhds n<GOAL>n a ≤ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<VAR>this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) = (Finset.filter (fun x => x.1 = a) s).prod f<GOAL>∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<VAR>this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) = (Finset.filter (fun x => x.1 = a) s).prod f<GOAL>∏ i ∈ s, f i = ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s)), f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<VAR>this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) = (Finset.filter (fun x => x.1 = a) s).prod f<GOAL>∏ i ∈ s, f i = ∏ᶠ (a : α), (Finset.filter (fun ab => ab.1 = a) s).prod f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<VAR>this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) = (Finset.filter (fun x => x.1 = a) s).prod f<GOAL>∀ i ∈ s, i.1 ∈ Finset.image Prod.fst s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset (α × β)<VAR>f : α × β → M<VAR>this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd (Finset.filter (fun ab => ab.1 = a) s), f (a, i) = (Finset.filter (fun x => x.1 = a) s).prod f<GOAL>∀ i ∈ s, ∃ a ∈ s, a.1 = i.1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.2224, u_1} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>⊤ f
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>A : Type u₃<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>g : UniversalEnvelopingAlgebra R L →ₐ[R] A<GOAL>⇑g ∘ ⇑(ι R) = ⇑f ↔ g = (lift R) f
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>A : Type u₃<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>g : UniversalEnvelopingAlgebra R L →ₐ[R] A<GOAL>⇑g ∘ ⇑(ι R) = ⇑f ↔ (lift R).symm g = f
<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>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁✝ π₂✝ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>π₁ π₂ : Prepartition I<VAR>hU : π₁.iUnion = π₂.iUnion<GOAL>∑ J ∈ π₁.boxes, integral J l f vol = ∑ J ∈ π₂.boxes, integral J l f vol