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>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α →. β<VAR>x✝¹ x✝ : α × β<GOAL>x✝ ∈ (PFun.id α).prodMap (PFun.id β) x✝¹ ↔ x✝ ∈ PFun.id (α × β) x✝¹
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : Mono f<VAR>inst✝ : Mono g<VAR>x : Subobject X<GOAL>(map (f ≫ g)).obj x = (map g).obj ((map f).obj x)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : Mono f<VAR>inst✝ : Mono g<VAR>t : MonoOver X<GOAL>(map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>b b' : F<GOAL>Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<GOAL>a⁻¹ = 0 ↔ a = 0
<VAR>s : Set ℤ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, b ≤ z<VAR>Hinh : ∃ z, z ∈ s<VAR>this : s.Nonempty ∧ BddBelow s<GOAL>sInf s = ↑(b.leastOfBdd Hb Hinh)
<VAR>s : Set ℤ<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>b : ℤ<VAR>Hb : ∀ z ∈ s, b ≤ z<VAR>Hinh : ∃ z, z ∈ s<VAR>this : s.Nonempty ∧ BddBelow s<GOAL>↑((Classical.choose ⋯).leastOfBdd ⋯ ⋯) = ↑(b.leastOfBdd Hb Hinh)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : CompleteSpace 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : UniformSpace E<VAR>inst✝⁴ : T2Space E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>CompleteSpace E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : CompleteSpace 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : UniformSpace E<VAR>inst✝⁴ : T2Space E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯<GOAL>CompleteSpace E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : CompleteSpace 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : UniformSpace E<VAR>inst✝⁴ : T2Space E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯<VAR>this : UniformEmbedding ⇑e.toEquiv.symm<GOAL>CompleteSpace E
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a / d ≤ b / c
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a * c ≤ b * d
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : ℙ K V<GOAL>v.submodule = Submodule.span K {v.rep}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : ℙ K V<GOAL>(mk K v.rep ⋯).submodule = Submodule.span K {v.rep}
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<GOAL>commProb M ≤ 1
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<GOAL>↑(Nat.card { p // Commute p.1 p.2 }) ≤ ↑(Nat.card M) ^ 2
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<GOAL>Nat.card { p // Commute p.1 p.2 } ≤ Nat.card (M × M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Memℒp (Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)) 1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>n : ℕ<GOAL>eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ ↑((ν a) univ).toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>n : ℕ<GOAL>(ν a) univ = ↑((ν a) univ).toNNReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>n : ℕ<GOAL>(ν a) univ ≠ ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : SupHomClass F α β<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<GOAL>s ⊻ s = s ↔ SupClosed ↑s
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<VAR>f g : C(X, ℝ)₀<VAR>this : SemilinearMapClass (C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] C(X, ℝ≥0)) (RingHom.id ℝ≥0) C(X, ℝ≥0)₀ C(X, ℝ≥0)<GOAL>(f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<VAR>f g : C(X, ℝ)₀<VAR>this : SemilinearMapClass (C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] C(X, ℝ≥0)) (RingHom.id ℝ≥0) C(X, ℝ≥0)₀ C(X, ℝ≥0)<GOAL>↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = ↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)
<VAR>z w : ℍ<VAR>r R a : ℝ<VAR>y₁ y₂ : ℍ<GOAL>dist (a +ᵥ y₁) (a +ᵥ y₂) = dist y₁ y₂
<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>a✝ a' : α<VAR>b : M<VAR>a : α<GOAL>(fun f => ⇑f) (single a 0) = (fun f => ⇑f) 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>ht_range : generateFrom (Set.range t) = m<GOAL>⨆ n, ↑(partitionFiltration ht) n = m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : LinearOrderedField β<VAR>a a₁ a₂ : α<VAR>b : β<VAR>q✝ q : ℚ<GOAL>cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>ht : NullMeasurableSet t μ<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>((μ.restrict t).restrict s) u = (μ.restrict (s ∩ t)) u
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∈ s<GOAL>(Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∈ s<GOAL>(Set.sumDiffSubset h) ((Set.sumDiffSubset h).symm x) = (Set.sumDiffSubset h) (Sum.inl ⟨↑x, hx⟩)
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∈ s<GOAL>x = inclusion h ⟨↑x, hx⟩
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hlt : ∀ i ∈ ↑l, ord I i < o₁<GOAL>(πs' C h) (eval (π C fun x => ord I x < o₁) l) = eval (π C fun x => ord I x < o₂) l
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hlt : ∀ i ∈ ↑l, ord I i < o₁<GOAL>((πs' C h) (eval (π C fun x => ord I x < o₁) l)).toFun = ⇑(eval (π C fun x => ord I x < o₂) l)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>r : R<GOAL>(fun r => r • 1) r = x ↔ (algebraMap R A) r = x
<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 : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : x.Compatible<GOAL>FamilyOfElements.restrict ⋯ x.sieveExtend = x
<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 : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : x.Compatible<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : R f<GOAL>FamilyOfElements.restrict ⋯ x.sieveExtend f hf = x f hf
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<GOAL>μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s✝ : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>s : ℝ<VAR>this : closedBall 0 (r * s) = r • closedBall 0 s<GOAL>μ (closedBall x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall 0 s)
<VAR>p b : ℝ<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<GOAL>∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)
<VAR>p b : ℝ<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<GOAL>∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)
<VAR>p b : ℝ<VAR>hp : 1 ≤ p<VAR>hb : 0 < b<GOAL>π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l : List M<VAR>h : ∀ x ∈ l, x = 1<GOAL>l.prod = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l : List M<VAR>h : ∀ x ∈ l, x = 1<GOAL>ℕ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝ : CanonicallyOrderedCommMonoid M<VAR>l : List M<VAR>h : ∀ x ∈ l, x = 1<GOAL>l.length = ?m.22276
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x y : 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>n : ℕ<GOAL>((WittVector.map g) (f x y)).coeff n = (f ((WittVector.map g) x) ((WittVector.map g) y)).coeff n
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x y : 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>n : ℕ<GOAL>(eval₂Hom (g.comp (algebraMap ℤ R)) fun i => g (![x.coeff, y.coeff] i.1 i.2)) (φ n) = (aeval fun a => ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2) (φ n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x y : 𝕎 R<VAR>φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n => peval (φ n) ![x.coeff, y.coeff]<VAR>n : ℕ<GOAL>(fun i => g (![x.coeff, y.coeff] i.1 i.2)) = fun a => ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Semigroup α<VAR>inst✝ : HasDistribNeg α<VAR>a b c : α<GOAL>(∃ b_1, -b = a * (Equiv.symm (Equiv.neg α)) b_1) ↔ a ∣ b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<GOAL>nats = 0 :: map succ nats
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<GOAL>∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n✝ : ℕ<GOAL>nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>n✝ : ℕ<GOAL>nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>x✝ : α × β × γ<GOAL>x✝ ∈ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
<VAR>p q : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d✝ a : ℕ<VAR>ha : a ≠ 0<VAR>n d : ℕ<GOAL>Rat.divInt (↑a * ↑n) (↑a * ↑d) = Rat.divInt ↑n ↑d
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>g : R[X]<GOAL>f ∣ h.repr (h.map g) - g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 s2 : WSeq α<VAR>t1 t2 : WSeq β<VAR>h1 : LiftRel R s1 t1<VAR>h2 : LiftRel R s2 t2<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>Computation.LiftRel (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 s2 : WSeq α<VAR>t1 t2 : WSeq β<VAR>h1 : LiftRel R s1 t1<VAR>h2 : LiftRel R s2 t2<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 s2 : WSeq α<VAR>t1 t2 : WSeq β<VAR>h1 : LiftRel R s1 t1<VAR>h2 : LiftRel R s2 t2<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>LiftRelO R (LiftRel R) a b → LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1 s2 : WSeq α<VAR>t1 t2 : WSeq β<VAR>h1 : LiftRel R s1 t1<VAR>h2 : LiftRel R s2 t2<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1✝ s2 : WSeq α<VAR>t1✝ t2 : WSeq β<VAR>h1 : LiftRel R s1✝ t1✝<VAR>h2 : LiftRel R s2 t2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t<VAR>s1 : WSeq α<VAR>t1 : WSeq β<VAR>h : LiftRel R s1 t1<GOAL>Computation.LiftRel (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) (s1.append s2).destruct (t1.append t2).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1✝ s2 : WSeq α<VAR>t1✝ t2 : WSeq β<VAR>h1 : LiftRel R s1✝ t1✝<VAR>h2 : LiftRel R s2 t2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t<VAR>s1 : WSeq α<VAR>t1 : WSeq β<VAR>h : LiftRel R s1 t1<GOAL>Computation.LiftRel (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) (s1.destruct.bind (destruct_append.aux s2)) (t1.destruct.bind (destruct_append.aux t2))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s1✝ s2 : WSeq α<VAR>t1✝ t2 : WSeq β<VAR>h1 : LiftRel R s1✝ t1✝<VAR>h2 : LiftRel R s2 t2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t<VAR>s1 : WSeq α<VAR>t1 : WSeq β<VAR>h : LiftRel R s1 t1<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) (destruct_append.aux s2 a) (destruct_append.aux t2 b)
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<VAR>x : Γ₀<VAR>hx : (hom v) x = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<VAR>x : Γ₀<VAR>hx : (hom v) x = 0<VAR>h_lt : 0 < x<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<VAR>x : Γ₀<VAR>hx : (hom v) x = 0<VAR>h_lt : 0 < x<VAR>hs : (hom v) 0 < (hom v) x<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>Γ₀ : Type u_2<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>inst✝ : v.RankOne<VAR>x : Γ₀<VAR>hx : (hom v) x = 0<VAR>h_lt : 0 < x<VAR>hs : 0 < 0<GOAL>False
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun x => cosKernel a x - 1) =O[atTop] fun x => rexp (-p * x)
<VAR>a : ℝ<GOAL>∃ p, 0 < p ∧ (fun x => cosKernel (↑a) x - 1) =O[atTop] fun x => rexp (-p * x)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ (fun x => cosKernel (↑a) x - 1) =O[atTop] fun x => rexp (-p * x)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 x - if 1 = 0 then 1 else 0)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * HurwitzKernelBounds.F_nat 0 1 x
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖cosKernel (↑a) t - 1‖ ≤ 2 * HurwitzKernelBounds.F_nat 0 1 t
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖∑' (b : ℕ), 2 * Real.cos (2 * π * a * (↑b + 1)) * rexp (-π * (↑b + 1) ^ 2 * t)‖ ≤ 2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 0 1 t n
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>∀ (i : ℕ), ‖2 * Real.cos (2 * π * a * (↑i + 1)) * rexp (-π * (↑i + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t i
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>‖2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>|Real.cos (2 * π * a * (↑n + 1))| * rexp (-π * (↑n + 1) ^ 2 * t) ≤ rexp (-π * (↑n + 1) ^ 2 * t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : GroupWithZero α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s / 0
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, cos x ^ 2 = (cos b * sin b - cos a * sin a + b - a) / 2
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i j : ι<GOAL>(erase i f) j = (f - single i (f i)) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<GOAL>(erase i f) i = (f - single i (f i)) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i j : ι<VAR>h : i ≠ j<GOAL>(erase i f) j = (f - single i (f i)) j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<GOAL>mrange (inr M N) = ⊥.prod ⊤
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<VAR>w : InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>ℚ⟮↑x⟯ = ⊤
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<VAR>w : InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>∀ (ψ : K →ₐ[ℚ] ℂ), w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<VAR>w : InfinitePlace K<VAR>h₁ : x ≠ 0<VAR>h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1<VAR>h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1<GOAL>∀ (x : K), Polynomial.Splits (algebraMap ℚ ℂ) (minpoly ℚ x)