ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>x : E<VAR>hx : x ∈ s<VAR>hw : f x ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}<VAR>ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty<VAR>hyt : ∀ ⦃x₁ : E⦄, x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x<GOAL>f x ∈ ⇑f '' extremePoints ℝ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>x : E<VAR>hx : x ∈ s<VAR>hw : f x ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}<VAR>ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty<VAR>hyt : ∀ ⦃x₁ : E⦄, x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x<VAR>y : E<VAR>hy : y ∈ s<VAR>z : E<VAR>hz : z ∈ s<VAR>hxyz : x ∈ openSegment ℝ y z<GOAL>y = x ∧ z = x
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>x : E<VAR>hx : x ∈ s<VAR>hw : f x ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}<VAR>ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty<VAR>hyt : ∀ ⦃x₁ : E⦄, x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x<VAR>y : E<VAR>hy : y ∈ s<VAR>z : E<VAR>hz : z ∈ s<VAR>hxyz : x ∈ openSegment ℝ y z<VAR>this : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)<GOAL>y = x ∧ z = x
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>x : E<VAR>hx : x ∈ s<VAR>hw : f x ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}<VAR>ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty<VAR>hyt : ∀ ⦃x₁ : E⦄, x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x<VAR>y : E<VAR>hy : y ∈ s<VAR>z : E<VAR>hz : z ∈ s<VAR>hxyz : x ∈ openSegment ℝ y z<VAR>this✝ : (fun a => f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)<VAR>this : f y = f x ∧ f z = f x<GOAL>y = x ∧ z = x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>c : R<GOAL>derivative (X - C c) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<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✝ : FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<GOAL>implicitFunction f f' hf hf' (f a) 0 = a
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<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✝ : FiniteDimensional 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>this : CompleteSpace F<GOAL>implicitFunction f f' hf hf' (f a) 0 = a
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.250723, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 3<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<GOAL>3 < 3 + 1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>↑Dᶜ = A \ ↑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>a : A<VAR>n : ℕ<GOAL>mulRight R a ^ n = mulRight R (a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>a : A<VAR>n : ℕ<GOAL>(mul R A).flip a ^ n = (mul R A).flip (a ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>decodeSum n = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>this : 1 ≤ n / 2<GOAL>decodeSum n = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>this : 1 ≤ n / 2<VAR>m : ℕ<VAR>e : n / 2 = m.succ<GOAL>decodeSum n = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>h : 2 ≤ n<VAR>this : 1 ≤ n / 2<VAR>m : ℕ<VAR>e : n / 2 = m.succ<GOAL>(match (n.bodd, n / 2) with | (false, m) => Option.map Sum.inl (decode m) | (fst, m) => Option.map Sum.inr (decode m)) = none
<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>f g : α → ℝ≥0∞<GOAL>∑' (i : α), f i * a = (∑' (i : α), f i) * a
<VAR>w x y z✝ z : ℝ<VAR>h : 0 ≤ z<VAR>h0 : 0 = z<GOAL>Monotone fun x => x ^ 0
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>h : (find p).isSome = true<GOAL>∃ i, p i
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>h : ∃ a, find p = some a<GOAL>∃ i, p i
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>i : Fin (n + 1)<VAR>hi : find p = some i<GOAL>∃ i, p i
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝¹ : DecidablePred p<VAR>x✝ : ∃ i, p i<VAR>i : ℕ<VAR>hin : i < n + 1<VAR>hi : p ⟨i, hin⟩<GOAL>(Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) (find fun i => p (i.castLT ⋯))).isSome = true
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝¹ : DecidablePred p<VAR>x✝ : ∃ i, p i<VAR>i : ℕ<VAR>hin : i < n + 1<VAR>hi : p ⟨i, hin⟩<VAR>h : (find fun i => p (i.castLT ⋯)) = none<GOAL>(Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) none).isSome = true
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝¹ : DecidablePred p<VAR>x✝ : ∃ i, p i<VAR>i : ℕ<VAR>hin : i < n + 1<VAR>hi : p ⟨i, hin⟩<VAR>j : Fin n<VAR>h : (find fun i => p (i.castLT ⋯)) = some j<GOAL>(Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) (some j)).isSome = true
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>homogeneousCore' 𝒜 I = sSup {J | IsHomogeneous 𝒜 J ∧ J ≤ I}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>IsLUB {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<GOAL>IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<GOAL>IsGreatest {J | IsHomogeneous 𝒜 J ∧ J ≤ I} (homogeneousCore' 𝒜 I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<GOAL>{J | IsHomogeneous 𝒜 J ∧ J ≤ I} = toIdeal '' {a | a.toIdeal ≤ I}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<VAR>x : Ideal A<GOAL>x ∈ {J | IsHomogeneous 𝒜 J ∧ J ≤ I} ↔ x ∈ toIdeal '' {a | a.toIdeal ≤ I}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<VAR>x : Ideal A<GOAL>IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<VAR>x : Ideal A<GOAL>(∃ x_1 ∈ {a | a.toIdeal ≤ I}, x_1.toIdeal = x) → IsHomogeneous 𝒜 x ∧ x ≤ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>coe_mono : Monotone toIdeal<VAR>x : HomogeneousIdeal 𝒜<VAR>hx : x ∈ {a | a.toIdeal ≤ I}<GOAL>IsHomogeneous 𝒜 x.toIdeal ∧ x.toIdeal ≤ I
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>μ (sphere x r) = 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>h : r < 0<GOAL>μ (sphere x r) = 0
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>h : 0 < r<GOAL>μ (sphere x r) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t : Set E<VAR>x : E<GOAL>x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g✝ : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x<VAR>x : X<GOAL>ContinuousWithinAt g (⋃ i, f i) x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g✝ : ι → Set X<VAR>g : X → Y<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x<VAR>x : X<GOAL>∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>b - toIcoMod hp a b = toIcoDiv hp a b • p
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁴ : CommRing R₁<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁<VAR>M : Matrix ι ι R₁<VAR>h : M.Nondegenerate<VAR>x : ι → R₁<VAR>hx : ∀ (y : ι → R₁), (((Matrix.toLinearMap₂' R₁) M) x) y = 0<VAR>y : ι → R₁<GOAL>x ⬝ᵥ M *ᵥ y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] ∅<GOAL>s ∪ t =ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] ∅<GOAL>t = ∅ ∪ t
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h✝ : β → G γ<VAR>f : β → γ<VAR>x : t β<VAR>g : α → F β<VAR>h : β → G γ<VAR>x✝ : t α<GOAL>traverse (Comp.mk ∘ map h ∘ g) x✝ = (Comp.mk ∘ map (traverse h) ∘ traverse g) x✝
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<GOAL>χ₀ n (RingEquiv.refl L) = 1
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<GOAL>(RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
<VAR>L : Type u<VAR>inst✝¹ : CommRing L<VAR>inst✝ : IsDomain L<VAR>n : ℕ+<VAR>t : ↥(rootsOfUnity n L)<VAR>this : 1 ≤ Fintype.card ↥(rootsOfUnity n L)<GOAL>(RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<GOAL>(dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<VAR>this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)<GOAL>(dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<VAR>this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)<VAR>e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator := (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator<GOAL>(dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<VAR>this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)<VAR>e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator := (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator<VAR>this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator<GOAL>(dualAnnihilator W).dualAnnihilator = map (Dual.eval K V) W
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<VAR>this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)<VAR>e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator := (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator<VAR>this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator<GOAL>finrank K ↥(map (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
<VAR>K✝ : Type uK<VAR>inst✝⁸ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K✝ V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>W : Subspace K V<VAR>inst✝ : FiniteDimensional K ↥W<VAR>e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W := (Free.chooseBasis K ↥W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm<VAR>this✝ : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)<VAR>e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator := (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)).toDualEquiv ≪≫ₗ (dualAnnihilator W).dualQuotEquivDualAnnihilator<VAR>this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator<GOAL>finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a / b < 1 ↔ a < b
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k<GOAL>upcrossings a b f ω < ⊤ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>this : upcrossings a b f ω < ⊤ ↔ ∃ k, upcrossings a b f ω ≤ ↑k<GOAL>(∃ k, ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k) ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>x y : (α →𝒄 β) × α<VAR>h : x ≤ y<GOAL>x.1 x.2 ≤ y.1 y.2
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c : Chain ((α →𝒄 β) × α)<GOAL>{ toFun := fun f => f.1 f.2, monotone' := ⋯ } (ωSup c) = ωSup (c.map { toFun := fun f => f.1 f.2, monotone' := ⋯ })
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c : Chain ((α →𝒄 β) × α)<GOAL>{ toFun := fun f => f.1 f.2, monotone' := ⋯ } (ωSup c) ≤ ωSup (c.map { toFun := fun f => f.1 f.2, monotone' := ⋯ })
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β : Type v<VAR>β' : Type u_2<VAR>γ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β<VAR>inst✝³ : OmegaCompletePartialOrder γ<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>c : Chain ((α →𝒄 β) × α)<GOAL>ωSup (c.map { toFun := fun f => f.1 f.2, monotone' := ⋯ }) ≤ { toFun := fun f => f.1 f.2, monotone' := ⋯ } (ωSup c)
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i j : ι<VAR>h_le : i ≤ j<VAR>hi_max : ¬IsMax i<VAR>hj_min : ¬IsMin j<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i j : ι<VAR>h_le : i ≤ j<VAR>hi_max : ¬IsMax i<VAR>hj_min : ¬IsMin j<VAR>hi : i0 ≤ i<VAR>hj : i0 ≤ j<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i j : ι<VAR>h_le : i ≤ j<VAR>hi_max : ¬IsMax i<VAR>hj_min : ¬IsMin j<VAR>hi : i0 ≤ i<VAR>hj : j < i0<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i j : ι<VAR>h_le : i ≤ j<VAR>hi_max : ¬IsMax i<VAR>hj_min : ¬IsMin j<VAR>hi : i < i0<VAR>hj : i0 ≤ j<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i j : ι<VAR>h_le : i ≤ j<VAR>hi_max : ¬IsMax i<VAR>hj_min : ¬IsMin j<VAR>hi : i < i0<VAR>hj : j < i0<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<GOAL>(LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g