ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : MvPolynomial σ R<GOAL>(p.support.sup fun s => toMultiset s) = p.degrees
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑e) s x = e
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderiv 𝕜 (⇑e) x = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f g : β → α<VAR>u₁ u₂ : α<VAR>s : Multiset β<VAR>a : β<VAR>b : Multiset β<VAR>h : fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))<GOAL>fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) (a ::ₘ b)) = op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>¬s.Nonempty ∨ ¬t.Nonempty ↔ s = ∅ ∨ t = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommSemiring R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1140245) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ cfcₙ f a ↔ ∀ x ∈ σₙ R a, 0 ≤ f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommSemiring R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(∀ (x : ↑(σₙ R a)), 0 x ≤ { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔ ∀ x ∈ σₙ R a, 0 ≤ f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommSemiring R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>h0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(∀ (a_1 : R) (b : a_1 ∈ σₙ R a), 0 ⟨a_1, b⟩ ≤ f a_1) ↔ ∀ x ∈ σₙ R a, 0 ≤ f x
<VAR>f✝ : Ordinal.{u} → Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>H : IsNormal f<VAR>a : Ordinal.{u_1}<GOAL>f a = a ↔ ∃ o, deriv f o = a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C<VAR>J : Type<VAR>hJ : SmallCategory J<VAR>hhJ : FinCategory J<VAR>this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C<VAR>l : J ≌ ULiftHom (ULift.{?u.1062, 0} J)<GOAL>HasLimitsOfShape J C
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<VAR>a✝ : Nontrivial α<GOAL>p.count m.factors ≠ 0 → p ≤ m
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<VAR>a✝ : Nontrivial α<GOAL>0 < p.count m.factors → p ≤ m
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<VAR>a✝ : Nontrivial α<VAR>h : 0 < p.count m.factors<GOAL>p ≤ m
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<VAR>a✝ : Nontrivial α<VAR>h : 0 < p.count m.factors<GOAL>p ^ 1 ≤ m
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<VAR>a✝ : Nontrivial α<VAR>h : 0 < p.count m.factors<GOAL>1 ≤ p.count m.factors
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>this : IsUnit ((Ideal.Quotient.mk ⊥.jacobson) a)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>y : R ⧸ ⊥.jacobson<VAR>h1 : (Ideal.Quotient.mk ⊥.jacobson) a * y = 1<VAR>h2 : y * (Ideal.Quotient.mk ⊥.jacobson) a = 1<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>y : R<VAR>h1 : (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) y = 1<VAR>h2 : (Ideal.Quotient.mk ⊥.jacobson) y * (Ideal.Quotient.mk ⊥.jacobson) a = 1<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>y : R<VAR>h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)<VAR>h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>y : R<VAR>h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)<VAR>h1 : IsUnit ((a * y - 1) * 1 + 1)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>h✝ : I ≤ ⊥.jacobson<VAR>a : R<VAR>h : IsUnit ((Ideal.Quotient.mk I) a)<VAR>y : R<VAR>h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)<VAR>h1 : IsUnit a ∧ IsUnit y<GOAL>IsUnit a
<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>hn : Nonempty ι<VAR>f g : PushoutI φ →* K<VAR>h : ∀ (i : ι), f.comp (of i) = g.comp (of i)<GOAL>f.comp (base φ) = g.comp (base φ)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u✝ : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>u : Finset ι<VAR>i : ℕ<VAR>x : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>h : ∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s<GOAL>iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
<VAR>x : ℝ<VAR>hx₀ : 0 ≤ x<VAR>hx : x ≤ π / 2<GOAL>1 - 2 / π * x ≤ cos x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s✝ : Set M<VAR>f✝ : SmoothPartitionOfUnity ι I M s✝<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s<VAR>x₀ : E<VAR>g : ι → E → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContDiffAt ℝ n (g i) x₀<GOAL>ContDiffAt ℝ n (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>s✝ : Set M<VAR>f✝ : SmoothPartitionOfUnity ι I M s✝<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s<VAR>x₀ : E<VAR>g : ι → E → F<VAR>hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) n (g i) x₀<GOAL>ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) n (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>m : Type u_8<VAR>n : Type u_9<VAR>inst✝ : Fintype n<VAR>A B : Matrix m n 𝕜<VAR>i j : m<GOAL>⟪(WithLp.equiv 2 (n → 𝕜)).symm (A i), (WithLp.equiv 2 (n → 𝕜)).symm (B j)⟫_𝕜 = (B * Aᴴ) j i
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>I.target = range ↑I
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>I.target = ↑I '' I.source
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : CommRing α<VAR>n k : ℕ<GOAL>∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : CommRing α<VAR>n k : ℕ<GOAL>∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : CommRing α<VAR>n k : ℕ<VAR>hkn : k ≤ n<GOAL>∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : CommRing α<VAR>n k : ℕ<VAR>hnk : n < k<GOAL>∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<GOAL>¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p
<VAR>f : StieltjesFunction<VAR>a b : ℝ<GOAL>f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : b ≤ a<GOAL>f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>hab : a < b<GOAL>f.measure (Ioo a b) = ofReal (leftLim (↑f) b - ↑f a)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>h_meas : NullMeasurableSet s μ<VAR>h_exists : ∀ (x : α), ∃! g, g • x ∈ s<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hxa : x ∈ (fun g => g • s) a<VAR>hxb : x ∈ (fun g => g • s) b<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : MulAction G α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction H β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>h_meas : NullMeasurableSet s μ<VAR>h_exists : ∀ (x : α), ∃! g, g • x ∈ s<VAR>a b : G<VAR>hab : a ≠ b<VAR>x : α<VAR>hxa : a⁻¹ • x ∈ s<VAR>hxb : b⁻¹ • x ∈ s<GOAL>False
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>x : G<VAR>n✝ : ℕ<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n % ↑(Nat.card G)) = a ^ n
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<GOAL>finrank k ↥(vectorSpan k (insert p s)) ≤ finrank k ↥(vectorSpan k s) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<GOAL>finrank k ↥(vectorSpan k (insert p ↑(affineSpan k s))) ≤ finrank k ↥(vectorSpan k s) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<GOAL>finrank k ↥(affineSpan k s).direction ≤ finrank k ↥(vectorSpan k s)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>s : S<VAR>t : (ι →₀ M) ⊗[R] N<GOAL>(finsuppLeft R M N ι) (s • t) = s • (finsuppLeft R M N ι) t
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = if n + 1 = 0 then 1 else 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<VAR>H : ∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1 = 1<GOAL>∑ k ∈ antidiagonal (n + 1), ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<VAR>H : ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 + ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 = 1<GOAL>↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 + ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 = 0
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<VAR>H : ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 + ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 = 1<GOAL>∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 = 0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<VAR>H : ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 + ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 = 1<GOAL>∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli x.1 = ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<VAR>h₁ : (1, n) ∈ antidiagonal n.succ<VAR>h₂ : ↑n + 1 ≠ 0<VAR>h₃ : (1 + n).choose n = n + 1<VAR>H : ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 + ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 = 1<GOAL>0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 = 1 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1
<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>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>hG : Group.IsNilpotent G<GOAL>∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
<VAR>d : ℤ<VAR>h₀ : 0 ≤ d<VAR>a : Solution₁ d<VAR>hx : a.x = 0<GOAL>False
<VAR>d : ℤ<VAR>h₀ : 0 ≤ d<VAR>a : Solution₁ d<VAR>hx : a.x = 0<VAR>h : 0 ≤ d * a.y ^ 2<GOAL>False
<VAR>d : ℤ<VAR>h₀ : 0 ≤ d<VAR>a : Solution₁ d<VAR>hx : a.x = 0<VAR>h : 0 ≤ -1<GOAL>False
<VAR>n : ℕ<GOAL>(bit true n).fastFibAux = let p := n.fastFibAux; (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
<VAR>n : ℕ<GOAL>(if true = true then ((binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 ^ 2 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 ^ 2, (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 * (2 * (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2)) else ((binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 * (2 * (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 - (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1), (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).2 ^ 2 + (binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n).1 ^ 2)) = let p := binaryRec (fib 0, fib 1) (fun b x p => if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)) n; (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
<VAR>n : ℕ<GOAL>(if false = true then ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2)) else ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) = (fib 0, fib 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))