ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f g : α → β<VAR>m m' : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>hf : StronglyMeasurable f<VAR>h_mono : m' ≤ m<VAR>f_approx : ℕ → α →ₛ β := fun n => { toFun := ↑(hf.approx n), measurableSet_fiber' := ⋯, finite_range' := ⋯ }<GOAL>StronglyMeasurable f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : MulAction A M<VAR>inst✝ : SMul R M<VAR>h : ∀ (r : R) (x : M), (algebraMap R A) r • x = r • x<VAR>r : R<VAR>a : A<VAR>x : M<GOAL>(r • a) • x = r • a • x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<GOAL>Submonoid.map (RingEquiv.refl R).toMonoidHom S = S
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L✝ L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>L : G ≃L[𝕜] G'<VAR>f : E → F →L[𝕜] G<VAR>x : E<GOAL>fderiv 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<GOAL>ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<GOAL>ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<VAR>this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)<GOAL>ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<VAR>this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)<GOAL>ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<VAR>this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)<GOAL>∫⁻ (x : X), ENNReal.ofReal (g x) ∂μ ≤ μ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<VAR>this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)<GOAL>∀ (a : X), ENNReal.ofReal (g a) ≤ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>f✝ : X → ℝ<VAR>s✝ : Set X<VAR>f : X → ℝ<VAR>s : Set X<VAR>hs : ∀ x ∈ s, f x ≤ 1<VAR>h's : ∀ x ∈ sᶜ, f x ≤ 0<VAR>H : Integrable f μ<VAR>g : X → ℝ := fun x => max (f x) 0<VAR>g_int : Integrable g μ<VAR>this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)<GOAL>∀ a ∈ sᶜ, ENNReal.ofReal (g a) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Mem.other' h ∈ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Mem.other h ∈ z
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝ : Fintype V<VAR>v : V<GOAL>⊥.degree v = 0
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝ : Fintype V<VAR>v : V<GOAL>∅.card = 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Matrix V V α<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<GOAL>¬A i j = 1 ↔ A i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDF f κ ν<VAR>a : α<GOAL>∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>f : i ⟶ j<VAR>g : j ⟶ k<VAR>h : F.eventualRange k = range (F.map g)<GOAL>F.eventualRange k = range (F.map (f ≫ g))
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>f : i ⟶ j<VAR>g : j ⟶ k<VAR>h : F.eventualRange k = range (F.map g)<GOAL>F.eventualRange k ⊆ range (F.map (f ≫ g))
<VAR>J : Type u<VAR>inst✝ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>f : i ⟶ j<VAR>g : j ⟶ k<VAR>h : F.eventualRange k = range (F.map g)<GOAL>range (F.map (f ≫ g)) ⊆ F.eventualRange k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : Semiring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : LinearOrderedField k<VAR>f : R →+* S<VAR>abv : S → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>p : R[X]<VAR>hd : 0 < p.degree<VAR>l : Filter α<VAR>z : α → S<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : Semiring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : LinearOrderedField k<VAR>f : R →+* S<VAR>abv : S → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>l : Filter α<VAR>z : α → S<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>∀ {a : R}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (C a * X))) l atTop
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : Semiring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : LinearOrderedField k<VAR>f : R →+* S<VAR>abv : S → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>l : Filter α<VAR>z : α → S<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>∀ {p : R[X]}, 0 < p.degree → (f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) → f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>k : Type u_3<VAR>α : Type u_4<VAR>inst✝³ : Semiring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : LinearOrderedField k<VAR>f : R →+* S<VAR>abv : S → k<VAR>inst✝ : IsAbsoluteValue abv<VAR>l : Filter α<VAR>z : α → S<VAR>hz : Tendsto (abv ∘ z) l atTop<GOAL>∀ {p : R[X]} {a : R}, 0 < p.degree → (f p.leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) → f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + C a))) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>↑↑((condexpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condexpIndSMul hm hs hμs x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>↑↑((condexpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condexpIndL1Fin hm hs hμs x)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>r : R<GOAL>r ∈ v.integer ↔ v r ≤ 1
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : LocallyCompactSpace Y<GOAL>Continuous uncurry
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : LocallyCompactSpace Y<GOAL>Continuous (Function.uncurry fun x y => x.uncurry y)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : LocallyCompactSpace Y<GOAL>Continuous ((Function.uncurry fun x y => x.uncurry y) ∘ ⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithTop α<VAR>h : a ≠ 0<GOAL>a * ⊤ = ⊤
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ a b : α<GOAL>a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N P Q : Bimod Y Z<VAR>f : N ⟶ P<VAR>g : P ⟶ Q<GOAL>(M.whiskerLeft (f ≫ g)).hom = (M.whiskerLeft f ≫ M.whiskerLeft g).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N P Q : Bimod Y Z<VAR>f : N ⟶ P<VAR>g : P ⟶ Q<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (f ≫ g)).hom = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft f ≫ M.whiskerLeft g).hom
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<GOAL>∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>hab : b < a<GOAL>∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
<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✝ ht : Independent t<VAR>i : ι<VAR>a✝ : i ∈ {i | t i ≠ ⊥}<VAR>j : ι<VAR>hj : t j ≠ ⊥<VAR>h : t i = t j<GOAL>i = 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✝ ht : Independent t<VAR>i : ι<VAR>a✝ : i ∈ {i | t i ≠ ⊥}<VAR>j : ι<VAR>hj : t j ≠ ⊥<VAR>h : t i = t j<VAR>contra : i ≠ j<GOAL>False
<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✝ ht : Independent t<VAR>i : ι<VAR>a✝ : i ∈ {i | t i ≠ ⊥}<VAR>j : ι<VAR>hj : t j ≠ ⊥<VAR>h : t i = t j<VAR>contra : i ≠ j<GOAL>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✝ ht : Independent t<VAR>i : ι<VAR>a✝ : i ∈ {i | t i ≠ ⊥}<VAR>j : ι<VAR>hj : t j ≠ ⊥<VAR>h : t i = t j<VAR>contra : i ≠ j<GOAL>t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
<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✝ ht : Independent t<VAR>i : ι<VAR>a✝ : i ∈ {i | t i ≠ ⊥}<VAR>j : ι<VAR>hj : t j ≠ ⊥<VAR>h : t i = t j<VAR>contra : j ≠ i<GOAL>t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>s : Finset L<VAR>this : DecidableEq L<GOAL>∃ y, y ≠ 0 ∧ ∀ x ∈ s, IsIntegral A (y • x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>s : Finset L<VAR>this : DecidableEq L<GOAL>∃ y, y ≠ 0 ∧ ∀ x ∈ ∅, IsIntegral A (y • x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : IsDomain A<VAR>inst✝¹¹ : Algebra A K<VAR>inst✝¹⁰ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝⁹ : Field L<VAR>C : Type u_5<VAR>inst✝⁸ : CommRing C<VAR>inst✝⁷ : Algebra K L<VAR>inst✝⁶ : Algebra A L<VAR>inst✝⁵ : IsScalarTower A K L<VAR>inst✝⁴ : Algebra C L<VAR>inst✝³ : IsIntegralClosure C A L<VAR>inst✝² : Algebra A C<VAR>inst✝¹ : IsScalarTower A C L<VAR>inst✝ : FiniteDimensional K L<VAR>s : Finset L<VAR>this : DecidableEq L<GOAL>∀ ⦃a : L⦄ {s : Finset L}, a ∉ s → (∃ y, y ≠ 0 ∧ ∀ x ∈ s, IsIntegral A (y • x)) → ∃ y, y ≠ 0 ∧ ∀ x ∈ insert a s, IsIntegral A (y • x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<VAR>h₁ : s ≤ u<VAR>h₂ : t ≤ u<GOAL>s ∪ t ≤ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<VAR>h₁ : s ≤ u<VAR>h₂ : t ≤ u<GOAL>s ∪ t ≤ u ∪ t
<VAR>α : Type u_1<VAR>I : Type u_2<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = finrank k ↥sp.direction + 1<GOAL>affineSpan k ↑(Finset.image p s) = sp
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = finrank k ↥sp.direction + 1<VAR>hn : s.Nonempty<GOAL>affineSpan k ↑(Finset.image p s) = sp
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = finrank k ↥sp.direction + 1<VAR>hn : s.Nonempty<GOAL>(affineSpan k ↑(Finset.image p s)).direction = sp.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = finrank k ↥sp.direction + 1<VAR>hn : s.Nonempty<VAR>hd : (affineSpan k ↑(Finset.image p s)).direction ≤ sp.direction<GOAL>(affineSpan k ↑(Finset.image p s)).direction = sp.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : DivisionRing k<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module k V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DecidableEq P<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>s : Finset ι<VAR>sp : AffineSubspace k P<VAR>inst✝ : FiniteDimensional k ↥sp.direction<VAR>hle : affineSpan k ↑(Finset.image p s) ≤ sp<VAR>hc : s.card = finrank k ↥sp.direction + 1<VAR>hn : s.Nonempty<VAR>hd : vectorSpan k ↑(Finset.image p s) ≤ sp.direction<GOAL>vectorSpan k ↑(Finset.image p s) = sp.direction
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<GOAL>HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<VAR>sum_L2 : HasSum (fun i => fourierCoeff (↑↑((toLp 2 haarAddCircle ℂ) f)) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)<GOAL>HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<VAR>sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)<GOAL>HasSum (fun i => fourierCoeff (⇑f) i • fourier i) f
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<VAR>sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)<GOAL>Summable fun a => ‖fourierCoeff (⇑f) a • fourier a‖
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>f : C(AddCircle T, ℂ)<VAR>h : Summable (fourierCoeff ⇑f)<VAR>sum_L2 : HasSum (fun i => fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)<GOAL>Summable fun a => ‖fourierCoeff (⇑f) a‖
<VAR>x y : ℝ<GOAL>cosh |x| = cosh x
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra S A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : IsScalarTower R S A<VAR>s✝ t : Set A<VAR>inst✝ : DecidableEq A<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : { x // x ∈ s } → Finset A<GOAL>adjoin R ↑(s.attach.biUnion f) = ⨆ x, adjoin R ↑(f x)
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π : TaggedPrepartition I<VAR>x : ι → ℝ<GOAL>x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π : TaggedPrepartition I<VAR>x : ι → ℝ<VAR>x✝ : Box ι<GOAL>x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π.toPrepartition), x ∈ ↑x✝
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>truncateFun n (x - y) = truncateFun n x - truncateFun n y
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝¹ : Monoid N✝<VAR>N : Type u_4<VAR>inst✝ : Monoid N<VAR>f : (i : ι) → M i →* N<GOAL>MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝¹ : Monoid N✝<VAR>N : Type u_4<VAR>inst✝ : Monoid N<VAR>f : (i : ι) → M i →* N<GOAL>⨆ i, Submonoid.closure (range fun b => (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → Σˣ f<VAR>i j : ι<VAR>hi : i ∈ upperBounds (range (Sigma.fst ∘ x))<VAR>hj : j ∈ upperBounds (range (Sigma.fst ∘ x))<VAR>k : ι<VAR>ik : i ≤ k<VAR>jk : j ≤ k<GOAL>RelMap R (unify f x i hi) = RelMap R (unify f x j hj)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>a : α<GOAL>erase a (erase a f) = erase a f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>(p • 1 + q • (mk W) Y) * (mk W) Y = (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 + (p - q * (C W.a₁ * X + C W.a₃)) • (mk W) Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<VAR>Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)<GOAL>(p • 1 + q • (mk W) Y) * (mk W) Y = (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 + (p - q * (C W.a₁ * X + C W.a₃)) • (mk W) Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<VAR>Y_sq : (mk W) Y ^ 2 = (mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - C (C W.a₁ * X + C W.a₃) * Y)<GOAL>(mk W) (C p) * (1 * (mk W) Y) + (mk W) (C q) * ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) - (mk W) (C (C W.a₁ * X + C W.a₃)) * (mk W) Y) = (mk W) (C q) * ((mk W) (C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * 1) + ((mk W) (C p) - (mk W) (C q) * (mk W) (C (C W.a₁ * X + C W.a₃))) * (mk W) Y
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>n : ℕ<GOAL>(lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}