ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>m : ι → OuterMeasure α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range fun i => m i, μ (t n) = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>p : Set X → Prop<VAR>he : p ∅<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<VAR>f : Filter X := comk p he ⋯ ⋯<GOAL>p s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>p : Set X → Prop<VAR>he : p ∅<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<VAR>f : Filter X := comk p he ⋯ ⋯<VAR>this : sᶜ ∈ f<GOAL>p s
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>x : F<VAR>hx : x ∈ f '' s<VAR>y : F<VAR>hy : y ∈ f '' s<VAR>A : PartialEquiv E F := hf.toPartialEquiv hc<VAR>Af : ∀ (z : E), ↑A z = f z<GOAL>‖↑A.symm x - ↑A.symm y - ↑f'.symm (x - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>y : F<VAR>hy : y ∈ f '' s<VAR>A : PartialEquiv E F := hf.toPartialEquiv hc<VAR>Af : ∀ (z : E), ↑A z = f z<VAR>x' : E<VAR>x's : x' ∈ s<VAR>hx : f x' ∈ f '' s<GOAL>‖↑A.symm (f x') - ↑A.symm y - ↑f'.symm (f x' - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>A : PartialEquiv E F := hf.toPartialEquiv hc<VAR>Af : ∀ (z : E), ↑A z = f z<VAR>x' : E<VAR>x's : x' ∈ s<VAR>hx : f x' ∈ f '' s<VAR>y' : E<VAR>y's : y' ∈ s<VAR>hy : f y' ∈ f '' s<GOAL>‖↑A.symm (f x') - ↑A.symm (f y') - ↑f'.symm (f x' - f y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖f x' - f y'‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>ε : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹<VAR>A : PartialEquiv E F := hf.toPartialEquiv hc<VAR>Af : ∀ (z : E), ↑A z = f z<VAR>x' : E<VAR>x's : x' ∈ s<VAR>hx : f x' ∈ f '' s<VAR>y' : E<VAR>y's : y' ∈ s<VAR>hy : f y' ∈ f '' s<GOAL>‖x' - y' - ↑f'.symm (↑A x' - ↑A y')‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖↑A x' - ↑A y'‖
<VAR>x : ℝ≥0∞<GOAL>↑x = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = ⟪↑v, y⟫_𝕜<VAR>u : E<VAR>hu : u ∈ K<GOAL>⟪u, x - y⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>K : Submodule 𝕜 E<VAR>x y : E<VAR>h : ∀ (v : ↥K), ⟪↑v, x⟫_𝕜 = ⟪↑v, y⟫_𝕜<VAR>u : E<VAR>hu : u ∈ K<GOAL>⟪u, x⟫_𝕜 = ⟪u, y⟫_𝕜
<VAR>w x✝ y✝ z x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ≥0<GOAL>(fun y => y ^ x) (y ^ x⁻¹) = y
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<GOAL>I.distortion = J.distortion
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<GOAL>(Finset.univ.sup fun i => (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) / (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) = Finset.univ.sup fun i => (Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i)
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<VAR>i : ι<GOAL>↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) / (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) = ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<VAR>i : ι<VAR>this : 0 < r<GOAL>↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) / (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) = ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>r : ℝ<VAR>h : ∀ (i : ι), I.upper i - I.lower i = (J.upper i - J.lower i) / r<VAR>i : ι<VAR>this : 0 < r<VAR>hn0 : Real.nnabs r ≠ 0<GOAL>↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b) / Real.nnabs r) / (Real.nnabs (J.upper i - J.lower i) / Real.nnabs r)) = ↑((Finset.univ.sup fun b => Real.nnabs (J.upper b - J.lower b)) / Real.nnabs (J.upper i - J.lower i))
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<VAR>hp : ¬p = 0<GOAL>(p.cancelLeads q).natDegree < q.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<VAR>hp : ¬p = 0<GOAL>(C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<VAR>hp : ¬p = 0<VAR>h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0<GOAL>(C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<VAR>hp : ¬p = 0<VAR>h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0<GOAL>(C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree ≤ q.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff<VAR>h : p.natDegree ≤ q.natDegree<VAR>hq : 0 < q.natDegree<VAR>hp : ¬p = 0<VAR>h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0<GOAL>(C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree ≠ q.natDegree
<VAR>ι : Type uι<VAR>inst✝¹⁰ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝³ : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝² : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>c : 𝕜<VAR>u : E i →L[𝕜] E' i<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>(mapL (update f i (c • u))) x = (c • mapL (update f i u)) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a \ b) \ b = a \ b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<GOAL>W.Nonsingular ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t : Finset ι<GOAL>∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t : Finset ι<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → (∀ (m' : (i : ι) → M₁ i), f (s.piecewise (m + m') m') = ∑ s ∈ s.powerset, f (s.piecewise m m')) → ∀ (m' : (i : ι) → M₁ i), f ((insert a s).piecewise (m + m') m') = ∑ s ∈ (insert a s).powerset, f (s.piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<GOAL>f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<VAR>A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)<GOAL>f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<VAR>A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)<VAR>B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'<VAR>m'' : (a : ι) → M₁ a := update m' i (m i)<VAR>C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''<GOAL>f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<VAR>A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)<VAR>B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'<VAR>m'' : (a : ι) → M₁ a := update m' i (m i)<VAR>C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''<GOAL>∑ s ∈ t.powerset, f (s.piecewise m m') + ∑ s ∈ t.powerset, f (s.piecewise m m'') = ∑ t ∈ t.powerset, f (t.piecewise m m') + ∑ t ∈ t.powerset, f ((insert i t).piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<VAR>A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)<VAR>B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'<VAR>m'' : (a : ι) → M₁ a := update m' i (m i)<VAR>C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''<GOAL>∑ s ∈ t.powerset, f (s.piecewise m m'') = ∑ t ∈ t.powerset, f ((insert i t).piecewise m m')
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>t✝ : Finset ι<VAR>i : ι<VAR>t : Finset ι<VAR>hit : i ∉ t<VAR>Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')<VAR>m' : (i : ι) → M₁ i<VAR>A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)<VAR>B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'<VAR>m'' : (a : ι) → M₁ a := update m' i (m i)<VAR>C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''<VAR>s : Finset ι<VAR>hs : s ∈ t.powerset<GOAL>f (s.piecewise m m'') = f ((insert i s).piecewise m m')
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>M : Matrix n n α<VAR>v : n → α<GOAL>M = (diagonal v)ᵀ ↔ M = diagonal v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>f : Filter α<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>u : α → β<VAR>b : β<VAR>h : b < liminf u f<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<GOAL>∀ᶠ (a : α) in f, b < u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>f : Filter α<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>u : α → β<VAR>b : β<VAR>h : b < liminf u f<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝<VAR>c : β<VAR>hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}<VAR>hbc : b < c<GOAL>∀ᶠ (a : α) in f, b < u a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℚ<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) univ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>hf : ¬Integrable f μ<GOAL>∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : IsCompact s<VAR>h's : MeasurableSet s<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : IsCompact s<VAR>h's : MeasurableSet s<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEMeasurable f (μ.restrict s) ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : IsCompact s<VAR>h's : MeasurableSet s<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>IsSeparable (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : IsCompact s<VAR>h's : MeasurableSet s<VAR>this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>wf : WellFounded r<VAR>x : α<VAR>h : ∃ y, r x y<GOAL>r x (wf.succ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>wf : WellFounded r<VAR>x : α<VAR>h : ∃ y, r x y<GOAL>r x (wf.min {y | r x y} h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<GOAL>(-s).toJordanDecomposition = -s.toJordanDecomposition
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<GOAL>(-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ⊤}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, a ∈ v ∧ v ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>x : α<VAR>s : Set α<VAR>xs : x ∈ s<VAR>hs : IsOpen s<GOAL>∃ v ∈ {s | IsOpen s ∧ μ s < ⊤}, x ∈ v ∧ v ⊆ s