ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha✝ : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<VAR>ha : (z - y) / (z - x) = a<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)<VAR>x : 𝕜<VAR>hx : x ∈ s<VAR>z : 𝕜<VAR>hz : z ∈ s<VAR>hxz✝ : x < z<VAR>a b : 𝕜<VAR>ha✝ : 0 < a<VAR>hb✝ : 0 < b<VAR>hab : a + b = 1<VAR>y : 𝕜 := a * x + b * z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)<VAR>hxz : 0 < z - x<VAR>ha : (z - y) / (z - x) = a<VAR>hb : (y - x) / (z - x) = b<GOAL>f (a • x + b • z) ≤ a • f x + b • f z
<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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>hf : IsLocalHomeomorph f<GOAL>IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}
<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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>hf : IsLocalHomeomorph f<GOAL>∀ u ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, IsOpen u
<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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>hf : IsLocalHomeomorph f<VAR>x : X<VAR>U : Set X<VAR>hx : x ∈ U<VAR>hU : IsOpen U<GOAL>∃ v ∈ {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}, x ∈ v ∧ v ⊆ U
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ<VAR>hp : 0 ≤ p<VAR>n : ℕ<GOAL>ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<VAR>this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<VAR>this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)<VAR>ht : MeasurableSet t<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<VAR>this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)<VAR>ht : MeasurableSet t<VAR>h2t : ((κ ⊗ₖ η) a) t ≠ ⊤<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<VAR>this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)<VAR>ht : MeasurableSet t<VAR>h2t : ((κ ⊗ₖ η) a) t ≠ ⊤<VAR>ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤<GOAL>∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<VAR>this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)<VAR>ht : MeasurableSet t<VAR>h2t : ((κ ⊗ₖ η) a) t ≠ ⊤<VAR>ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤<VAR>b : β<VAR>hb : (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤<GOAL>(η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>f : P ⟶ Q<VAR>x : FamilyOfElements P R<VAR>h : x.Compatible<VAR>Z₁ Z₂ W : C<VAR>g₁ : W ⟶ Z₁<VAR>g₂ : W ⟶ Z₂<VAR>f₁ : Z₁ ⟶ X<VAR>f₂ : Z₂ ⟶ X<VAR>h₁ : R f₁<VAR>h₂ : R f₂<VAR>eq : g₁ ≫ f₁ = g₂ ≫ f₂<GOAL>Q.map g₁.op (f.app (op Z₁) (x f₁ h₁)) = Q.map g₂.op (f.app (op Z₂) (x f₂ h₂))
<VAR>α✝ : Type u_1<VAR>inst✝³ : DecidableEq α✝<VAR>inst✝² : Fintype α✝<VAR>α : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>card ↑(derangements α) = numDerangements (card α)
<VAR>α✝ : Type u_1<VAR>inst✝³ : DecidableEq α✝<VAR>inst✝² : Fintype α✝<VAR>α : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>card ↑(derangements (Fin (card α))) = numDerangements (card α)
<VAR>V W : SemiNormedGrp<VAR>i : V ≅ W<VAR>h1 : NormedAddGroupHom.NormNoninc i.hom<VAR>h2 : NormedAddGroupHom.NormNoninc i.inv<VAR>v : ↑V<GOAL>‖i.hom v‖ = ‖v‖
<VAR>V W : SemiNormedGrp<VAR>i : V ≅ W<VAR>h1 : NormedAddGroupHom.NormNoninc i.hom<VAR>h2 : NormedAddGroupHom.NormNoninc i.inv<VAR>v : ↑V<GOAL>‖v‖ ≤ ‖i.hom v‖
<VAR>b m n : ℕ<VAR>h₁ : b ^ m ≤ n<VAR>h₂ : n < b ^ (m + 1)<GOAL>log b n = m
<VAR>b n : ℕ<VAR>h₁ : b ^ 0 ≤ n<VAR>h₂ : n < b ^ (0 + 1)<GOAL>log b n = 0
<VAR>b m n : ℕ<VAR>h₁ : b ^ m ≤ n<VAR>h₂ : n < b ^ (m + 1)<VAR>hm : m ≠ 0<GOAL>log b n = m
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<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✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>0 < Module.rank R M ↔ ∃ x, x ≠ 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<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✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>¬0 < Module.rank R M ↔ ¬∃ x, x ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < r i n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>hf : Function.Injective ⇑f<GOAL>comap f ⊥ ≤ I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>hf : Function.Injective ⇑f<VAR>x : R<VAR>hx : x ∈ comap f ⊥<GOAL>x ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>ι : Sort u_3<VAR>hf : Function.Injective ⇑f<VAR>x : R<VAR>hx : f x = f 0<GOAL>x ∈ ⊥
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>z w : E<VAR>g : ℂ → F := f ∘ fun t => t • (w - z) + z<GOAL>g 0 = g 1
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>z w : E<VAR>g : ℂ → F := f ∘ fun t => t • (w - z) + z<GOAL>Differentiable ℂ g
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>hb : Bornology.IsBounded (range f)<VAR>z w : E<VAR>g : ℂ → F := f ∘ fun t => t • (w - z) + z<GOAL>Bornology.IsBounded (range g)
<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✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂<VAR>m : M 0<VAR>x : (i : Fin n) → M i.succ<GOAL>(f.uncurryLeft.curryLeft m) x = (f m) 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✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>f : M 0 →ₗ[R] MultilinearMap R (fun i => M i.succ) M₂<VAR>m : M 0<VAR>x : (i : Fin n) → M i.succ<GOAL>(f (cons m x 0)) x = (f m) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : Ring α<VAR>h : Periodic f c<VAR>n : ℤ<GOAL>Periodic f (↑n * c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 1<GOAL>∏' (b : β), f b = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>f : β → α<VAR>b : β<VAR>hf : ∀ (b' : β), b' ≠ b → f b' = 1<GOAL>∀ b_1 ∉ {b}, f b_1 = 1
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ<VAR>hl : ∀ i ∈ l, 0 ≤ f i<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ<VAR>hl : ∀ i ∈ l, 0 ≤ f i<VAR>r : ℝ<GOAL>(List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>l : List ι<VAR>f : ι → ℝ<VAR>hl : ∀ i ∈ l, 0 ≤ f i<VAR>r : ℝ<GOAL>∀ x ∈ List.map f l, 0 ≤ 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✝ : Semiring R<VAR>c : R<GOAL>derivative (X + C c) = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<VAR>l : List α<VAR>hl : ∀ x ∈ ⟦l⟧, 1 ≤ x<GOAL>1 ≤ prod ⟦l⟧
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddZeroClass G<VAR>f : k[G]<GOAL>f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<GOAL>f.ker.index = Nat.card ↑(Set.range ⇑f)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G →* G'<GOAL>Nat.card ↥f.range = Nat.card ↑(Set.range ⇑f)
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝² : AddGroup A<VAR>inst✝¹ : Ring R<VAR>α : Type u_3<VAR>inst✝ : Group α<VAR>a : α<GOAL>(↑(zpowers a)).Finite ↔ IsOfFinOrder a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<GOAL>(x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔ (x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : (x :: y :: l).formPerm = (x' :: y' :: l').formPerm<GOAL>(x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<GOAL>(x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<GOAL>(x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<VAR>n : ℕ<VAR>hn : n < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨n, hn⟩ = x'<GOAL>(x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<VAR>n : ℕ<VAR>hn : n < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨n, hn⟩ = x'<VAR>hl : (x :: y :: l).length = (x' :: y' :: l').length<GOAL>(x :: y :: l) ~r (x' :: y' :: l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<VAR>n : ℕ<VAR>hn : n < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨n, hn⟩ = x'<VAR>hl : (x :: y :: l).length = (x' :: y' :: l').length<GOAL>(x :: y :: l).rotate n = x' :: y' :: l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<VAR>n : ℕ<VAR>hn : n < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨n, hn⟩ = x'<VAR>hl : (x :: y :: l).length = (x' :: y' :: l').length<GOAL>((x :: y :: l).rotate n).length = (x' :: y' :: l').length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ x y x' y' : α<VAR>l l' : List α<VAR>hd : (x :: y :: l).Nodup<VAR>hd' : (x' :: y' :: l').Nodup<VAR>h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1<VAR>hx : x' ∈ x :: y :: l<VAR>n : ℕ<VAR>hn : n < (x :: y :: l).length<VAR>hx' : (x :: y :: l).get ⟨n, hn⟩ = x'<VAR>hl : (x :: y :: l).length = (x' :: y' :: l').length<GOAL>∀ (n_1 : ℕ) (h₁ : n_1 < ((x :: y :: l).rotate n).length) (h₂ : n_1 < (x' :: y' :: l').length), ((x :: y :: l).rotate n).get ⟨n_1, h₁⟩ = (x' :: y' :: l').get ⟨n_1, h₂⟩
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<GOAL>((map f) p).vars ⊆ p.vars
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x : m α<VAR>g : β → m γ<VAR>f : α → β<GOAL>f <$> x >>= g = x >>= g ∘ f
<VAR>α β γ : Type u<VAR>m : Type u → Type v<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>x : m α<VAR>g : β → m γ<VAR>f : α → β<GOAL>(x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[c • f|m] =ᶠ[ae μ] c • μ[f|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>↑↑(condexpL1 hm μ (c • f)) =ᶠ[ae μ] c • μ[f|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>↑↑(c • condexpL1 hm μ f) =ᶠ[ae μ] c • μ[f|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>∀ᵐ (x : α) ∂μ, (μ[f|m]) x = ↑↑(condexpL1 hm μ f) x → ↑↑(c • condexpL1 hm μ f) x = (c • μ[f|m]) x
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>c : 𝕜<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<VAR>x : α<VAR>hx1 : ↑↑(c • condexpL1 hm μ f) x = (c • ↑↑(condexpL1 hm μ f)) x<VAR>hx2 : (μ[f|m]) x = ↑↑(condexpL1 hm μ f) x<GOAL>↑↑(c • condexpL1 hm μ f) x = (c • μ[f|m]) x
<VAR>m n a b c d : ℕ<GOAL>a ≡ 0 [MOD n] ↔ n ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : TopologicalSpace γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : PseudoMetrizableSpace β<VAR>inst✝⁴ : BorelSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : PseudoMetrizableSpace γ<VAR>inst✝¹ : OpensMeasurableSpace γ<VAR>inst✝ : SecondCountableTopology γ<VAR>g : β → γ<VAR>hg : Measurable g<VAR>f : α →ₘ[μ] β<GOAL>compMeasurable g hg f = mk (g ∘ ↑f) ⋯
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>j : Fin n<GOAL>i.insertNth x p (i.succAbove j) = p j
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>j : Fin n<GOAL>(if h : j.castSucc < i then ⋯ ▸ p ((i.succAbove j).castPred ⋯) else ⋯ ▸ p ((i.succAbove j).pred ⋯)) = p j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>inst✝ : OrderTopology β<VAR>huv : u ~[l] v<VAR>hu : Tendsto u l atBot<GOAL>Tendsto v l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : NormedLinearOrderedField β<VAR>u v : α → β<VAR>l : Filter α<VAR>inst✝ : OrderTopology β<VAR>huv : u ~[l] v<VAR>hu : Tendsto u l atBot<GOAL>v = Neg.neg ∘ fun x => -v x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderTopology G<VAR>l : Filter α<VAR>f✝ g f : α → G<GOAL>Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderTopology G<VAR>l : Filter α<VAR>f✝ g f : α → G<VAR>h : Tendsto (abs ∘ f) l (𝓝 0)<GOAL>Tendsto f l (𝓝 0)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : OrderTopology G<VAR>l : Filter α<VAR>f✝ g f : α → G<VAR>h : Tendsto (abs ∘ f) l (𝓝 0)<VAR>this : Tendsto (fun a => -|f a|) l (𝓝 0)<GOAL>Tendsto f l (𝓝 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<GOAL>support R M ⊆ support R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<GOAL>∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0