ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s✝ t : Multiset α<VAR>a✝ : α<VAR>s : Multiset α<VAR>a : α<VAR>l : List α<VAR>this : l <+~ a :: l ∧ ¬l ~ a :: l<GOAL>Quot.mk Setoid.r l < a ::ₘ Quot.mk Setoid.r l
<VAR>L : Language<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>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>inst✝ : Nonempty M<VAR>P : {m : ℕ} → L.BoundedFormula α m → Prop<VAR>φ : L.BoundedFormula α n<VAR>hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ<VAR>hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀'ψ)<VAR>hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃'φ)<VAR>hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>P φ
<VAR>L : Language<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>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>inst✝ : Nonempty M<VAR>P : {m : ℕ} → L.BoundedFormula α m → Prop<VAR>φ : L.BoundedFormula α n<VAR>hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ<VAR>hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀'ψ)<VAR>hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃'φ)<VAR>hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)<GOAL>∀ {m : ℕ} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>this : -2 = ↑(-2)<GOAL>legendreSym p (-2) = χ₈' ↑p
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : WithBot ℕ<VAR>f : R[X]<GOAL>f ∈ degreeLE R n ↔ f.degree ≤ n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : WithBot ℕ<VAR>f : R[X]<GOAL>(∀ (i : ℕ), ↑i > n → (lcoeff R i) f = 0) ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>∫ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a = ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<GOAL>(fun x => F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x))) =ᶠ[ae (κ a)] fun x => F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f g : β × γ → E<VAR>F : E → E'<VAR>hf : Integrable f ((κ ⊗ₖ η) a)<VAR>hg : Integrable g ((κ ⊗ₖ η) a)<VAR>a✝ : β<VAR>h2f : Integrable (fun y => f (a✝, y)) (η (a, a✝))<VAR>h2g : Integrable (fun y => g (a✝, y)) (η (a, a✝))<GOAL>F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂η (a, a✝)) = F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂η (a, a✝))
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<GOAL>(zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<VAR>h : whiskerLeft F (zero F s i).inv = (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv<GOAL>(zero F s i).inv.app (F.obj X) = F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<GOAL>LiftProp P f ↔ Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae (μ.trim hm)] ↑↑f
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<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>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp F p (μ.trim hm))<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) =ᶠ[ae μ] ↑↑f
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>c : G<VAR>s t : Set α<GOAL>c • s ≤ᶠ[ae μ] c • t ↔ s ≤ᶠ[ae μ] t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<GOAL>essSup (fun x => ↑(c * ‖g x‖₊)) μ = essSup (fun x => ↑c * ↑‖g x‖₊) μ
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p : K[X]<VAR>hp : ¬p = 0<GOAL>(p * C p.leadingCoeff⁻¹).degree = p.degree
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<GOAL>atTop = comap Subtype.val atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<GOAL>(Independent fun i => t ↑i) ↔ Independent t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : Independent fun i => t ↑i<GOAL>Independent t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<GOAL>∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<VAR>i : ι<GOAL>Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<VAR>i : ι<VAR>hi : t i ≠ ⊥<GOAL>Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<VAR>i : ι<VAR>hi : t i ≠ ⊥<GOAL>⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<VAR>i : ι<VAR>hi : t i ≠ ⊥<VAR>this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥<GOAL>⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<VAR>h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)<VAR>i : ι<VAR>hi : t i ≠ ⊥<VAR>this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥<GOAL>(⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 = ⨆ i_1, ⨆ (h : t i_1 ≠ ⊥), ⨆ (_ : ⟨i_1, h⟩ ≠ ⟨i, hi⟩), t ↑⟨i_1, h⟩
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<GOAL>sSup ({x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x}) ≤ sSup ({x_1 | ∃ b_1, ∃ (_ : b_1 < b), f (lfpApprox f x b_1) = x_1} ∪ {x})
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<GOAL>{x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ∪ {x} ⊆ {x_1 | ∃ b_1, ∃ (_ : b_1 < b), f (lfpApprox f x b_1) = x_1} ∪ {x}
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<GOAL>{x_1 | ∃ b, ∃ (_ : b < a), f (lfpApprox f x b) = x_1} ≤ {x_1 | ∃ b_1, ∃ (_ : b_1 < b), f (lfpApprox f x b_1) = x_1}
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<GOAL>∀ a_1 < a, ∃ b_1 < b, f (lfpApprox f x b_1) = f (lfpApprox f x a_1)
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<VAR>a' : Ordinal.{u}<VAR>h' : a' < a<GOAL>∃ b_1 < b, f (lfpApprox f x b_1) = f (lfpApprox f x a')
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h : a ≤ b<VAR>a' : Ordinal.{u}<VAR>h' : a' < a<GOAL>a' < b ∧ f (lfpApprox f x a') = f (lfpApprox f x a')
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>HasSum (fun n => (cauchyPowerSeries f c R n) fun x => w) ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R : ℝ<VAR>w : ℂ<VAR>hf : CircleIntegrable f c R<VAR>hw : Complex.abs w < R<GOAL>HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>(r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>AEMeasurable ((r • ν).rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>AEMeasurable (r • ν.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ ν μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : ν.HaveLebesgueDecomposition μ<VAR>r : ℝ≥0<GOAL>∫⁻ (x : α), (r • ν).rnDeriv μ x ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : Fintype α<VAR>inst✝ : AddCommMonoid M<VAR>f : α →₀ M<GOAL>∑ a : α, single a (f a) = f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>(colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F (op i)).op).app A = limit.π (F.rightOp ⋙ yoneda.obj A) i
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b : R<VAR>hb : b ≠ 0<VAR>hab : b ∣ a<GOAL>b * (a / b) = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addRightEmbedding c) (Ioo a b) = Ioo (a + c) (b + c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addRightEmbedding c) '' Set.Ioo a b = Set.Ioo (a + c) (b + c)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s✝ t s : Set G<VAR>this : s ⊆ s * {1}<GOAL>s ⊆ s * closure {1}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>β : G.ComponentCompl K → Prop<VAR>f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)<GOAL>∀ (C : G.ComponentCompl K), β C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>β : G.ComponentCompl K → Prop<VAR>f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)<GOAL>∀ (v : ↑Kᶜ), β ((induce Kᶜ G).connectedComponentMk v)
<VAR>α : Type u_1<VAR>cut : α → Ordering<VAR>cmp : α → α → Ordering<VAR>f : α → α<VAR>t : RBNode α<VAR>h : Ordered cmp t<VAR>c✝ : RBColor<VAR>l✝ : RBNode α<VAR>v✝ : α<VAR>r✝ : RBNode α<VAR>x✝ : Path α<VAR>H : OnRoot (fun x => cmpEq cmp (f x) x) (node c✝ l✝ v✝ r✝, x✝).fst<VAR>eq : RBNode.zoom cut t = (node c✝ l✝ v✝ r✝, x✝)<GOAL>Path.RootOrdered cmp x✝ (f v✝) ∧ OnRoot (cmpEq cmp (f v✝)) (node c✝ l✝ v✝ r✝)
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R[ℕ]<GOAL>{ toFinsupp := a } = 1 ↔ a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : ↑n ≤ s.chainHeight<GOAL>∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : ↑n ≤ s.chainHeight<VAR>ha : ⨆ l, ↑(↑l).length = ⊤<GOAL>∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>n : ℕ<VAR>hn : ↑n ≤ s.chainHeight<VAR>ha : ⨆ l, ↑(↑l).length < ⊤<GOAL>∃ l ∈ s.subchain, l.length = n
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure α<VAR>t : Set α<VAR>a✝ : MeasurableSet t<GOAL>(Measure.comap f (Measure.map f μ)) t = μ t
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<GOAL>xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d a1 * yn a1 m * yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im<VAR>im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re<GOAL>xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d a1 * yn a1 m * yn a1 n
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : CG L M<VAR>f : M →[L] N<GOAL>f.range.CG
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>h : CG L M<VAR>f : M →[L] N<GOAL>(map f ⊤).CG
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>h : hζ.toInteger - 1 ∣ 2<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>h : hζ.toInteger - 1 ∣ 2<VAR>this : NumberField K<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K<VAR>h : hζ.toInteger - 1 ∣ ↑2<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K<VAR>h : ↑↑p ∣ 2<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K<VAR>h : hζ.toInteger - 1 ∣ ↑2<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>a : ℕ<VAR>ha0 : 0 < a<GOAL>(↑a)⁻¹.den = a
<VAR>a : ℕ<VAR>ha0 : 0 < a<GOAL>0 < ↑a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>hn : 1 < n<VAR>a : K<GOAL>X.natDegree < (X ^ n - C a).natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : IsNilpotent ((aeval x) P)<VAR>n : ℕ<GOAL>IsNilpotent (P.newtonMap^[n] x - x)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β✝<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s✝<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<VAR>s : Set γ<GOAL>s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β✝<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s✝<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<VAR>s : Set γ<GOAL>DirectedOn (g ⁻¹'o fun x x_1 => x ≥ x_1) f.sets
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β✝<VAR>ι : Sort u_6<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s✝<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<VAR>s : Set γ<GOAL>(∃ i ∈ f.sets, s ∈ g i) ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>I : Ideal R<VAR>hI : I ≠ ⊤<GOAL>I.closure ≠ ⊤
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>I : Ideal R<VAR>hI : I ≠ ⊤<VAR>h : closure ↑I ⊆ nonunits R<GOAL>I.closure ≠ ⊤
<VAR>α : Type u_1<VAR>hd : α<VAR>tl : List α<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl.get? ix = l'.get? (f ix)) → tl <+ l'<VAR>l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), (hd :: tl).get? ix = l'.get? (f ix)<VAR>this : some hd = l'.get? (f 0)<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl : List α<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl.get? ix = l'.get? (f ix)) → tl <+ l'<VAR>l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), (hd :: tl).get? ix = l'.get? (f ix)<VAR>this : ∃ (h : f 0 < l'.length), l'.get ⟨f 0, h⟩ = hd<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl : List α<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl.get? ix = l'.get? (f ix)) → tl <+ l'<VAR>l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), (hd :: tl).get? ix = l'.get? (f ix)<VAR>w : f 0 < l'.length<VAR>h : l'.get ⟨f 0, w⟩ = hd<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl : List α<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl.get? ix = l'.get? (f ix)) → tl <+ l'<VAR>l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), (hd :: tl).get? ix = l'.get? (f ix)<VAR>w : f 0 < l'.length<VAR>h : l'.get ⟨f 0, w⟩ = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl : List α<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl.get? ix = l'.get? (f ix)) → tl <+ l'<VAR>l' : List α<VAR>f : ℕ ↪o ℕ<VAR>hf : ∀ (ix : ℕ), (hd :: tl).get? ix = l'.get? (f ix)<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<GOAL>hd :: tl <+ l'
<VAR>α : Type u_1<VAR>hd : α<VAR>tl l' : List α<VAR>f : ℕ ↪o ℕ<VAR>w : f 0 < l'.length<VAR>h : l'[f 0] = hd<VAR>f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) ⋯<VAR>hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?<VAR>IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'<GOAL>hd :: tl <+ l'