ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<GOAL>map i p = C (i p.leadingCoeff) * (Multiset.map (fun a => X - C a) (map i p).roots).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<GOAL>map i p = C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<GOAL>C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod = map i p
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<GOAL>Multiset.card (map i p).roots = (map i p).natDegree
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>hsplit : Splits i p<GOAL>Multiset.card (map i p).roots = p.natDegree
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : StrictOrderedCommRing R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x z : P<VAR>t : R<VAR>ht0 : 0 ≤ t<VAR>right✝ : t ≤ 1<GOAL>SameRay R ((lineMap x z) t -ᵥ x) (z -ᵥ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid α<VAR>a b c : α<GOAL>Finite a (b * c) → Finite a c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid α<VAR>a b c : α<GOAL>Finite a (c * b) → Finite a c
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<GOAL>(pushoutSymmetry f f).hom = 𝟙 (pushout f f)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<GOAL>∫ (x : ℝ) in a..b, f (-x) = ∫ (x : ℝ) in -b..-a, f x
<VAR>K : Type u_1<VAR>inst✝⁷ : DivisionRing K<VAR>inst✝⁶ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : T1Space 𝕜<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : HasContinuousInv₀ 𝕜<VAR>inst✝ : ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq : EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<GOAL>EqOn f g S ∨ EqOn f (-g) S
<VAR>K : Type u_1<VAR>inst✝⁷ : DivisionRing K<VAR>inst✝⁶ : TopologicalSpace K<VAR>α : Type u_2<VAR>𝕜 : Type u_3<VAR>f g : α → 𝕜<VAR>S : Set α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : T1Space 𝕜<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : HasContinuousInv₀ 𝕜<VAR>inst✝ : ContinuousMul 𝕜<VAR>hS : IsPreconnected S<VAR>hf : ContinuousOn f S<VAR>hg : ContinuousOn g S<VAR>hsq✝ : EqOn (f ^ 2) (g ^ 2) S<VAR>hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0<VAR>hsq : EqOn ((f / g) ^ 2) 1 S<GOAL>EqOn f g S ∨ EqOn f (-g) S
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>(lift R) (⇑g ∘ ι R) = g
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>X : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>g : FreeAlgebra R X →ₐ[R] A<GOAL>(lift R) ((lift R).symm g) = g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝¹ : LinearOrderedAddCommGroupWithTop Γ₀<VAR>inst✝ : Ring R<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>h : v x < v y<GOAL>v (x + y) = v x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>Compatibility.τ₀.hom.app K = (Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀).hom.app K
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>Preadditive.DoldKan.equivalence.counitIso.hom.app ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) = Preadditive.DoldKan.equivalence.functor.map (isoΓ₀.hom.app K) ≫ isoN₁.hom.app (Γ.obj K) ≫ N₁Γ₀.hom.app K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : 1 < s.encard<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : 1 < s.encard<VAR>a : α<VAR>h' : ∀ b ∈ s, b = a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : 1 < s.encard<VAR>a : α<VAR>h' : ∀ b ∈ s, b = a<VAR>b b' : α<VAR>hb : b ∈ s<VAR>hb' : b' ∈ s<VAR>hne : b ≠ b'<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : β → ℝ≥0<GOAL>∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : β → ℝ≥0<VAR>h : ∑' (b : β), ↑(f b) ≠ ⊤<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : β → ℝ≥0<VAR>a : ℝ≥0<VAR>ha : ↑a = ∑' (b : β), ↑(f b)<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : β → ℝ≥0<VAR>a : ℝ≥0<VAR>ha : ↑a = ∑' (b : β), ↑(f b)<GOAL>HasSum (fun a => ↑(f a)) ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : β → ℝ≥0<VAR>a : ℝ≥0<VAR>ha : ↑a = ∑' (b : β), ↑(f b)<GOAL>HasSum (fun a => ↑(f a)) (∑' (b : β), ↑(f b))
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F proj<VAR>x✝ : Z<VAR>e' : Trivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>e : Trivialization F proj<VAR>b : B<VAR>h : b ∈ e.baseSet<VAR>x : F<GOAL>e.coordChange e b x = x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K : Cofork I.fstSigmaMap I.sndSigmaMap<GOAL>((I.ofSigmaCoforkFunctor ⋙ I.toSigmaCoforkFunctor).obj K).π ≫ (Iso.refl ((I.ofSigmaCoforkFunctor ⋙ I.toSigmaCoforkFunctor).obj K).pt).hom = ((𝟭 (Cofork I.fstSigmaMap I.sndSigmaMap)).obj K).π
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K : Cofork I.fstSigmaMap I.sndSigmaMap<GOAL>∀ (j : Discrete I.R), colimit.ι (Discrete.functor I.right) j ≫ ((I.ofSigmaCoforkFunctor ⋙ I.toSigmaCoforkFunctor).obj K).π ≫ (Iso.refl ((I.ofSigmaCoforkFunctor ⋙ I.toSigmaCoforkFunctor).obj K).pt).hom = colimit.ι (Discrete.functor I.right) j ≫ ((𝟭 (Cofork I.fstSigmaMap I.sndSigmaMap)).obj K).π
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K : Cofork I.fstSigmaMap I.sndSigmaMap<VAR>j : I.R<GOAL>colimit.ι (Discrete.functor I.right) { as := j } ≫ Sigma.desc (Multicofork.ofSigmaCofork I K).π ≫ 𝟙 K.pt = colimit.ι (Discrete.functor I.right) { as := j } ≫ K.π
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K : Cofork I.fstSigmaMap I.sndSigmaMap<VAR>j : I.R<GOAL>(Multicofork.ofSigmaCofork I K).π j = colimit.ι (Discrete.functor I.right) { as := j } ≫ K.π
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a ≤ 1 / b ↔ b ≤ 1 / a
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u₁<VAR>inst✝² : Category.{v₁, u₁} D<VAR>inst✝¹ : Preadditive D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>biproduct.ι (fun i => F.obj ((embedding C).obj (M.X i))) i ≫ (biproduct.desc fun j => F.map (biproduct.ι (fun i => (embedding C).obj (M.X i)) j)) ≫ F.map (biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) = F.map (biproduct.ι (fun i => (embedding C).obj (M.X i)) i ≫ biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel α γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((κ ×ₖ η) a) s = ∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>p : R[X]<VAR>k : ℕ<GOAL>(matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>p : R[X]<VAR>k : ℕ<GOAL>∀ (p q : R[X]), (matPolyEquiv (stdBasisMatrix i j p)).coeff k = stdBasisMatrix i j (p.coeff k) → (matPolyEquiv (stdBasisMatrix i j q)).coeff k = stdBasisMatrix i j (q.coeff k) → (matPolyEquiv (stdBasisMatrix i j (p + q))).coeff k = stdBasisMatrix i j ((p + q).coeff k)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>i j : n<VAR>p : R[X]<VAR>k : ℕ<GOAL>∀ (n_1 : ℕ) (a : R), (matPolyEquiv (stdBasisMatrix i j ((monomial n_1) a))).coeff k = stdBasisMatrix i j (((monomial n_1) a).coeff k)
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑r ≤ 1 ↔ r ≤ 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>l m : List α<VAR>o : Ordinal.{u}<VAR>hl : Sorted (fun x x_1 => x > x_1) l<VAR>hm : Sorted (fun x x_1 => x > x_1) m<VAR>hlt : ∀ i ∈ l, Ordinal.typein (fun x x_1 => x < x_1) i < o<VAR>hmltl : Lex (fun x x_1 => x < x_1) m l<GOAL>∀ i ∈ m, Ordinal.typein (fun x x_1 => x < x_1) i < o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : OrderedCommSemiring α<VAR>inst✝² : StrictOrderedSemiring β<VAR>inst✝¹ : Algebra α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>a a₁✝ a₂✝ a₁ a₂ : α<VAR>ha : a₁ < a₂<GOAL>(algebraMap α β) a₁ < (algebraMap α β) a₂
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>|(o.areaForm x) y| = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>∏ i : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Pairwise fun i j => ⟪![x, y] i, ![x, y] j⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ : 𝕜 → E<VAR>a✝ b✝ : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>a b : 𝕜<GOAL>(b - a) • dslope f a b = f b - f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<GOAL>WellFoundedGT ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<GOAL>WellFoundedGT ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<GOAL>↑n.succ ≤ s.chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<VAR>i : α<VAR>h : i ∈ map Subtype.val (ofFn fun i => f ↑i)<GOAL>i ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<VAR>this : IsTrans { x // x ∈ s } fun x x_1 => x < x_1<VAR>n : ℕ<VAR>hn : ↑n = s.chainHeight<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1<GOAL>↑n.succ ≤ ↑(map Subtype.val (ofFn fun i => f ↑i)).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f✝ g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : univ ⊆ s ∪ t<VAR>hc : StronglyMeasurable fun a => f ↑a<VAR>hd : StronglyMeasurable fun a => f ↑a<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : Countable ι<VAR>f✝ g : α → β<VAR>m : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>h : univ ⊆ s ∪ t<VAR>hc : StronglyMeasurable fun a => f ↑a<VAR>hd : StronglyMeasurable fun a => f ↑a<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<GOAL>Function.extend Subtype.val (fun x => f ↑x) (Function.extend Subtype.val (fun x => f ↑x) fun x => default) = f
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>(foldl (fun l x => { down := l.down + 1 }) { down := 0 } xs).down = (toList xs).length
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>(List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } (toList xs)).down = (toList xs).length
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<VAR>ys : List α<GOAL>(List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<VAR>ys : List α<GOAL>(List.foldl (fun l x => { down := l.down + 1 }) { down := 0 } ys).down = ys.length + 0
<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>s : Set E<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y
<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∫ (x : ℂ), rexp (-‖x‖ ^ p) = π * Real.Gamma (2 / p + 1)
<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>∫ (x : ℂ), rexp (-‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-‖x‖ ^ p)
<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma ((0 + 2) / p)
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>a b : α<VAR>h : ¬R b a<GOAL>destutter' R b (a :: l) = destutter' R b l
<VAR>k : ℕ<GOAL>riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝³ : L.IsOrdered<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : LE M<VAR>inst✝ : L.OrderedStructure M<VAR>a b : M<GOAL>RelMap leSymb ![a, b] ↔ a ≤ b
<VAR>L : Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>inst✝³ : L.IsOrdered<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : LE M<VAR>inst✝ : L.OrderedStructure M<VAR>a b : M<GOAL>RelMap (L.orderLHom.onRelation leSymb) ![a, b] ↔ a ≤ b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<GOAL>Multiset.count x p.roots ≤ 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<GOAL>rootMultiplicity x p ≤ 1
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<GOAL>∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<GOAL>∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<GOAL>∀ x ∈ Ico a b, ‖f' x - g' x‖ ≤ ↑K * ‖f x - g x‖ + (εf + εg)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<VAR>t : ℝ<VAR>ht : t ∈ Ico a b<GOAL>‖f' t - g' t‖ ≤ ↑K * ‖f t - g t‖ + (εf + εg)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<VAR>t : ℝ<VAR>ht : t ∈ Ico a b<VAR>this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))<GOAL>‖f' t - g' t‖ ≤ ↑K * ‖f t - g t‖ + (εf + εg)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv✝ : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<VAR>t : ℝ<VAR>ht : t ∈ Ico a b<VAR>this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))<VAR>hv : dist (v t (f t)) (v t (g t)) ≤ ↑K * dist (f t) (g t)<GOAL>dist (f' t) (g' t) ≤ ↑K * dist (f t) (g t) + (εf + εg)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv✝ : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Icc a b)<VAR>hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t<VAR>f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Icc a b)<VAR>hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t<VAR>g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Ico a b, g t ∈ s t<VAR>ha : ‖f a - g a‖ ≤ δ<VAR>h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t<VAR>t : ℝ<VAR>ht : t ∈ Ico a b<VAR>this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))<VAR>hv : dist (v t (f t)) (v t (g t)) ≤ ↑K * dist (f t) (g t)<GOAL>εf + εg + ↑K * dist (f t) (g t) ≤ ↑K * dist (f t) (g t) + (εf + εg)
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<GOAL>(q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<GOAL>(q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
<VAR>q r : ℚ<VAR>s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den<GOAL>(q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den