ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>R₁ : Type u_10<VAR>inst✝⁴ : Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M → ι → R<VAR>hadd : ∀ (x y : M), f (x + y) = f x + f y<VAR>hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x<VAR>f_eq : ∀ (i : ι), f (b i) = ⇑(Finsupp.single i 1)<VAR>x : M<VAR>i : ι<VAR>f_i : M →ₗ[R] R := { toFun := fun x => f x i, map_add' := ⋯, map_smul' := ⋯ }<GOAL>(b.repr x) i = f x i
<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<VAR>R₁ : Type u_10<VAR>inst✝⁴ : Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M → ι → R<VAR>hadd : ∀ (x y : M), f (x + y) = f x + f y<VAR>hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x<VAR>f_eq : ∀ (i : ι), f (b i) = ⇑(Finsupp.single i 1)<VAR>x : M<VAR>i : ι<VAR>f_i : M →ₗ[R] R := { toFun := fun x => f x i, map_add' := ⋯, map_smul' := ⋯ }<VAR>this : Finsupp.lapply i ∘ₗ ↑b.repr = f_i<GOAL>(b.repr x) i = f x i
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : map f p ≤ P ^ n<VAR>hgt : ¬map f p ≤ P ^ (n + 1)<VAR>Q : ℕ → Prop := fun m => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m<GOAL>ramificationIdx f p P = n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : map f p ≤ P ^ n<VAR>hgt : ¬map f p ≤ P ^ (n + 1)<VAR>Q : ℕ → Prop := fun m => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m<VAR>this : Q n<GOAL>ramificationIdx f p P = n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : map f p ≤ P ^ n<VAR>hgt : ¬map f p ≤ P ^ (n + 1)<VAR>Q : ℕ → Prop := fun m => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m<VAR>this : Q n<GOAL>Nat.find ⋯ = n
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : map f p ≤ P ^ n<VAR>hgt : ¬map f p ≤ P ^ (n + 1)<VAR>Q : ℕ → Prop := fun m => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m<VAR>this : Q n<VAR>h : Nat.find ⋯ < n<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>n : ℕ<VAR>hle : map f p ≤ P ^ n<VAR>hgt : ¬map f p ≤ P ^ (n + 1)<VAR>Q : ℕ → Prop := fun m => ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ m<VAR>this : Q n<VAR>h : Nat.find ⋯ < n<VAR>this' : Q (Nat.find ⋯)<GOAL>False
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : Ordinal.{u}<GOAL>x ≤ sSup ({x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x})
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a : Ordinal.{u}<GOAL>x ∈ {x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x}
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁷ : Fintype α<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>S : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulCommClass R S M<VAR>v : α → M<VAR>inst✝ : DecidableEq α<VAR>i : α<VAR>r : R<GOAL>((Fintype.total R S) v) (Pi.single i r) = r • v i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁷ : Fintype α<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>S : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulCommClass R S M<VAR>v : α → M<VAR>inst✝ : DecidableEq α<VAR>i : α<VAR>r : R<GOAL>(∑ x : α, if x = i then r • v x else 0) = r • v i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_4, u_1} C<VAR>inst✝⁶ : Category.{u_3, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : hr₁.IsPreservedBy F<VAR>inst✝ : hr₂.IsPreservedBy F<VAR>γ : RightHomologyMapData φ hr₁ hr₂<GOAL>F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>t : Set E<VAR>x y : E<VAR>ht : Convex ℝ t<VAR>hs₁ : Convex ℝ ∅<VAR>hs₂ : IsOpen ∅<VAR>disj : Disjoint ∅ t<GOAL>∃ f u, (∀ a ∈ ∅, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>ht : Convex ℝ ∅<VAR>disj : Disjoint s ∅<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ ∅, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this : 0 ∈ C<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝ : 0 ∈ C<VAR>this : Convex ℝ C<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝¹ : 0 ∈ C<VAR>this✝ : Convex ℝ C<VAR>this : x₀ ∉ C<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝¹ : 0 ∈ C<VAR>this✝ : Convex ℝ C<VAR>this : x₀ ∉ C<VAR>f : E →L[ℝ] ℝ<VAR>hf₁ : f x₀ = 1<VAR>hf₂ : ∀ x ∈ C, f x < 1<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝² : 0 ∈ C<VAR>this✝¹ : Convex ℝ C<VAR>this✝ : x₀ ∉ C<VAR>f : E →L[ℝ] ℝ<VAR>hf₁ : f x₀ = 1<VAR>hf₂ : ∀ x ∈ C, f x < 1<VAR>this : f b₀ = f a₀ + 1<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝² : 0 ∈ C<VAR>this✝¹ : Convex ℝ C<VAR>this✝ : x₀ ∉ C<VAR>f : E →L[ℝ] ℝ<VAR>hf₁ : f x₀ = 1<VAR>hf₂ : ∀ x ∈ C, f x < 1<VAR>this : f b₀ = f a₀ + 1<VAR>forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝² : 0 ∈ C<VAR>this✝¹ : Convex ℝ C<VAR>this✝ : x₀ ∉ C<VAR>f : E →L[ℝ] ℝ<VAR>hf₁ : f x₀ = 1<VAR>hf₂ : ∀ x ∈ C, f x < 1<VAR>this : f b₀ = f a₀ + 1<VAR>forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b<GOAL>⇑f '' s ⊆ Iio (sInf (⇑f '' t))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<VAR>x₀ : E := b₀ - a₀<VAR>C : Set E := x₀ +ᵥ (s - t)<VAR>this✝² : 0 ∈ C<VAR>this✝¹ : Convex ℝ C<VAR>this✝ : x₀ ∉ C<VAR>f : E →L[ℝ] ℝ<VAR>hf₁ : f x₀ = 1<VAR>hf₂ : ∀ x ∈ C, f x < 1<VAR>this : f b₀ = f a₀ + 1<VAR>forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b<VAR>b : E<VAR>hb : b ∈ t<GOAL>sInf (⇑f '' t) ≤ f b
<VAR>x y z : PGame<GOAL>⟦(x + y) * z⟧ = ⟦x * z⟧ + ⟦y * z⟧
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : 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_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<GOAL>range 0 = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>(fun t => f₀ (x + t • v)) =ᶠ[𝓝[(fun t => x + t • v) ⁻¹' s] 0] fun t => f₁ (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>f₀ (x + 0 • v) = f₁ (x + 0 • v)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Icc (a + n • p) (a + (n + 1) • p) = univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>p : Fix F → Prop<VAR>h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), p (Quot.mk Setoid.r (f a))<GOAL>p ⟦WType.mk a f⟧
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>p : Fix F → Prop<VAR>h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), p (Quot.mk Setoid.r (f a))<GOAL>p (mk (abs ⟨a, fun x => ⟦f x⟧⟩))
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>p : Fix F → Prop<VAR>h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), p (Quot.mk Setoid.r (f a))<GOAL>Liftp p (abs ⟨a, fun x => ⟦f x⟧⟩)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>p : Fix F → Prop<VAR>h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)<VAR>x✝ : Fix F<VAR>a : (P F).A<VAR>f : (P F).B a → WType (P F).B<VAR>ih : ∀ (a : (P F).B a), p (Quot.mk Setoid.r (f a))<GOAL>∃ a_1 f_1, abs ⟨a, fun x => ⟦f x⟧⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : (P F).B a_1), p (f_1 i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f✝ : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>f : α × β → StieltjesFunction<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : ℝ<GOAL>∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f✝ : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>f : α × β → StieltjesFunction<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : ℝ<GOAL>(κ a) (s ×ˢ Iic x) ≠ ⊤
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>HasIntegral I l (s.indicator fun x => y) μ.toBoxAdditive.toSMul ((μ (s ∩ ↑I)).toReal • y)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>this : ∀ x ∈ s ∩ Box.Icc I, ∃ r, closedBall x ↑r ⊆ U<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>l : IntegrationParams<VAR>hl : l.bRiemann = false<VAR>s : Set (ι → ℝ)<VAR>hs : MeasurableSet s<VAR>I : Box ι<VAR>y : E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ε<VAR>A : μ (s ∩ Box.Icc I) ≠ ⊤<VAR>B : μ (s ∩ ↑I) ≠ ⊤<VAR>F : Set (ι → ℝ)<VAR>hFs : F ⊆ s ∩ Box.Icc I<VAR>hFc : IsClosed F<VAR>hμF : μ ((s ∩ Box.Icc I) \ F) < ↑ε<VAR>U : Set (ι → ℝ)<VAR>hsU : s ∩ Box.Icc I ⊆ U<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ (s ∩ Box.Icc I)) < ↑ε<VAR>rs : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hrsU : ∀ x ∈ s ∩ Box.Icc I, closedBall x ↑(rs x) ⊆ U<VAR>this : ∀ x ∈ Box.Icc I \ s, ∃ r, closedBall x ↑r ⊆ Fᶜ<GOAL>∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (integralSum (s.indicator fun x => y) μ.toBoxAdditive.toSMul π) ((μ (s ∩ ↑I)).toReal • y) ≤ ‖y‖ * ↑ε