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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>g : P.complex ⟶ Q.complex<VAR>w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f<GOAL>(F.leftDerived n).map f = (P.isoLeftDerivedObj F n).hom ≫ (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map g ≫ (Q.isoLeftDerivedObj F n).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✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>g : P.complex ⟶ Q.complex<VAR>w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f<GOAL>g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : s₂ ⊆ s₁<GOAL>d.Has (s₁ \ s₂)
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : s₂ ⊆ s₁<GOAL>d.Has (s₁ \ s₂)ᶜ
<VAR>α : Type u_1<VAR>d : DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : s₂ ⊆ s₁<GOAL>d.Has (s₁ᶜ ∪ s₂)
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>inst✝ : HasCountableSeparatingOn α p t<GOAL>∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>inst✝ : HasCountableSeparatingOn α p t<VAR>S : Set (Set α)<VAR>hSne : S.Nonempty<VAR>hSc : S.Countable<VAR>hS : (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>inst✝ : HasCountableSeparatingOn α p t<VAR>S : ℕ → Set α<VAR>hSne : (range S).Nonempty<VAR>hSc : (range S).Countable<VAR>hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y<GOAL>∃ S, (∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
<VAR>α : Type u_1<VAR>p : Set α → Prop<VAR>s₀ : Set α<VAR>hp : p s₀<VAR>t : Set α<VAR>inst✝ : HasCountableSeparatingOn α p t<VAR>S : ℕ → Set α<VAR>hSne : (range S).Nonempty<VAR>hSc : (range S).Countable<VAR>hS : (∀ s ∈ range S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ range S, x ∈ s ↔ y ∈ s) → x = y<GOAL>(∀ (n : ℕ), p (S n)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (n : ℕ), x ∈ S n ↔ y ∈ S n) → x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Monoid α<VAR>inst✝ : ContinuousMul α<VAR>x : α<VAR>l : List α<VAR>ih : Tendsto prod (𝓝 l) (𝓝 l.prod)<GOAL>Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Monoid α<VAR>inst✝ : ContinuousMul α<VAR>x : α<VAR>l : List α<VAR>ih : Tendsto prod (𝓝 l) (𝓝 l.prod)<GOAL>Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Monoid α<VAR>inst✝ : ContinuousMul α<VAR>x : α<VAR>l : List α<VAR>ih : Tendsto prod (𝓝 l) (𝓝 l.prod)<VAR>this : ContinuousAt (fun p => p.1 * p.2) (x, l.prod)<GOAL>Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Monoid α<VAR>inst✝ : ContinuousMul α<VAR>x : α<VAR>l : List α<VAR>ih : Tendsto prod (𝓝 l) (𝓝 l.prod)<VAR>this : Tendsto (fun p => p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))<GOAL>Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))
<VAR>x y : EReal<GOAL>sign (x * y) = sign x * sign y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N✝ N₂ : LieSubmodule R L M<VAR>N' : LieSubmodule R L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M'<VAR>m✝ : M'<GOAL>m✝ ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m✝ ∈ N
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>wittSub p 0 = X (0, 0) - X (1, 0)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(map (Int.castRingHom ℚ)) (wittSub p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))
<VAR>α : Type u_1<VAR>f : Bool → α<GOAL>range f = {f false, f true}
<VAR>y : EReal<GOAL>∃ a, a.log = y
<VAR>y : EReal<VAR>y_bot : y = ⊥<GOAL>∃ a, a.log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<GOAL>∃ a, a.log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<VAR>y_top : y = ⊤<GOAL>∃ a, a.log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<VAR>y_ntop : y < ⊤<GOAL>∃ a, a.log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<VAR>y_ntop : y < ⊤<GOAL>(ENNReal.ofReal (Real.exp y.toReal)).log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<VAR>y_ntop : y < ⊤<VAR>exp_y_pos : ¬Real.exp y.toReal ≤ 0<GOAL>(ENNReal.ofReal (Real.exp y.toReal)).log = y
<VAR>y : EReal<VAR>y_nbot : ⊥ < y<VAR>y_ntop : y < ⊤<VAR>exp_y_pos : ¬Real.exp y.toReal ≤ 0<GOAL>↑y.toReal = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>h : e.source ⊆ s<GOAL>(e.restr s).source = e.source
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n { byteIdx := utf8Len [] } = { byteIdx := utf8Len [] + utf8Len (List.take n m) }<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r { str := s.str, startPos := s.startPos + { byteIdx := utf8Len (List.take n m) }, stopPos := s.stopPos }
<VAR>l m r : List Char<VAR>s : Substring<VAR>h : ValidFor l m r s<VAR>n : Nat<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) }, stopPos := { byteIdx := utf8Len l + utf8Len m } }
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>ValidFor (l ++ List.take n m) (List.drop n m) r { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) }, stopPos := { byteIdx := utf8Len l + utf8Len m } }
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>{ str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.stopPos.byteIdx = utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
<VAR>l m r : List Char<VAR>s : Substring<VAR>n : Nat<VAR>h : ValidFor l (List.take n m ++ List.drop n m) r s<VAR>this : { str := s.str, startPos := s.startPos, stopPos := s.stopPos }.nextn n 0 = { byteIdx := utf8Len (List.take n m) }<GOAL>{ str := { data := l ++ (List.take n m ++ List.drop n m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) }, stopPos := { byteIdx := utf8Len l + utf8Len (List.take n m ++ List.drop n m) } }.stopPos.byteIdx = utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>h : a ∈ s<GOAL>(s \ {a}).encard = s.encard - 1
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ₁ θ₂ : Real.Angle<VAR>x✝ : V<GOAL>((o.rotation θ₁).trans (o.rotation θ₂)) x✝ = (o.rotation (θ₂ + θ₁)) x✝
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>μs : ℕ → Measure Ω<VAR>f : Ω → ℝ<VAR>f_cont : Continuous f<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>μs : ℕ → Measure Ω<VAR>f : Ω → ℝ<VAR>f_cont : Continuous f<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} ≤ liminf (fun i => ∫⁻ (t : ℝ) in Ioi 0, (μs i) {a | t < f a}) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>ν : Measure α<GOAL>AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>ν : Measure α<GOAL>AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>IsLocalAtTarget P
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<GOAL>P f → ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)
<VAR>P : MorphismProperty Scheme<VAR>inst✝ : P.RespectsIso<VAR>restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)<VAR>of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)<GOAL>∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<GOAL>∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β × γ), ⨆ n, ↑(F n) a = Function.uncurry f a<GOAL>∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<GOAL>∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<GOAL>∫⁻ (bc : β × γ), ⨆ n, ↑(F n) (bc.1, bc.2) ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<GOAL>∫⁻ (bc : β × γ), ⨆ n, ↑(F n) (bc.1, bc.2) ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<GOAL>⨆ n, ∫⁻ (a : β × γ), ↑(F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<GOAL>⨆ n, ∫⁻ (a : β × γ), ↑(F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<GOAL>⨆ n, ∫⁻ (a : β × γ), ↑(F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<GOAL>⨆ n, ∫⁻ (a : β × γ), ↑(F n) a ∂(κ ⊗ₖ η) a = ⨆ n, ∫⁻ (a_1 : β), ∫⁻ (c : γ), ↑(F n) (a_1, c) ∂η (a, a_1) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<GOAL>∀ (n : ℕ), Measurable fun b => ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<GOAL>Monotone fun n b => ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<VAR>n : ℕ<GOAL>∫⁻ (a : β × γ), ↑(F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), ↑(F n) (a_1, c) ∂η (a, a_1) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<VAR>n : ℕ<GOAL>∀ (c : ℝ≥0∞) {s : Set (β × γ)} (hs : MeasurableSet s), ∫⁻ (a : β × γ), ↑(SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c_1 : γ), ↑(SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) (a_1, c_1) ∂η (a, a_1) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β → γ → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)<VAR>h : ∀ (a : β) (b : γ), ⨆ n, ↑(F n) (a, b) = f a b<VAR>h_mono : Monotone F<VAR>this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, ↑(F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), ↑(F n) (b, c) ∂η (a, b)<VAR>h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b => ∫⁻ (c : γ), ↑f' (b, c) ∂η (a, b)<VAR>n : ℕ<GOAL>∀ ⦃f g : SimpleFunc (β × γ) ℝ≥0∞⦄, Disjoint (Function.support ↑f) (Function.support ↑g) → ∫⁻ (a : β × γ), ↑f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_2 : β), ∫⁻ (c : γ), ↑f (a_2, c) ∂η (a, a_2) ∂κ a → ∫⁻ (a : β × γ), ↑g a ∂(κ ⊗ₖ η) a = ∫⁻ (a_3 : β), ∫⁻ (c : γ), ↑g (a_3, c) ∂η (a, a_3) ∂κ a → ∫⁻ (a : β × γ), ↑(f + g) a ∂(κ ⊗ₖ η) a = ∫⁻ (a_4 : β), ∫⁻ (c : γ), ↑(f + g) (a_4, c) ∂η (a, a_4) ∂κ a
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>m : Fin n →₀ ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<GOAL>coeff m (((finSuccEquiv R n) f).coeff i) = coeff (cons i m) f
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>j : Fin (n + 1) →₀ ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p q : MvPolynomial (Fin (n + 1)) R<VAR>hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) p).coeff i) = coeff (cons i m) p<VAR>hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) q).coeff i) = coeff (cons i m) q<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>coeff m (((finSuccEquiv R n) (p + q)).coeff i) = coeff (cons i m) (p + q)
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>j : Fin (n + 1) →₀ ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x : Fin n, X x ^ j x.succ)).coeff i) = if j = cons i m then r else 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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>j : Fin (n + 1) →₀ ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>r * coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0