ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<VAR>haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M<GOAL>eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<VAR>haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M<GOAL>(μ.restrict s) univ ^ p.toReal⁻¹ * ENNReal.ofReal M ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<VAR>haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M<GOAL>μ s ^ p.toReal⁻¹ ≤ ENNReal.ofReal ε / ENNReal.ofReal M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<VAR>haebdd : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ M<GOAL>ENNReal.ofReal M ≠ 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : λ ∣ x + 1<GOAL>λ ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : λ ∣ -x - 1<GOAL>λ ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : λ ∣ -x - 1<GOAL>x ^ 3 + 1 = -((-x) ^ 3 - 1)
<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<GOAL>Disjoint K Kᗮ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>I : InjectiveResolution Z<VAR>n : ℕ<GOAL>ExactAt I.cocomplex (n + 1)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>I : InjectiveResolution Z<VAR>n : ℕ<GOAL>QuasiIsoAt I.ι (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<GOAL>SurjOn f (Ico a b) (Ico (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : a < b<GOAL>SurjOn f (Ico a b) (Ico (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Surjective f<VAR>a b : α<VAR>hab : b ≤ a<GOAL>SurjOn f (Ico a b) (Ico (f a) (f b))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsConnected (⇑h ⁻¹' s) ↔ IsConnected s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>p : ι → Prop<VAR>l : Filter α<VAR>h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i<GOAL>l = ⨅ i, ⨅ (_ : p i), f i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>p : ι → Prop<VAR>l : Filter α<VAR>h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i<GOAL>l = ⨅ x, f ↑x
<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>f : MultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.succ<VAR>c : R<VAR>x : M 0<GOAL>f (cons (c • x) m) = c • f (cons x m)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : SeminormedAddCommGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>a : α<GOAL>‖s.indicator f a‖ ≤ ‖f a‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝ : SeminormedAddCommGroup E<VAR>s t : Set α<VAR>f : α → E<VAR>a : α<GOAL>s.indicator (fun a => ‖f a‖) a ≤ ‖f a‖
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>s : Set M<VAR>inst✝ : Fintype ↑s<GOAL>Module.rank R ↥(span R s) ≤ ↑s.toFinset.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a ≤ b⁻¹ ↔ b ≤ a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<VAR>α : Type u_3<VAR>φ : L.Formula α<VAR>v : α → ↥⊤<GOAL>φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<VAR>α : Type u_3<VAR>φ : L.Formula α<VAR>v : α → ↥⊤<GOAL>φ.Realize (⇑topEquiv ∘ v) ↔ φ.Realize (Subtype.val ∘ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>rlt : α → α → Prop<VAR>inst✝ : IsNonstrictStrictOrder α r rlt<GOAL>x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt x y → y ∉ s
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ✝ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>n m : σ✝<VAR>s : σ✝ →₀ ℕ<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S₁<VAR>p q : MvPolynomial σ✝ R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : IsEmpty σ<GOAL>Surjective ⇑C
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ✝ : Type u_1<VAR>a✝ a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>n m : σ✝<VAR>s : σ✝ →₀ ℕ<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ✝ R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : IsEmpty σ<VAR>p : MvPolynomial σ R<VAR>a : σ →₀ ℕ<GOAL>(C (p.toFun 0)) a = p a
<VAR>R✝ : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ✝ : Type u_1<VAR>a✝ a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>n m : σ✝<VAR>s : σ✝ →₀ ℕ<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ✝ R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : IsEmpty σ<VAR>p : MvPolynomial σ R<VAR>a : σ →₀ ℕ<GOAL>p.toFun 0 = p 0
<VAR>α : Type u_1<VAR>x✝ : Bool × ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(uncurry bit (b, n)).boddDiv2 = (b, n)
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>uncurry bit n.boddDiv2 = n
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<VAR>h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<VAR>h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2<GOAL>(x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<VAR>h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2<GOAL>x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<VAR>h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2<GOAL>x = 2 * m * n
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hzpos : 0 < z<VAR>m n : ℤ<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1<VAR>co : m.gcd n = 1<VAR>pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hz : z ≠ 0<VAR>h2 : y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2<GOAL>2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2) = ↑(2 * m * n) / ↑(m ^ 2 + n ^ 2)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Supermartingale f ℱ μ<GOAL>Supermartingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[(c • f) j|↑ℱ i] ≤ᶠ[ae μ] (c • f) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>c • μ[f j|↑ℱ i] ≤ᶠ[ae μ] (c • f) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝ : Ω<VAR>hle : (μ[f j|↑ℱ i]) a✝ ≤ f i a✝<GOAL>(c • μ[f j|↑ℱ i]) a✝ ≤ (c • f) i a✝
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁷ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>F : Type u_4<VAR>inst✝³ : NormedLatticeAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : OrderedSMul ℝ F<VAR>f : ι → Ω → F<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : Supermartingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝ : Ω<VAR>hle : (μ[f j|↑ℱ i]) a✝ ≤ f i a✝<GOAL>c • (μ[f j|↑ℱ i]) a✝ ≤ c • f i a✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ X : SimplicialObject C<VAR>X₀ : C<VAR>f : X _[0] ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<VAR>i j : SimplexCategoryᵒᵖ<VAR>g : i ⟶ j<GOAL>X.map g ≫ X.map ([0].const (unop j) 0).op ≫ f = (X.map ([0].const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ X : SimplicialObject C<VAR>X₀ : C<VAR>f : X _[0] ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<VAR>i j : SimplexCategoryᵒᵖ<VAR>g : i ⟶ j<GOAL>X.map g.unop.op ≫ X.map ([0].const (unop j) 0).op ≫ f = (X.map ([0].const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>b₁ : σ₁<VAR>ab : Reaches f₁ a₁ b₁<GOAL>∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₂ : σ₂<VAR>b₁ : σ₁<VAR>aa : tr b₁ a₂<VAR>ab : Reaches f₁ b₁ b₁<GOAL>∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>b₁ : σ₁<VAR>ab✝ : Reaches f₁ a₁ b₁<VAR>ab : TransGen (fun a b => b ∈ f₁ a) a₁ b₁<GOAL>∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>h : ‖f n‖ ≤ ‖g n‖<GOAL>‖term f s n‖ ≤ ‖term g s n‖
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>h : ‖f n‖ ≤ ‖g n‖<GOAL>(if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re) ≤ if n = 0 then 0 else ‖g n‖ / ↑n ^ s.re
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a : M<GOAL>z₁ * z₂ * a = z₂ * z₁ * a
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a : M<GOAL>z₂ * z₁ * a = z₂ * (z₁ * a)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a : M<GOAL>z₂ * (z₁ * a) = a * z₁ * z₂
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a : M<GOAL>a * z₁ * z₂ = a * (z₁ * z₂)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>b c : M<GOAL>z₁ * z₂ * (b * c) = z₁ * (z₂ * (b * c))
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>b c : M<GOAL>z₁ * (z₂ * (b * c)) = z₁ * (z₂ * b * c)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>b c : M<GOAL>z₁ * (z₂ * b * c) = z₁ * (z₂ * b) * c
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>b c : M<GOAL>z₁ * (z₂ * b) * c = z₁ * z₂ * b * c
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a c : M<GOAL>a * (z₁ * z₂) * c = a * z₁ * z₂ * c
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a c : M<GOAL>a * z₁ * z₂ * c = a * z₁ * (z₂ * c)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a c : M<GOAL>a * z₁ * (z₂ * c) = a * (z₁ * (z₂ * c))
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a c : M<GOAL>a * (z₁ * (z₂ * c)) = a * (z₁ * z₂ * c)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a b : M<GOAL>a * b * (z₁ * z₂) = a * b * z₁ * z₂
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a b : M<GOAL>a * b * z₁ * z₂ = a * (b * z₁) * z₂
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a b : M<GOAL>a * (b * z₁) * z₂ = a * (b * z₁ * z₂)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ center M<VAR>hz₂ : z₂ ∈ center M<VAR>a b : M<GOAL>a * (b * z₁ * z₂) = a * (b * (z₁ * z₂))
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝² : Semiring α✝<VAR>inst✝¹ : Semiring β<VAR>a b : α✝<VAR>m n : ℕ<VAR>α : Type u_5<VAR>inst✝ : Semiring α<VAR>x : α<GOAL>(x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>aux1 : ∀ (n : ℕ), ↑n = ↑n<VAR>aux2 : ∀ (p : R[X]), ↑p.natTrailingDegree = ↑p.natTrailingDegree<GOAL>(p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.trailingCoeff * q.trailingCoeff ≠ 0<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>aux1 : ∀ (n : ℕ), ↑n = ↑n<VAR>aux2 : ∀ (p : R[X]), ↑p.natTrailingDegree = ↑p.natTrailingDegree<GOAL>(p * q).trailingDegree = ↑(p.natTrailingDegree + q.natTrailingDegree)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>lift.{u, w} #↥((closure L).toFun s) ≤ max ℵ₀ (lift.{u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>lift.{max w u, w} #↥((closure L).toFun s) ≤ max ℵ₀ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>max ℵ₀ #(↑s ⊕ (i : ℕ) × L.Functions i) ≤ max ℵ₀ (lift.{max w u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>N : Type u_12<VAR>inst✝¹ : Monoid N<VAR>inst✝ : SMul M N<VAR>h : ∀ (x : M) (y : N), x • 1 * y = x • y<VAR>x : M<VAR>y z : N<GOAL>(x • y) • z = x • y • z
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed (C0 C ho)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed {f | f (term I ho) = false}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h : Continuous fun f => f (term I ho)<GOAL>IsClosed {f | f (term I ho) = false}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝² : (i : ι) → DecidableEq (γ i)<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → Zero (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x : (i : ι) → γ i<VAR>hf₁ : ∀ (i : ι), Injective (f i)<VAR>hf₂ : ∀ (i : ι), f i 0 = 0<GOAL>(hammingNorm fun i => f i (x i)) = hammingNorm x
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a * b⁻¹ < 1 ↔ a < b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝³ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : ∀ (i : ι), NoAtoms (μ i)<VAR>f g : (i : ι) → α i<GOAL>(univ.pi fun i => Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)
<VAR>n : ℤ<GOAL>cos (↑n * (2 * π) - π) = -1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R 2<VAR>x y : R<GOAL>x - y = x + y