ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : PowerSeries R<VAR>n : ℕ<GOAL>((ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff R n) x
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≠ 0<GOAL>0 < a / 2
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y✝ Z✝ : C<VAR>f✝ : Y✝ ⟶ X<VAR>S✝ R✝ : Sieve X<VAR>R : Presieve X<VAR>S : Sieve X<VAR>ss : R ≤ S.arrows<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>g : Z ⟶ X<VAR>hg : R g<GOAL>S.arrows (f ≫ g)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : PrimeSpectrum R<GOAL>IsClosed {x} ↔ x.asIdeal.IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : PrimeSpectrum R<GOAL>zeroLocus ↑x.asIdeal ⊆ {x} ↔ x.asIdeal.IsMaximal
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z z' z1 : ℤ_[p]<VAR>hz' : z' = z - z1<VAR>hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>n : ℕ<VAR>hz : ih_gen n z<GOAL>‖z' - z‖ = ‖z1‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z z' z1 : ℤ_[p]<VAR>hz' : z' = z - z1<VAR>hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖<VAR>n : ℕ<VAR>hz : ih_gen n z<GOAL>‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>I✝ : Ideal R<VAR>y : R<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Away y S<VAR>inst✝ : IsJacobson R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<VAR>hy : y ∉ I<GOAL>(map (algebraMap R S) I).IsMaximal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>I✝ : Ideal R<VAR>y : R<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Away y S<VAR>inst✝ : IsJacobson R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<VAR>hy : y ∉ I<GOAL>I.IsMaximal ∧ y ∉ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).OuterRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>hx : 0 ≠ ⊤<GOAL>(0 • μ).OuterRegular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ✝ μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>h0 : x ≠ 0<GOAL>(x • μ).OuterRegular
<VAR>m✝ n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : m.castSucc < i<GOAL>(finSuccEquiv' i) m.castSucc = some m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(m.bind dirac) s = m s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<GOAL>{i | i < k}.encard = ↑k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<GOAL>{i | i < k}.encard = (↑(Finset.range k)).encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<GOAL>↑k = ↑(Finset.range k).card
<VAR>l m r : List Char<GOAL>{ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.bsize = utf8Len m
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>k : Type u_2<VAR>inst✝¹ : Field k<VAR>inst✝ : Algebra k K<VAR>φ : K →+* ℂ<VAR>σ : K ≃ₐ[k] K<VAR>hσ : IsConj φ σ<VAR>x : K<GOAL>(conjugate φ) x = (φ.comp ↑σ.symm) x
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a b : Ordinal.{u_1}<VAR>h : b ≤ nfp f a<GOAL>f b ≤ nfp f a
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : ↑{ num := N, den := D, den_nz := P, reduced := C } ^ n = ↑m<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑D ≠ 0<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : ↑({ num := N, den := D, den_nz := P, reduced := C } ^ n) = ↑m<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑D ≠ 0<VAR>c2 : ↑↑D ^ n ≠ 0<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : m * ↑D ^ n = N ^ n<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑D ≠ 0<VAR>c2 : ↑↑D ^ n ≠ 0<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : m * ↑D ^ n = N ^ n<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑D ≠ 0<VAR>c2 : ↑↑D ^ n ≠ 0<VAR>hdivn : ↑D ^ n ∣ N ^ n<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>D : ℕ<VAR>P : D ≠ 0<VAR>C : N.natAbs.Coprime D<VAR>hxr : m * ↑D ^ n = N ^ n<VAR>hv : ¬∃ y, ↑{ num := N, den := D, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑D ≠ 0<VAR>c2 : ↑↑D ^ n ≠ 0<VAR>hdivn : D ∣ N.natAbs<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>P : 1 ≠ 0<VAR>C : N.natAbs.Coprime 1<VAR>hxr : m * ↑1 ^ n = N ^ n<VAR>hv : ¬∃ y, ↑{ num := N, den := 1, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑1 ≠ 0<VAR>c2 : ↑↑1 ^ n ≠ 0<VAR>hdivn : 1 ∣ N.natAbs<GOAL>False
<VAR>n : ℕ<VAR>m : ℤ<VAR>hnpos : 0 < n<VAR>N : ℤ<VAR>P : 1 ≠ 0<VAR>C : N.natAbs.Coprime 1<VAR>hxr : m * ↑1 ^ n = N ^ n<VAR>hv : ¬∃ y, ↑{ num := N, den := 1, den_nz := P, reduced := C } = ↑y<VAR>c1 : ↑↑1 ≠ 0<VAR>c2 : ↑↑1 ^ n ≠ 0<VAR>hdivn : 1 ∣ N.natAbs<GOAL>↑{ num := N, den := 1, den_nz := P, reduced := C } = ↑N
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : MulSemiringAction M R<VAR>m : M<GOAL>HSMul.hSMul m = map (MulSemiringAction.toRingHom M R m)
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : MulSemiringAction M R<VAR>m : M<GOAL>DistribMulAction.toAddMonoidHom R[X] m = (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : MulSemiringAction M R<VAR>m : M<VAR>n : ℕ<VAR>r : R<GOAL>m • (monomial n) r = map (MulSemiringAction.toRingHom M R m) ((monomial n) r)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocRing α<VAR>a b : α<GOAL>a * (1 - b) = a - a * b
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : 0 < ε<GOAL>x ∈ ball x ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁵ : Norm E<VAR>inst✝¹⁴ : Norm F<VAR>inst✝¹³ : Norm G<VAR>inst✝¹² : SeminormedAddCommGroup E'<VAR>inst✝¹¹ : SeminormedAddCommGroup F'<VAR>inst✝¹⁰ : SeminormedAddCommGroup G'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F''<VAR>inst✝⁷ : NormedAddCommGroup G''<VAR>inst✝⁶ : SeminormedRing R<VAR>inst✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝¹ : One F<VAR>inst✝ : NormOneClass F<GOAL>(f' =o[l] fun _x => 1) ↔ Tendsto f' l (𝓝 0)
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝¹¹ : Fintype m<VAR>inst✝¹⁰ : DecidableEq m<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : (i : m) → Fintype (n' i)<VAR>inst✝⁶ : (i : m) → DecidableEq (n' i)<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : TopologicalSpace 𝔸<VAR>inst✝² : TopologicalRing 𝔸<VAR>inst✝¹ : Algebra 𝕂 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>v : m → 𝔸<GOAL>exp 𝕂 (diagonal v) = diagonal (exp 𝕂 v)
<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>inst✝ : TopologicalSpace γ✝<VAR>f✝ g✝ : α → β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mα : MeasurableSpace α<VAR>f : γ → α<VAR>μ : Measure γ<VAR>hf : MeasurableEmbedding f<VAR>g : α → β<GOAL>AEStronglyMeasurable g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ
<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>inst✝ : TopologicalSpace γ✝<VAR>f✝ g✝ : α → β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mα : MeasurableSpace α<VAR>f : γ → α<VAR>μ : Measure γ<VAR>hf : MeasurableEmbedding f<VAR>g : α → β<GOAL>AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)
<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>inst✝ : TopologicalSpace γ✝<VAR>f✝ g✝ : α → β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mα : MeasurableSpace α<VAR>f : γ → α<VAR>μ : Measure γ<VAR>hf : MeasurableEmbedding f<VAR>g : α → β<VAR>g₁ : γ → β<VAR>hgm₁ : StronglyMeasurable g₁<VAR>heq : g ∘ f =ᶠ[ae μ] g₁<GOAL>AEStronglyMeasurable g (Measure.map f μ)
<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>inst✝ : TopologicalSpace γ✝<VAR>f✝ g✝ : α → β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mα : MeasurableSpace α<VAR>f : γ → α<VAR>μ : Measure γ<VAR>hf : MeasurableEmbedding f<VAR>g g₂ : α → β<VAR>hgm₂ : StronglyMeasurable g₂<VAR>hgm₁ : StronglyMeasurable (g₂ ∘ f)<VAR>heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f<GOAL>AEStronglyMeasurable g (Measure.map f μ)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<GOAL>φ.IsNilRegular x ↔ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff φ.nilRank) ≠ 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : IntermediateField F E<VAR>t : Finset E<VAR>ht : Algebra.adjoin F ↑t = S.toSubalgebra<GOAL>S.FG
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<GOAL>∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>this : CharP R (ringChar R) := (Classical.choose_spec (CharP.exists_unique R)).left<GOAL>∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>Q : R[T;T⁻¹] → Prop<VAR>f : R[T;T⁻¹]<VAR>Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))<GOAL>Q f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>Q : R[T;T⁻¹] → Prop<VAR>f : R[T;T⁻¹]<VAR>Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))<VAR>n : ℕ<VAR>f' : R[X]<VAR>hf : toLaurent f' = f * T ↑n<GOAL>Q f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>Q : R[T;T⁻¹] → Prop<VAR>f : R[T;T⁻¹]<VAR>Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))<VAR>n : ℕ<VAR>f' : R[X]<VAR>hf : toLaurent f' = f * T ↑n<GOAL>Q (toLaurent f' * T (-↑n))
<VAR>m n k : ℕ<VAR>h : k < m<VAR>hk : optParam (k < m + n) ⋯<VAR>hnk : optParam (n + k < n + m) ⋯<GOAL>finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>hs : EqOn f₁ f s<VAR>hx : f₁ x = f x<GOAL>(fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Embedding f ↔ ∀ (i : ι), Embedding ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Inducing f ∧ Function.Injective f ↔ ∀ (i : ι), Inducing ((U i).carrier.restrictPreimage f) ∧ Function.Injective ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Inducing f ∧ Function.Injective f ↔ (∀ (x : ι), Inducing ((U x).carrier.restrictPreimage f)) ∧ ∀ (x : ι), Function.Injective ((U x).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Inducing f ↔ ∀ (x : ι), Inducing ((U x).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>h : Continuous f<GOAL>Function.Injective f ↔ ∀ (x : ι), Function.Injective ((U x).carrier.restrictPreimage f)
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : εNFA α σ<VAR>S✝ : Set σ<VAR>x✝ : List α<VAR>s : σ<VAR>a✝ : α<VAR>S : Set σ<VAR>x : List α<VAR>a : α<GOAL>M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : TopologicalSpace 𝔸<VAR>inst✝¹ : TopologicalRing 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>x y : 𝔸<VAR>h : Commute x y<GOAL>Commute x (exp 𝕂 y)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : TopologicalSpace 𝔸<VAR>inst✝¹ : TopologicalRing 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>x y : 𝔸<VAR>h : Commute x y<GOAL>Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'<GOAL>All P (l.balanceR x r) ↔ All P l ∧ P x ∧ All P r
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<VAR>a✝ : Nontrivial R<GOAL>t.prod.natDegree = (Multiset.map natDegree t).sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun f => f.leadingCoeff) t).prod ≠ 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun f => f.leadingCoeff) t).prod = 1
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<VAR>a✝ : Nontrivial R<GOAL>Multiset.map (fun f => f.leadingCoeff) t = replicate (Multiset.card t) 1
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ f ∈ t, f.Monic<VAR>a✝ : Nontrivial R<GOAL>1 = 1 ^ Multiset.card t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g s : ι → Set X<VAR>hs : LocallyFinite s<VAR>hs' : ∀ (i : ι), IsClosed (s i)<VAR>x : X<GOAL>∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g s : ι → Set X<VAR>hs : LocallyFinite s<VAR>hs' : ∀ (i : ι), IsClosed (s i)<VAR>x y : X<VAR>hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ<VAR>i : ι<VAR>hi : i ∈ {i | y ∈ s i}<GOAL>i ∈ {i | x ∈ s i}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g s : ι → Set X<VAR>hs : LocallyFinite s<VAR>hs' : ∀ (i : ι), IsClosed (s i)<VAR>x y : X<VAR>i : ι<VAR>hi : i ∈ {i | y ∈ s i}<VAR>hy : ∀ (i : ι), x ∉ s i → y ∉ s i<GOAL>i ∈ {i | x ∈ s i}
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>(isoRestrict f).inv ≫ f = Y.ofRestrict ⋯
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>im (↑r * z) = r * im z
<VAR>x y z t : EReal<VAR>h1 : x < y<VAR>h2 : z < t<GOAL>x + z < y + t
<VAR>y z t : EReal<VAR>h2 : z < t<VAR>h1 : ⊥ < y<GOAL>⊥ + z < y + t
<VAR>x y z t : EReal<VAR>h1 : x < y<VAR>h2 : z < t<VAR>hx : x ≠ ⊥<GOAL>x + z < y + t
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : DecidableEq δ'<VAR>e : δ' → δ<VAR>he : Injective e<VAR>s : Finset δ'<VAR>f : ((i : δ') → π (e i)) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : δ) → π i<VAR>h : Measurable fun x => (fun {x_1} => x) ∘' e<GOAL>(∫⋯∫⁻_Finset.image e s, f ∘ fun x => (fun {x_1} => x) ∘' e ∂μ) x = (∫⋯∫⁻_s, f ∂(fun {x} => μ) ∘' e) ((fun {x_1} => x) ∘' e)
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c a : α<VAR>u : αˣ<GOAL>a * (↑u⁻¹ * ↑u) = a
<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✝ R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : P.obj (op X)<VAR>ht : x.IsAmalgamation t<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : (generate R).arrows f<GOAL>P.map f.op t = P.map ⋯.choose.op (x ⋯.choose ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝ : MeasurableSpace α<GOAL>toMeasure 0 ⋯ = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>IsCompact (closure K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hKU : closure K ⊆ ⋃ i, U i<GOAL>∃ t, closure K ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>ι✝ : Type u_1<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hKU : closure K ⊆ ⋃ i, U i<VAR>t : Finset ι✝<VAR>ht : K ⊆ ⋃ i ∈ t, U i<GOAL>∃ t, closure K ⊆ ⋃ i ∈ t, U i
<VAR>θ : Angle<GOAL>(↑π - θ).sign = θ.sign
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : SFinite μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) t = (⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ) t
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : SFinite μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>this : μ.restrict μ.sigmaFiniteSetᶜ = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSetᶜ<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) t = (⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ) t
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : SFinite μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>this : μ.restrict μ.sigmaFiniteSetᶜ = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSetᶜ<GOAL>(μ.restrict μ.sigmaFiniteSetᶜ) t = ⊤ * (μ.toFinite.restrict μ.sigmaFiniteSetᶜ) t
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : SFinite μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>this : μ.restrict μ.sigmaFiniteSetᶜ = (μ.toFinite.withDensity μ.densityToFinite).restrict μ.sigmaFiniteSetᶜ<GOAL>∫⁻ (a : α) in t ∩ μ.sigmaFiniteSetᶜ, μ.densityToFinite a ∂μ.toFinite = ⊤ * μ.toFinite (t ∩ μ.sigmaFiniteSetᶜ)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>0 < z ↔ ∃ x > 0, ↑x = z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>0 < re z ∧ im z = 0 ↔ ∃ x > 0, re ↑x = re z ∧ im ↑x = im z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝³ : DecidablePred p<VAR>inst✝² : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset β<VAR>b a✝ : β<GOAL>a✝ ∈ filter (fun a => b ≠ a) s ↔ a✝ ∈ s.erase b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝³ : DecidablePred p<VAR>inst✝² : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset β<VAR>b a✝ : β<GOAL>a✝ ∈ s ∧ ¬b = a✝ ↔ ¬a✝ = b ∧ a✝ ∈ s
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>g : G<VAR>s : Set G<GOAL>g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>0 ≤ logb b x ↔ x ≤ 1
<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>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<GOAL>s.card < t.card
<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>t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑∅ < affineSpan k ↑t<GOAL>∅.card < t.card
<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>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<GOAL>s.card < t.card
<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>s : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hs' : s.Nonempty<VAR>hst : affineSpan k ↑s < affineSpan k ↑∅<GOAL>s.card < ∅.card
<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>s t : Finset V<VAR>hs : AffineIndependent k Subtype.val<VAR>hst : affineSpan k ↑s < affineSpan k ↑t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>s.card < t.card