ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝² : CommSemiring S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R S<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>Z : Set (PrimeSpectrum S)<GOAL>(∃ s, zeroLocus s = Z) ↔ ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<GOAL>integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<VAR>hf' : f.FinMeasSupp μ<GOAL>integral μ (map (ENNReal.toReal ∘ g) f) = (∫⁻ (a : α), g (↑f a) ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<VAR>hf' : f.FinMeasSupp μ<GOAL>integral μ (map (ENNReal.toReal ∘ g) f) = ((map g f).lintegral μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<VAR>hf' : f.FinMeasSupp μ<GOAL>∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • (ENNReal.toReal ∘ g) x = ∑ a ∈ f.range, (g a * μ (↑f ⁻¹' {a})).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<VAR>hf' : f.FinMeasSupp μ<GOAL>∀ a ∈ f.range, g a * μ (↑f ⁻¹' {a}) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ E<VAR>g : E → ℝ≥0∞<VAR>hf : Integrable (↑f) μ<VAR>hg0 : g 0 = 0<VAR>ht : ∀ (b : E), g b ≠ ⊤<VAR>hf' : f.FinMeasSupp μ<GOAL>(ENNReal.toReal ∘ g) 0 = 0
<VAR>a b : ℕ<VAR>ha : a % 4 = 1<VAR>hb : Odd b<GOAL>J(↑a | b) = J(↑b | a)
<VAR>x y : ℤ[i]<GOAL>(toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)
<VAR>x y : ℤ[i]<GOAL>(toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round ↑(↑(x * star y).im / ↑(norm y)) }).im = ↑(round (toComplex x / toComplex y).im)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : Injective fa<VAR>hf : InjOn f (range fa)<GOAL>InjOn fb (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : Injective fa<VAR>hf : InjOn f (fa '' univ)<GOAL>InjOn fb (f '' univ)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>α₁ α₂ : Ext X Y n<VAR>m : ℕ<VAR>β : Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>((α₁ + α₂).comp β h).hom = (α₁.comp β h + α₂.comp β h).hom
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x✝ : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>x : ι<VAR>y : α x<GOAL>⟨x, y⟩ ∈ s₁.sigma t₁ ∩ s₂.sigma t₂ ↔ ⟨x, y⟩ ∈ (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddCommGroup H<VAR>a : G<VAR>b : H<VAR>f : G →+c[a, b] H<VAR>x✝ : G<GOAL>(fun x => -f (-x)) (x✝ + a) = (fun x => -f (-x)) x✝ + b
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g g' : F[X]<VAR>m m' : ℕ<VAR>h_expand : (expand F (q ^ m)) g = (expand F (q ^ m')) g'<VAR>hg : g.Separable<VAR>hg' : g'.Separable<VAR>hm : m ≤ m'<GOAL>g.natDegree = g'.natDegree
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g g' : F[X]<VAR>m : ℕ<VAR>hg : g.Separable<VAR>hg' : g'.Separable<VAR>s : ℕ<VAR>h_expand : (expand F (q ^ m)) g = (expand F (q ^ (m + s))) g'<VAR>hm : m ≤ m + s<GOAL>g.natDegree = g'.natDegree
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g g' : F[X]<VAR>m : ℕ<VAR>hg : g.Separable<VAR>hg' : g'.Separable<VAR>s : ℕ<VAR>h_expand : g = (expand F (q ^ s)) g'<VAR>hm : m ≤ m + s<GOAL>g.natDegree = g'.natDegree
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g' : F[X]<VAR>m : ℕ<VAR>hg' : g'.Separable<VAR>s : ℕ<VAR>hm : m ≤ m + s<VAR>hg : ((expand F (q ^ s)) g').Separable<GOAL>((expand F (q ^ s)) g').natDegree = g'.natDegree
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g' : F[X]<VAR>m : ℕ<VAR>hg' : g'.Separable<VAR>s : ℕ<VAR>hm : m ≤ m + s<VAR>hg : ((expand F (q ^ s)) g').Separable<VAR>h : IsUnit g'<GOAL>((expand F (q ^ s)) g').natDegree = g'.natDegree
<VAR>F✝ : Type u_1<VAR>inst✝² : Field F✝<VAR>q✝ : ℕ<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>q : ℕ<VAR>f : F[X]<VAR>hf : HasSeparableContraction q f<VAR>hq : NeZero q<VAR>inst✝ : CharP F q<VAR>g' : F[X]<VAR>m : ℕ<VAR>hg' : g'.Separable<VAR>hm : m ≤ m + 0<VAR>hg : ((expand F (q ^ 0)) g').Separable<GOAL>((expand F (q ^ 0)) g').natDegree = g'.natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>Multiset.count a (toMultiset f) = f.sum fun x n => Multiset.count a (n • {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>Multiset.count a (f.sum fun a n => n • {a}) = f.sum fun x n => Multiset.count a (n • {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>(f.sum fun x n => Multiset.count a (n • {x})) = f.sum fun x n => n * Multiset.count a {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a a' : α<VAR>x✝ : f a' ≠ 0<VAR>H : a' ≠ a<GOAL>f a' * Multiset.count a {a'} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ ℕ<VAR>a : α<GOAL>f a * Multiset.count a {a} = f a
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>inst✝⁷ : Field 𝕜<VAR>inst✝⁶ : CharZero 𝕜<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Algebra 𝕜 R<VAR>inst✝³ : UniformSpace R<VAR>inst✝² : TopologicalRing R<VAR>inst✝¹ : CompleteSpace R<VAR>inst✝ : T2Space R<VAR>r : R<GOAL>exp 𝕜 (r • ε) = 1 + r • ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>LiftRel R s.think t ↔ LiftRel R s t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
<VAR>α β✝ γ✝ : Type u<VAR>S S' : Set (α → ℕ)<VAR>β : Type u<VAR>p : Poly (α ⊕ β)<VAR>pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>γ : Type u<VAR>q : Poly (α ⊕ γ)<VAR>qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, q (v ⊗ t) = 0<VAR>v : α → ℕ<GOAL>(S ∪ S') v ↔ ∃ t, (Poly.map (inl ⊗ inr ∘ inl) p * Poly.map (inl ⊗ inr ∘ inr) q) (v ⊗ t) = 0
<VAR>α β✝ γ✝ : Type u<VAR>S S' : Set (α → ℕ)<VAR>β : Type u<VAR>p : Poly (α ⊕ β)<VAR>pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>γ : Type u<VAR>q : Poly (α ⊕ γ)<VAR>qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, q (v ⊗ t) = 0<VAR>v : α → ℕ<GOAL>(∃ t, p (v ⊗ t) = 0) ↔ ∃ x, p ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) = 0
<VAR>α β✝ γ✝ : Type u<VAR>S S' : Set (α → ℕ)<VAR>β : Type u<VAR>p : Poly (α ⊕ β)<VAR>pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0<VAR>γ : Type u<VAR>q : Poly (α ⊕ γ)<VAR>qe : ∀ (v : α → ℕ), S' v ↔ ∃ t, q (v ⊗ t) = 0<VAR>v : α → ℕ<GOAL>(∃ t, q (v ⊗ t) = 0) ↔ ∃ x, q ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a : R[X]<GOAL>p.scaleRoots r ∣ (p * a).scaleRoots r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a : R[X]<GOAL>p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : IsDomain α<VAR>x y : α<GOAL>span {x} < span {y} ↔ DvdNotUnit y x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n✝ m✝ n : ℤ<VAR>f : F ⟶ G<VAR>z : Cochain G K n<VAR>m : ℤ<GOAL>δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ γ : Path x y<VAR>t : ↑I<GOAL>γ (σ (σ t)) = γ t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<GOAL>(map Prod.swap ρ).snd = ρ.fst
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<GOAL>map (Prod.snd ∘ Prod.swap) ρ = ρ.fst
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 l)<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 l)<VAR>h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc✝ : ContinuousOn f (Ioo a b)<VAR>ha : Tendsto f (𝓝[>] a) (𝓝 l)<VAR>hb : Tendsto f (𝓝[<] b) (𝓝 l)<VAR>h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)<VAR>c : X<VAR>hc : c ∈ Ioo a b<VAR>hfc : IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>k : ℕ<VAR>x : L<GOAL>((toEnd R L M₂) x ^ k) ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x ^ k
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>k : ℕ<VAR>x : L<GOAL>(toEnd R L M₂) x ∘ₗ ↑f = ↑f ∘ₗ (toEnd R L M) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<GOAL>↑⌊a⌋ + ↑⌊b⌋ ≤ a + b
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>l : List α<GOAL>(map Prod.fst l.enum).Nodup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<GOAL>(p.bindOnSupport f).bindOnSupport g = p.bindOnSupport fun a ha => (f a ha).bindOnSupport fun b hb => g b ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<VAR>a : γ<GOAL>((p.bindOnSupport f).bindOnSupport g) a = (p.bindOnSupport fun a ha => (f a ha).bindOnSupport fun b hb => g b ⋯) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<VAR>a : γ<GOAL>(∑' (a_1 : β), (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) * if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) = ∑' (a_1 : α), p a_1 * if h : p a_1 = 0 then 0 else ∑' (a_2 : β), (f a_1 h) a_2 * if h : (f a_1 h) a_2 = 0 then 0 else (g a_2 ⋯) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<VAR>a : γ<GOAL>(∑' (a_1 : β) (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) * if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) = ∑' (a_1 : α) (i : β), p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<VAR>a : γ<GOAL>(∑' (a_1 : β) (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) * if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) = 0 then 0 else (g a_1 ⋯) a) = ∑' (a_1 : α) (i : β), p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : (a : α) → a ∈ p.support → PMF β<VAR>g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ<VAR>a : γ<VAR>a' : α<VAR>b : β<GOAL>((p a' * if h : p a' = 0 then 0 else (f a' h) b) * if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0 then 0 else (g b ⋯) a) = p a' * if h : p a' = 0 then 0 else (f a' h) b * if h : (f a' h) b = 0 then 0 else (g b ⋯) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g✝ : α → β<VAR>inst✝¹ : Zero β<VAR>inst✝ : T2Space β<VAR>g : α → β<VAR>hg : FinStronglyMeasurable g μ<VAR>hfg : f =ᶠ[ae μ] g<GOAL>∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g✝ : α → β<VAR>inst✝¹ : Zero β<VAR>inst✝ : T2Space β<VAR>g : α → β<VAR>hg : FinStronglyMeasurable g μ<VAR>hfg : f =ᶠ[ae μ] g<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hgt_zero : ∀ x ∈ tᶜ, g x = 0<VAR>htμ : SigmaFinite (μ.restrict t)<GOAL>∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g✝ : α → β<VAR>inst✝¹ : Zero β<VAR>inst✝ : T2Space β<VAR>g : α → β<VAR>hg : FinStronglyMeasurable g μ<VAR>hfg : f =ᶠ[ae μ] g<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hgt_zero : ∀ x ∈ tᶜ, g x = 0<VAR>htμ : SigmaFinite (μ.restrict t)<GOAL>f =ᶠ[ae (μ.restrict tᶜ)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g✝ : α → β<VAR>inst✝¹ : Zero β<VAR>inst✝ : T2Space β<VAR>g : α → β<VAR>hg : FinStronglyMeasurable g μ<VAR>hfg : f =ᶠ[ae μ] g<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hgt_zero : ∀ x ∈ tᶜ, g x = 0<VAR>htμ : SigmaFinite (μ.restrict t)<GOAL>g =ᶠ[ae (μ.restrict tᶜ)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f g✝ : α → β<VAR>inst✝¹ : Zero β<VAR>inst✝ : T2Space β<VAR>g : α → β<VAR>hg : FinStronglyMeasurable g μ<VAR>hfg : f =ᶠ[ae μ] g<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hgt_zero : ∀ x ∈ tᶜ, g x = 0<VAR>htμ : SigmaFinite (μ.restrict t)<GOAL>∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S T : Subgroupoid C<VAR>h : S ≤ T<VAR>s t : ↑S.objs<VAR>x✝¹ x✝ : s ⟶ t<VAR>f : ↑s ⟶ ↑t<VAR>hf : f ∈ S.arrows ↑s ↑t<VAR>g : ↑s ⟶ ↑t<VAR>hg : g ∈ S.arrows ↑s ↑t<GOAL>⟨f, ⋯⟩ = ⟨g, ⋯⟩ → ⟨f, hf⟩ = ⟨g, hg⟩
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S T : Subgroupoid C<VAR>h : S ≤ T<VAR>s t : ↑S.objs<VAR>x✝¹ x✝ : s ⟶ t<VAR>f : ↑s ⟶ ↑t<VAR>hf : f ∈ S.arrows ↑s ↑t<VAR>g : ↑s ⟶ ↑t<VAR>hg : g ∈ S.arrows ↑s ↑t<GOAL>f = g → f = g
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s t : Multiset α<GOAL>{a}.Disjoint t ∧ s.Disjoint t ↔ a ∉ t ∧ s.Disjoint t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℕ<GOAL>round (↑y + x) = ↑y + round x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedCommSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<VAR>c : 𝕜<GOAL>StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedCommSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>z : E<VAR>c : 𝕜<VAR>h : StarConvex 𝕜 (z + c • x) ((fun x => z + x) '' (c • s))<GOAL>StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : ↑u * a = 1<GOAL>↑u⁻¹ = ↑u⁻¹ * 1
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : ↑u * a = 1<GOAL>↑u⁻¹ * 1 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>s : Set β<VAR>hs : ¬s.Finite<GOAL>count (f '' s) = count s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>s : Set β<VAR>hs : ¬s.Finite<GOAL>count (f '' s) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s✝ : Set α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : MeasurableSingletonClass β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>s : Set β<VAR>hs : ¬(f '' s).Finite<GOAL>count (f '' s) = ⊤
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>i : B<GOAL>cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)
<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 : Finset M<VAR>hs : LinearIndependent R Subtype.val<GOAL>finrank R ↥(span R ↑s) = s.card
<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 : Finset M<VAR>hs : LinearIndependent R Subtype.val<GOAL>s = (↑s).toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t s : Set α<GOAL>𝓟 s ⊓ 𝓟 sᶜ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s✝ t s : Set α<GOAL>𝓟 s ⊔ 𝓟 sᶜ = ⊤
<VAR>b : Ordinal.{u_1}<GOAL>0 ^ succ b = 0 ^ b * 0
<VAR>a b : Ordinal.{u_1}<VAR>h : ¬a = 0<GOAL>a ^ succ b = a ^ b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>r C : ℝ≥0∞<VAR>hr : r < 1<VAR>hC : C ≠ ⊤<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>edist (f 0) a ≤ C / (1 - r)