ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<VAR>a : Set α<VAR>ha₁ : MeasurableSet a<VAR>ha₂ : a ⊆ ⋃ n, f n<GOAL>↑v a ≤ ↑w a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<VAR>a : Set α<VAR>ha₁ : MeasurableSet a<VAR>ha₂ : a ⊆ ⋃ n, f n<VAR>ha₃ : ⋃ n, a ∩ disjointed f n = a<GOAL>↑v a ≤ ↑w a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<VAR>a : Set α<VAR>ha₁ : MeasurableSet a<VAR>ha₂ : a ⊆ ⋃ n, f n<VAR>ha₃ : ⋃ n, a ∩ disjointed f n = a<VAR>ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)<GOAL>↑v a ≤ ↑w a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<VAR>a : Set α<VAR>ha₁ : MeasurableSet a<VAR>ha₂ : a ⊆ ⋃ n, f n<VAR>ha₃ : ⋃ n, a ∩ disjointed f n = a<VAR>ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)<GOAL>∑' (i : ℕ), ↑v (a ∩ disjointed f i) ≤ ∑' (i : ℕ), ↑w (a ∩ disjointed f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : OrderedAddCommMonoid M<VAR>inst✝ : OrderClosedTopology M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (n : ℕ), MeasurableSet (f n)<VAR>hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)<VAR>a : Set α<VAR>ha₁ : MeasurableSet a<VAR>ha₂ : a ⊆ ⋃ n, f n<VAR>ha₃ : ⋃ n, a ∩ disjointed f n = a<VAR>ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)<GOAL>∀ (i : ℕ), MeasurableSet (a ∩ disjointed f i)
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : CommSemigroup β<VAR>inst✝¹ : LE β<VAR>inst✝ : SubmultiplicativeHomClass F α β<VAR>f : F<VAR>a b c : α<GOAL>f (a / c) ≤ f (a / b) * f (b / c)
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J : Box ι<VAR>hJ : J ∈ π.boxes.biUnion fun J => (πi J).boxes<GOAL>J ≤ I
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J : Box ι<VAR>hJ : ∃ a ∈ π, J ∈ πi a<GOAL>J ≤ I
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J J' : Box ι<VAR>hJ' : J' ∈ π<VAR>hJ : J ∈ πi J'<GOAL>J ≤ I
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<GOAL>(↑(π.boxes.biUnion fun J => (πi J).boxes)).Pairwise (Disjoint on Box.toSet)
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<GOAL>∀ ⦃x : Box ι⦄, (∃ a ∈ π.boxes, x ∈ (πi a).boxes) → ∀ ⦃y : Box ι⦄, (∃ a ∈ π.boxes, y ∈ (πi a).boxes) → x ≠ y → (Disjoint on Box.toSet) x y
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J₁' J₁ : Box ι<VAR>hJ₁ : J₁ ∈ π.boxes<VAR>hJ₁' : J₁' ∈ (πi J₁).boxes<VAR>J₂' J₂ : Box ι<VAR>hJ₂ : J₂ ∈ π.boxes<VAR>hJ₂' : J₂' ∈ (πi J₂).boxes<VAR>Hne : J₁' ≠ J₂'<GOAL>(Disjoint on Box.toSet) J₁' J₂'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J₁' J₁ : Box ι<VAR>hJ₁ : J₁ ∈ π.boxes<VAR>hJ₁' : J₁' ∈ (πi J₁).boxes<VAR>J₂' J₂ : Box ι<VAR>hJ₂ : J₂ ∈ π.boxes<VAR>hJ₂' : J₂' ∈ (πi J₂).boxes<VAR>Hne : J₁' ≠ J₂'<GOAL>∀ ⦃a : ι → ℝ⦄, a ∈ ↑J₁' → a ∉ ↑J₂'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂✝ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J₁' J₁ : Box ι<VAR>hJ₁ : J₁ ∈ π.boxes<VAR>hJ₁' : J₁' ∈ (πi J₁).boxes<VAR>J₂' J₂ : Box ι<VAR>hJ₂ : J₂ ∈ π.boxes<VAR>hJ₂' : J₂' ∈ (πi J₂).boxes<VAR>Hne : J₁' ≠ J₂'<VAR>x : ι → ℝ<VAR>hx₁ : x ∈ ↑J₁'<VAR>hx₂ : x ∈ ↑J₂'<GOAL>J₁' = J₂'
<VAR>ι : Type u_1<VAR>I J J₁✝ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x✝ : ι → ℝ<VAR>πi : (J : Box ι) → Prepartition J<VAR>J₁' J₁ : Box ι<VAR>hJ₁ : J₁ ∈ π.boxes<VAR>hJ₁' : J₁' ∈ (πi J₁).boxes<VAR>J₂' : Box ι<VAR>Hne : J₁' ≠ J₂'<VAR>x : ι → ℝ<VAR>hx₁ : x ∈ ↑J₁'<VAR>hx₂ : x ∈ ↑J₂'<VAR>hJ₂ : J₁ ∈ π.boxes<VAR>hJ₂' : J₂' ∈ (πi J₁).boxes<GOAL>J₁' = J₂'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>y : α<VAR>h : ∃ y_1, r y y_1<GOAL>r y (⋯.succ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε : α<VAR>ε0 : ε > 0<VAR>j : ℕ<VAR>x✝ : j ≥ 0<GOAL>abv (↑0 j) < ε
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<VAR>this : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<VAR>this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)<VAR>this : Rₘ →ₐ[R] Q := let __src := IsLocalization.lift this✝; { toRingHom := __src, commutes' := ⋯ }<GOAL>∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<VAR>this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)<VAR>this : Rₘ →ₐ[R] Q := let __src := IsLocalization.lift this✝; { toRingHom := __src, commutes' := ⋯ }<GOAL>(Ideal.Quotient.mkₐ R I).comp this = f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<VAR>this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)<VAR>this : Rₘ →ₐ[R] Q := let __src := IsLocalization.lift this✝; { toRingHom := __src, commutes' := ⋯ }<GOAL>↑((Ideal.Quotient.mkₐ R I).comp this) = ↑f
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f : Rₘ →ₐ[R] Q ⧸ I<VAR>this✝ : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)<VAR>this : Rₘ →ₐ[R] Q := let __src := IsLocalization.lift this✝; { toRingHom := __src, commutes' := ⋯ }<GOAL>(↑((Ideal.Quotient.mkₐ R I).comp this)).comp (algebraMap R Rₘ) = (↑f).comp (algebraMap R Rₘ)
<GOAL>eval (1 / 4) (bernoulli 3) = 3 / 64
<GOAL>eval (1 / 4) (∑ i ∈ Finset.range 0, (monomial (3 - i)) (_root_.bernoulli i * ↑(Nat.choose 3 i))) + _root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + _root_.bernoulli 1 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) + _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) + _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) = 3 / 64
<GOAL>_root_.bernoulli 0 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) + _root_.bernoulli 2 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) + _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) = 3 / 64
<GOAL>1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) + 1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) + 0 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) = 3 / 64
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>f⁻¹.IsCycleOn s ↔ f.IsCycleOn s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>(∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) → (Set.BijOn (⇑f⁻¹) s s ↔ Set.BijOn (⇑f) s s)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<GOAL>∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<VAR>this : Fact (Nat.Prime (ringChar F))<GOAL>∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<VAR>this : Fact (Nat.Prime (ringChar F))<VAR>htr : (∀ (n : F), ((Algebra.traceForm (ZMod (ringChar F)) F) a) n = 0) → a = 0<GOAL>∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<VAR>this : Fact (Nat.Prime (ringChar F))<VAR>htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0<GOAL>∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>inst✝¹ : Finite F<VAR>inst✝ : Algebra (ZMod (ringChar F)) F<VAR>a : F<VAR>ha : a ≠ 0<VAR>this : Fact (Nat.Prime (ringChar F))<VAR>htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0<VAR>hf : ∀ (b : F), (Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0<GOAL>False
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>x✝¹ x✝ : ↑(Iic a)<GOAL>{ toFun := fun x => ⟨↑↑x, ⋯⟩, invFun := fun x => ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤ { toFun := fun x => ⟨↑↑x, ⋯⟩, invFun := fun x => ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝ ↔ x✝¹ ≤ x✝
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>X✝ Y✝ Z : C<VAR>inst✝¹ : HasPullbacks C<VAR>X Y S X' Y' S' : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>f' : X' ⟶ S'<VAR>g' : Y' ⟶ S'<VAR>i₁ : X ⟶ X'<VAR>i₂ : Y ⟶ Y'<VAR>i₃ : S ⟶ S'<VAR>e₁ : f ≫ i₃ = i₁ ≫ f'<VAR>e₂ : g ≫ i₃ = i₂ ≫ g'<VAR>inst✝ : Mono i₃<GOAL>lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ = lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂
<VAR>α : Type u_1<VAR>s✝ t : Set α<VAR>a : α<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : StarRing α<VAR>s : Set α<VAR>x✝ : α<GOAL>x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝ : J.HasSheafCompose (forget D)<GOAL>Presieve.IsSeparated J (F₁.val ⋙ forget D)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝ : J.HasSheafCompose (forget D)<GOAL>Presieve.IsSheaf J (F₁.val ⋙ forget D)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : ConcreteCategory D<VAR>J : GrothendieckTopology C<VAR>F₁ F₂ : Sheaf J D<VAR>φ : F₁ ⟶ F₂<VAR>inst✝ : J.HasSheafCompose (forget D)<GOAL>Presheaf.IsSheaf J (F₁.val ⋙ forget D)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>infDist x s ≤ infDist y s + dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>(infEdist x s).toReal ≤ (infEdist y s).toReal + (edist x y).toReal
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>infEdist y s = ⊤ → infEdist x s = ⊤
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>∀ (x : E), (∃ a, (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) → ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<GOAL>IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>this : Prod.map f f '' A ⊆ t ×ˢ t<GOAL>IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommMonoid G<VAR>inst✝ : AddCommMonoid H<VAR>A B : Set (G × G)<VAR>s : Set G<VAR>t : Set H<VAR>f : G → H<VAR>a b c x₁ y₁ x₂ y₂ : G<VAR>hf : IsAddFreimanIso 2 s t f<VAR>hAs : A ⊆ s ×ˢ s<VAR>this : Prod.map f f '' A ⊆ t ×ˢ t<GOAL>(∀ ⦃x₁ : H⦄, x₁ ∈ t → ∀ ⦃y₁ : H⦄, y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔ ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f✝ : X ⟶ Y<VAR>F✝ F'✝ : MonoFactorisation f✝<VAR>hF✝ : IsImage F✝<VAR>hF' : IsImage F'✝<VAR>f g : Arrow C<VAR>F : MonoFactorisation f.hom<VAR>hF : IsImage F<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<VAR>F' : MonoFactorisation g.hom<GOAL>(fun F' => hF.lift (F'.ofArrowIso (inv sq))) F' ≫ F'.m = (F.ofArrowIso sq).m
<VAR>α : Type u<VAR>m n : ℕ<VAR>a : Fin m → α<VAR>b : Fin n → α<GOAL>ofFn (Fin.append a b) = ofFn a ++ ofFn b
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : HasBinaryProduct X Y<GOAL>(pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd 0 0
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq (ι → ℕ)<VAR>s : Finset ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>f : ι → ℕ<GOAL>f ∈ SMul.smul n (s.piAntidiag m) ↔ f ∈ filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq (ι → ℕ)<VAR>s : Finset ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>f : ι → ℕ<GOAL>(∃ y ∈ s.piAntidiag m, n • y = f) ↔ f ∈ filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq (ι → ℕ)<VAR>s : Finset ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>f : ι → ℕ<GOAL>(∃ y, s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f) ↔ s.sum f = n * m ∧ (∀ (i : ι), f i ≠ 0 → i ∈ s) ∧ ∀ i ∈ s, n ∣ f i
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq (ι → ℕ)<VAR>s : Finset ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>f : ι → ℕ<VAR>hfsum : s.sum f = n * m<VAR>hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s<VAR>hfdvd : ∀ i ∈ s, n ∣ f i<VAR>this : ∀ (i : ι), n ∣ f i<GOAL>∑ i ∈ s, f i / n = m ∧ (∀ (i : ι), (fun i => f i / n) i ≠ 0 → i ∈ s) ∧ (n • fun i => f i / n) = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<GOAL>IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<VAR>h : ∀ s ≤ N, s.FG<VAR>s : Submodule R ↥N<GOAL>s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<VAR>h : ∀ s ≤ N, s.FG<VAR>s : Submodule R ↥N<VAR>f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s<GOAL>s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<VAR>h : ∀ s ≤ N, s.FG<VAR>s : Submodule R ↥N<VAR>f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s<VAR>h₁ : (Submodule.map N.subtype s).FG<GOAL>s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<VAR>h : ∀ s ≤ N, s.FG<VAR>s : Submodule R ↥N<VAR>f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s<VAR>h₁ : (Submodule.map N.subtype s).FG<VAR>h₂ : Submodule.map f ⊤ = ⊤<GOAL>s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R P<VAR>N : Submodule R M<VAR>h : ∀ s ≤ N, s.FG<VAR>s : Submodule R ↥N<VAR>f : ↥(Submodule.map N.subtype s) ≃ₗ[R] ↥s<VAR>h₁ : (Submodule.map N.subtype s).FG<VAR>h₂ : Submodule.map f ⊤ = ⊤<VAR>h₃ : (Submodule.map ↑f ⊤).FG<GOAL>s.FG
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hz : ∀ (i : ι), v i ≠ 0<VAR>ho : Pairwise fun i j => ⟪v i, v j⟫_𝕜 = 0<GOAL>LinearIndependent 𝕜 v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hz : ∀ (i : ι), v i ≠ 0<VAR>ho : Pairwise fun i j => ⟪v i, v j⟫_𝕜 = 0<GOAL>∀ (s : Finset ι) (g : ι → 𝕜), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t u v : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<GOAL>AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f✝ : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f✝ : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>0 < (Classical.choose ⋯).nnnorm
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : lowerCrossingTime a b f N (n + 1) ω ≠ N<GOAL>upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : lowerCrossingTime a b f N (n + 1) ω ≠ N<VAR>h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω<GOAL>b ≤ stoppedValue f (lowerCrossingTime a b f N (n + 1)) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : lowerCrossingTime a b f N (n + 1) ω ≠ N<VAR>h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω<GOAL>b ≤ f (upperCrossingTime a b f N (n + 1) ω) ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : DivisionSemiring α<VAR>inst✝ : Neg β<VAR>h : Antiperiodic f c<VAR>a : α<VAR>ha : a ≠ 0<GOAL>Antiperiodic (fun x => f (x * a)) (c / a)