ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>(Q.lift ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (e.invFunIdAssoc G).hom)).obj (Cone.whisker e.inverse s)) ≫ P.lift ((Cones.postcompose w.hom).obj (Cone.whisker e.functor t))) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>s.π.app (e.inverse.obj (e.functor.obj j)) ≫ w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<GOAL>s.π.app (e.inverse.obj (e.functor.obj j)) ≫ w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<VAR>l : w.hom.app j = w.hom.app ((𝟭 J).obj j)<GOAL>s.π.app (e.inverse.obj (e.functor.obj j)) ≫ w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<VAR>j : J<VAR>l : w.hom.app j = w.hom.app ((𝟭 J).obj j)<GOAL>s.π.app (e.inverse.obj (e.functor.obj j)) ≫ w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ w.hom.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.unitInv.app j) = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t) ≫ Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s) = 𝟙 t.pt
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F✝ : J ⥤ C<VAR>t✝ : Cone F✝<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>G : K ⥤ C<VAR>t : Cone G<VAR>P : IsLimit s<VAR>Q : IsLimit t<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G<GOAL>∀ (j : K), (P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t) ≫ Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s)) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q : ℝ≥0<VAR>p : ℝ<GOAL>1 ≤ ENNReal.ofReal p ↔ 1 ≤ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>this : HasSum (fun n => C * r ^ n) (C / (1 - r))<GOAL>dist (f n) a ≤ C * r ^ n / (1 - r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>this : HasSum (fun n => C * r ^ n) (C / (1 - r))<GOAL>C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>this : HasSum (fun n => C * r ^ n) (C / (1 - r))<GOAL>C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>r C : ℝ<VAR>hr : r < 1<VAR>f : ℕ → α<VAR>hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<VAR>this : HasSum (fun n => C * r ^ n) (C / (1 - r))<GOAL>r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α✝<VAR>g g₁ g₂ : Filter β<VAR>m : α✝ → β<VAR>m' : β → γ<VAR>s✝ : Set α✝<VAR>t✝ : Set β<VAR>α : Type u_2<VAR>s : Set α<VAR>t : Set ↑s<GOAL>𝓟 t = comap Subtype.val (𝓟 (Subtype.val '' t))
<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 : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<VAR>i : ℕ<GOAL>(p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq β<VAR>f g : α →. β<VAR>inst✝¹ : (x : α) → Decidable (f x).Dom<VAR>inst✝ : (x : α) → Decidable (g x).Dom<VAR>t : Finset α<VAR>b : β<VAR>h₂ : ∀ x ∈ t, f x = g x<VAR>y : β<GOAL>y ∈ pimage f t ↔ y ∈ pimage g t
<VAR>p q : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>h₂ : d₂ ≠ 0<GOAL>divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁
<VAR>p q : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>h₂ : d₂ ≠ 0<GOAL>↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁
<VAR>p q : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>h₂ : d₂ ≠ 0<GOAL>↑n₁ * ↑d₂ = ↑n₂ * ↑d₁ ↔ n₁ * d₂ = n₂ * d₁
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>ha : ¬Polynomial.eval a F = 0<GOAL>∃ z, Polynomial.eval z F = 0 ∧ ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A✝ : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : AddMonoidWithOne B<VAR>inst✝² : FunLike F ℕ A✝<VAR>inst✝¹ : AddMonoidWithOne A✝<VAR>A : Type u_6<VAR>inst✝ : AddMonoidWithOne A<GOAL>∀ (n : ℕ), n • 1 = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A✝ : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : AddMonoidWithOne B<VAR>inst✝² : FunLike F ℕ A✝<VAR>inst✝¹ : AddMonoidWithOne A✝<VAR>A : Type u_6<VAR>inst✝ : AddMonoidWithOne A<VAR>f : ℕ →+ A := { toFun := fun n => n • 1, map_zero' := ⋯, map_add' := ⋯ }<GOAL>∀ (n : ℕ), n • 1 = ↑n
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : PerfectField E<VAR>eq : perfectClosure F E = ⊥<VAR>p : ℕ := ringExpChar F<GOAL>PerfectField F
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : PerfectField E<VAR>eq : perfectClosure F E = ⊥<VAR>p : ℕ := ringExpChar F<VAR>this : ExpChar E p<GOAL>PerfectField F
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : PerfectField E<VAR>eq : perfectClosure F E = ⊥<VAR>p : ℕ := ringExpChar F<VAR>this✝ : ExpChar E p<VAR>this : PerfectRing F p<GOAL>PerfectField F
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : ι → ℕ<VAR>x : ℕ<GOAL>(∏ i : ι, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x
<VAR>m : Type u_1 → Type u_2<VAR>ρ α✝ : Type u_1<VAR>p : α✝ → Prop<VAR>x : ReaderT ρ m α✝<VAR>inst✝ : Monad m<VAR>a : ReaderT ρ m { a // p a }<GOAL>Subtype.val <$> a = x ↔ ∀ (x_1 : ρ), Subtype.val <$> a x_1 = x x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : r ≺i r<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : r ≺i r<VAR>h : r (f.toRelEmbedding f.top) f.top<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>f : r ≺i r<VAR>h : r f.top f.top<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : HeytingAlgebra α<VAR>inst✝² : HeytingAlgebra β<VAR>inst✝¹ : HeytingAlgebra γ<VAR>inst✝ : HeytingAlgebra δ<VAR>f f₁ f₂ : HeytingHom α β<VAR>g g₁ g₂ : HeytingHom β γ<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a \ b) \ (a \ c) ≤ c \ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ a ⊔ (b ⊔ c)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>K : Type u_3<VAR>inst✝ : Group K<VAR>f : G ∗ H →* K<GOAL>f.range = (f.comp inl).range ⊔ (f.comp inr).range
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖
<VAR>v : Multiset ℕ+<VAR>h : ∀ p ∈ v, p.Prime<GOAL>(ofPNatMultiset v h).toPNatMultiset.prod = v.prod
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : ker f = ⊥<GOAL>∃ K > 0, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : ker f = ⊥<VAR>h✝ : Subsingleton E<GOAL>∃ K > 0, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁶ : AddCommGroup F'<VAR>inst✝⁵ : Module 𝕜 F'<VAR>inst✝⁴ : TopologicalSpace F'<VAR>inst✝³ : TopologicalAddGroup F'<VAR>inst✝² : ContinuousSMul 𝕜 F'<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : ker f = ⊥<VAR>h✝ : Nontrivial E<GOAL>∃ K > 0, AntilipschitzWith K ⇑f
<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>n : ℕ<VAR>hn : n ≠ 0<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 n (fun x => c) s x = 0
<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>f✝ : ℝ → E<VAR>a✝ b✝ c d : ℝ<VAR>μ✝ ν : Measure ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>hf : AEStronglyMeasurable f (μ.restrict (Ι a b))<GOAL>IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
<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>f✝ : ℝ → E<VAR>a✝ b✝ c d : ℝ<VAR>μ✝ ν : Measure ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<VAR>hf : AEStronglyMeasurable f (μ.restrict (Ι a b))<GOAL>Integrable (fun t => ‖f t‖) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : StrictMonoOn f (Iic a)<VAR>h₂ : StrictMonoOn f (Ici a)<GOAL>StrictMono f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : StrictMonoOn f (Iic a)<VAR>h₂ : StrictMonoOn f (Ici a)<GOAL>StrictMonoOn f (Iic a ∪ Ici a)
<VAR>M : Type u_1<VAR>inst✝⁴ : Mul M<VAR>inst✝³ : Finite M<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)
<VAR>M : Type u_1<VAR>inst✝⁴ : Mul M<VAR>inst✝³ : Finite M<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)
<VAR>M : Type u_1<VAR>inst✝⁴ : Mul M<VAR>inst✝³ : Finite M<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>↑(Nat.card G) ≠ 0
<VAR>M : Type u_1<VAR>inst✝⁴ : Mul M<VAR>inst✝³ : Finite M<VAR>G : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>0 < ↑(Nat.card (G ⧸ H))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Bornology α<GOAL>cobounded α = ⊥ ↔ BoundedSpace α
<VAR>x y : ℝ<GOAL>cosh (2 * x) = cosh x ^ 2 + sinh x ^ 2
<VAR>x y : ℝ<GOAL>↑(cosh (2 * x)) = ↑(cosh x ^ 2 + sinh x ^ 2)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>(mk' S x₁ y₁ + mk' S x₂ y₂) * (algebraMap R S) ↑(y₁ * y₂) = (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>(algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ = (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>(algebraMap R S) ↑y₁ * ((algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂) * (algebraMap R S) x₂ + (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂ * (algebraMap R S) x₁ * (algebraMap R S) ↑y₂ = ((algebraMap R S) x₁ * (algebraMap R S) ↑y₂ + (algebraMap R S) x₂ * (algebraMap R S) ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
<VAR>s : ℂ<GOAL>LSeriesSummable (fun n => ↑(μ n)) s ↔ 1 < s.re
<VAR>s : ℂ<VAR>H : LSeriesSummable (fun n => ↑(μ n)) s<GOAL>1 < s.re
<VAR>s : ℂ<VAR>n : ℕ<VAR>x✝ : n ≠ 0<GOAL>Complex.abs ↑(μ n) ≤ 1
<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' : δ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f₁ : α → β → β'<VAR>f₂ : α → γ → γ'<VAR>g' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)<VAR>a : α<VAR>ha : a ∈ s<VAR>b : β<VAR>hb : b ∈ t<VAR>c : γ<VAR>hc : c ∈ u<GOAL>g' (f₁ a b) (f₂ a c) ∈ image2 g' (image2 f₁ s t) (image2 f₂ s u)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>p * q %ₘ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>q ∣ p * q
<VAR>S : Set Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>enumOrd S o = sInf (S ∩ {b | ∀ c < o, enumOrd S c < b})
<VAR>S : Set Ordinal.{u}<VAR>o : Ordinal.{u}<GOAL>sInf (S ∩ Ici (o.blsub fun a x => enumOrd S a)) = sInf (S ∩ {b | ∀ c < o, enumOrd S c < b})
<VAR>S : Set Ordinal.{u}<VAR>o x✝ : Ordinal.{u}<GOAL>x✝ ∈ Ici (o.blsub fun a x => enumOrd S a) ↔ x✝ ∈ {b | ∀ c < o, enumOrd S c < b}
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>r : S<GOAL>(X + C r).leadingCoeff = 1
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<GOAL>Absorbent 𝕜 (p.ball x r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<VAR>y : E<VAR>hy : y ∈ p.ball 0 (r - p x)<GOAL>y ∈ p.ball x r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>hpr : p x < r<VAR>y : E<VAR>hy : p y < r - p x<GOAL>y ∈ p.ball x r
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<GOAL>Injective (finsetClopens X)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<GOAL>Injective (((image fun t => t.carrier) ∘ Finset.toSet) ∘ finsetClopens X)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<GOAL>Injective fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>toSetoid✝¹ : Setoid X<VAR>isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹.Rel x))<VAR>toSetoid✝ : Setoid X<VAR>isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝.Rel x))<VAR>h : (fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes) { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } = (fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes) { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }<GOAL>toSetoid✝¹ = toSetoid✝
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>inst✝ : CompactSpace X<VAR>toSetoid✝¹ : Setoid X<VAR>isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹.Rel x))<VAR>toSetoid✝ : Setoid X<VAR>isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝.Rel x))<VAR>h : (fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes) { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } = (fun x => match x with | { toSetoid := f, isOpen_setOf_rel := isOpen_setOf_rel } => f.classes) { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }<GOAL>toSetoid✝¹.classes = toSetoid✝.classes
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : Stream' (Option α)<VAR>al : f.IsSeq<GOAL>(cons a ⟨f, al⟩).tail = ⟨f, al⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>f : Stream' (Option α)<VAR>al : f.IsSeq<GOAL>↑(cons a ⟨f, al⟩).tail = ↑⟨f, al⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<GOAL>((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫ (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫ (X₁ ⊗ X₂) ◁ (β_ X₃ (Y₁ ⊗ Y₂)).hom ▷ Y₃ ≫ (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷ (X₃ ⊗ Y₃) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom = ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫ ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫ X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫ X₁ ◁ (β_ (X₂ ⊗ X₃) Y₁).hom ▷ (Y₂ ⊗ Y₃) ≫ X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫ (X₁ ⊗ Y₁) ◁ ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫ X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)