ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>i : Nat<VAR>xs : List α<VAR>p : α → Bool<VAR>w : findIdx? p xs = some i<GOAL>match xs.get? i with | some a => p a = true | none => false = true
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<GOAL>∃ x, f x ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.246298}<VAR>a b c : Cardinal.{u}<GOAL>a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.246298}<VAR>a b c : Cardinal.{u}<GOAL>(∀ (i : ↑(Iio b)), a ^ ↑i ≤ c) ↔ ∀ x < b, a ^ x ≤ c
<VAR>α β : Type u<VAR>c✝ : Cardinal.{?u.246298}<VAR>a b c : Cardinal.{u}<GOAL>BddAbove (range fun c => a ^ ↑c)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : OrderTop α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq β<VAR>c : α<GOAL>c ≤ (s₁ ∪ s₂).inf f ↔ c ≤ s₁.inf f ⊓ s₂.inf f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.105888, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ : Triangle Cᵒᵖ<VAR>φ : T₁ ⟶ T₂<GOAL>((shiftFunctor C 1).map φ.hom₃.unop).op ≫ ((shiftFunctor C 1).map T₂.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ = (((shiftFunctor C 1).map T₁.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁) ≫ φ.hom₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝⁵ : GroupWithZero G₀<VAR>inst✝⁴ : TopologicalSpace G₀<VAR>inst✝³ : HasContinuousInv₀ G₀<VAR>inst✝² : ContinuousMul G₀<VAR>f g : α → G₀<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>a : α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h₀ : ∀ (x : α), g x ≠ 0<GOAL>Continuous fun x => f x / g x
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>(of i) ((φ i) x) = (base φ) x
<VAR>a b c d m n : ℤ<VAR>ha : a ≠ 0<VAR>h : m * a ∣ n * a<GOAL>a * m ∣ a * n
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ<VAR>hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ<GOAL>AEMeasurable (f :: l).prod μ
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ<VAR>hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ<GOAL>AEMeasurable (f :: l).prod μ
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ<VAR>hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ<GOAL>AEMeasurable (f * l.prod) μ
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>h : LinearMap.IsSymm B₁<VAR>x y : M<GOAL>(((associatedHom S) B₁.toQuadraticMap) x) y = (B₁ x) y
<VAR>P : TopCat → Prop<VAR>inst✝ : HasExplicitFiniteCoproducts P<VAR>hP' : ∀ ⦃X Y B : CompHausLike P⦄ (f : X ⟶ B) (g : Y ⟶ B), OpenEmbedding ⇑f → HasExplicitPullback f g<VAR>X✝ Y✝ Z✝ : CompHausLike P<VAR>f : Z✝ ⟶ X✝ ⨿ Y✝<GOAL>OpenEmbedding ⇑coprod.inl
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>mabs (a * b) ≤ mabs a * mabs b
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>a * b ≤ mabs a * mabs b
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>(a * b)⁻¹ ≤ mabs a * mabs b
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n i : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(erase n { toFinsupp := toFinsupp✝ }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp✝ }.coeff i
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n i : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(Finsupp.erase n toFinsupp✝) i = if i = n then 0 else toFinsupp✝ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>c - a - (c - b) ≤ b - a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>c ≤ c - b + (a + (b - a))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ a₁ a₂ b b₁ b₂ c x a : α<GOAL>Injective (uIcc a)
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>(minCardFinsetOfMemConvexHull hx).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>hx : x ∈ (convexHull 𝕜) s<GOAL>((convexHull 𝕜) ↑(minCardFinsetOfMemConvexHull hx)).Nonempty
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>m n✝ : ℕ<GOAL>↑(m / (n✝ + 1)) ≤ ↑m / ↑(n✝ + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>m n✝ : ℕ<GOAL>m / (n✝ + 1) * (n✝ + 1) ≤ m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>m n✝ : ℕ<GOAL>0 < ↑(n✝ + 1)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : V<VAR>hx : x ∈ (p.takeUntil u h).support<GOAL>x ∈ p.support
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ x✝ y : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>h : u ∈ p.support<VAR>x : V<VAR>hx : x ∈ (p.takeUntil u h).support<GOAL>x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>σ.cycleType.sum = σ.support.card
<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>X : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>f : X → E<VAR>hf : HasCompactSupport f<VAR>h2f : AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C<GOAL>Memℒp f p μ
<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>X : Type u_5<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : MeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>f : X → E<VAR>hf : HasCompactSupport f<VAR>h2f : AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C<VAR>this : Memℒp f ⊤ μ<GOAL>Memℒp f p μ
<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>inst✝² : IsCofilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>IsCofilteredOrEmpty C
<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>inst✝² : IsCofilteredOrEmpty D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>IsFilteredOrEmpty Cᵒᵖ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i✝ : ι<VAR>hsum : Multipliable g<VAR>hg : ∀ (i : ι), 1 ≤ g i<VAR>i : ι<VAR>hi : 1 < g i<GOAL>1 < ∏' (i : ι), g i
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i✝ : ι<VAR>hsum : Multipliable g<VAR>hg : ∀ (i : ι), 1 ≤ g i<VAR>i : ι<VAR>hi : 1 < g i<GOAL>∏' (x : ?m.49247), 1 < ∏' (i : ι), g i
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i✝ : ι<VAR>hsum : Multipliable g<VAR>hg : ∀ (i : ι), 1 ≤ g i<VAR>i : ι<VAR>hi : 1 < g i<GOAL>Type ?u.49244
<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x<GOAL>(Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x<VAR>x✝ : ℕ<GOAL>2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>wittStructureRat p Φ n * C (↑p ^ n) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>this : xInTermsOfW p ℚ n * C (↑p ^ n) = X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)<GOAL>wittStructureRat p Φ n * C (↑p ^ n) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>this : (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n * C (↑p ^ n)) = (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))<GOAL>wittStructureRat p Φ n * C (↑p ^ n) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>this : (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) = (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))<GOAL>wittStructureRat p Φ n * C (↑p ^ n) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) Φ - (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) = (bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range n, C ↑p ^ x * (bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ x) ^ p ^ (n - x) = ∑ x ∈ Finset.range n, C ↑p ^ x * wittStructureRat p Φ x ^ p ^ (n - x)
<VAR>α β : Type u<GOAL>#α < ℵ₀ ↔ Finite α
<VAR>x : Tree Unit<VAR>n : ℕ<GOAL>x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Monoid α<VAR>inst✝² : AddGroup β<VAR>inst✝¹ : DistribMulAction α β<VAR>inst✝ : DecidableEq β<VAR>a : α<VAR>s : Finset α<VAR>t : Finset β<GOAL>a • -t = -(a • t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasBinaryCoproducts C<VAR>inst✝ : HasPushouts C<VAR>F : WalkingParallelPair ⥤ C<GOAL>pushoutInl F = pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left)) (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))
<VAR>α : Type u_1<VAR>s✝ t s : Set α<GOAL>(fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t✝ : Set α<VAR>a✝ b a : α<VAR>t : Set α<VAR>h : a ∉ t<GOAL>(insert a t).encard = t.encard + 1
<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₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>h : Injective f<VAR>x y : α<GOAL>f x ≤ f y ↔ x ≤ y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m✝ m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfg : μ.withDensity f = μ.withDensity g<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m✝ m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t : Set α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hfg : μ.withDensity f = μ.withDensity g<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : μ s < ⊤<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>(π.map g).map ⟦p'⟧ = hcast ⋯ ≫ (π.map H.uliftMap).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) ⟦p'⟧) ≫ hcast ⋯
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), g (p' t) = H.uliftMap (((Path.refl { down := 1 }).prod p') t)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), g (p' t) = H.uliftMap ((fun t => ((Path.refl { down := 1 }) t, p' t)) t)
<VAR>X Y : TopCat<VAR>f g : C(↑X, ↑Y)<VAR>H : f.Homotopy g<VAR>x₀ x₁ : ↑X<VAR>p : fromTop x₀ ⟶ fromTop x₁<VAR>p' : Path (fromTop x₀).as (fromTop x₁).as<GOAL>∀ (t : ↑I), g (p' t) = H (((Path.refl { down := 1 }) t).down, p' t)
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>Finset.univ.noncommProd (fun j => (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>(insert i (Finset.univ.erase i)).noncommProd (fun j => (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>(ϕ i) (Pi.mulSingle i y i) * (Finset.univ.erase i).noncommProd (fun j => (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>(ϕ i) y * (Finset.univ.erase i).noncommProd (fun j => (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>(ϕ i) y * ?m ^ (Finset.univ.erase i).card = (ϕ i) y
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>M
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>N : ι → Type u_3<VAR>inst✝ : (i : ι) → Monoid (N i)<VAR>ϕ : (i : ι) → N i →* M<VAR>hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)<VAR>f g : (i : ι) → N i<VAR>i : ι<VAR>y : N i<GOAL>∀ x ∈ Finset.univ.erase i, (ϕ x) (Pi.mulSingle i y x) = ?m
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℂ<GOAL>logDeriv sin x✝ = x✝.cot
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>S : Set (Subring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>x : R<VAR>n : ℤ<GOAL>(algebraMap R A) (eval x (T R n)) = eval ((algebraMap R A) x) (T A n)
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪ₑ[L] N<VAR>α : Type u_5<VAR>φ : L.Formula α<VAR>x : α → M<GOAL>φ.Realize (⇑f ∘ x) ↔ φ.Realize x
<VAR>x✝ y✝ z : ℝ<VAR>n✝ : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<VAR>n : ℤ<GOAL>x ^ (y + ↑n) = x ^ y * x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑f j| < ε ∧ |↑g j| < ε<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : |↑f j| < ε<VAR>H₂ : |↑g j| < ε<GOAL>|↑(f ⊓ g) j| < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑f j| < ε ∧ |↑g j| < ε<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : -ε < ↑f j ∧ ↑f j < ε<VAR>H₂ : -ε < ↑g j ∧ ↑g j < ε<GOAL>-ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : Arrow C<VAR>X : Augmented C<VAR>G : F ⟶ Augmented.toArrow.obj X<VAR>x : SimplexCategory<VAR>j : Fin (x.len + 1)<GOAL>G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map ((SimplexCategory.mk 0).const x j) = G.left ≫ X.hom.app x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : Arrow C<VAR>X : Augmented C<VAR>G : F ⟶ Augmented.toArrow.obj X<VAR>x : SimplexCategory<VAR>j : Fin (x.len + 1)<VAR>t : ((const C).obj X.left).map ((SimplexCategory.mk 0).const x j) ≫ X.hom.app x = X.hom.app (SimplexCategory.mk 0) ≫ ((𝟭 (CosimplicialObject C)).obj X.right).map ((SimplexCategory.mk 0).const x j)<GOAL>G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map ((SimplexCategory.mk 0).const x j) = G.left ≫ X.hom.app x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : Arrow C<VAR>X : Augmented C<VAR>G : F ⟶ Augmented.toArrow.obj X<VAR>x : SimplexCategory<VAR>j : Fin (x.len + 1)<VAR>t : 𝟙 X.left ≫ X.hom.app x = X.hom.app (SimplexCategory.mk 0) ≫ X.right.map ((SimplexCategory.mk 0).const x j)<GOAL>G.left ≫ X.hom.app (SimplexCategory.mk 0) ≫ X.right.map ((SimplexCategory.mk 0).const x j) = G.left ≫ X.hom.app x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : Arrow C<VAR>X : Augmented C<VAR>G : F ⟶ Augmented.toArrow.obj X<VAR>x : SimplexCategory<VAR>j : Fin (x.len + 1)<VAR>t : X.hom.app x = X.hom.app (SimplexCategory.mk 0) ≫ X.right.map ((SimplexCategory.mk 0).const x j)<GOAL>G.left ≫ X.hom.app (SimplexCategory.mk 0) ≫ X.right.map ((SimplexCategory.mk 0).const x j) = G.left ≫ X.hom.app x
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>a₁ a₂ : ℤ<VAR>b : ℕ<GOAL>J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)
<VAR>a₁ a₂ : ℤ<VAR>b : ℕ<GOAL>(List.map (fun x => legendreSym (↑x) a₁ * legendreSym (↑x) a₂) b.primeFactorsList.attach).prod = (List.map (fun x => legendreSym (↑x) a₁) b.primeFactorsList.attach).prod * (List.map (fun x => legendreSym (↑x) a₂) b.primeFactorsList.attach).prod
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<VAR>b : α<VAR>nth_partDen_eq : g.partDens.get? n = some b<GOAL>∃ gp, g.s.get? n = some gp ∧ gp.b = b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : MeasurableSpace E<VAR>μ : Measure E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>b₀ : Basis ι ℝ E<GOAL>μ (fundamentalDomain b) = ENNReal.ofReal |b₀.det ⇑b| * μ (fundamentalDomain b₀)