ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>s : Set α<VAR>f : α → β<GOAL>Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹³ : RingHomInvPair σ σ'<VAR>inst✝¹² : RingHomInvPair σ' σ<VAR>inst✝¹¹ : RingHomIsometric σ<VAR>inst✝¹⁰ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜' F✝<VAR>f✝ : E →SL[σ] F✝<VAR>inst✝⁵ : CompleteSpace F✝<VAR>inst✝⁴ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E →L[𝕜] F<VAR>G : Submodule 𝕜 F<VAR>h : IsCompl (LinearMap.range f) G<VAR>inst✝ : CompleteSpace ↥G<VAR>hker : LinearMap.ker f = ⊥<GOAL>LinearMap.range f = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹³ : RingHomInvPair σ σ'<VAR>inst✝¹² : RingHomInvPair σ' σ<VAR>inst✝¹¹ : RingHomIsometric σ<VAR>inst✝¹⁰ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜' F✝<VAR>f✝ : E →SL[σ] F✝<VAR>inst✝⁵ : CompleteSpace F✝<VAR>inst✝⁴ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E →L[𝕜] F<VAR>G : Submodule 𝕜 F<VAR>h : IsCompl (LinearMap.range f) G<VAR>inst✝ : CompleteSpace ↥G<VAR>hker : LinearMap.ker f = ⊥<GOAL>LinearMap.range f = LinearMap.range ↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F' →L[ℝ] F<VAR>f : α →ₛ F'<GOAL>∑ x ∈ f.range, ‖(T (↑f ⁻¹' {x})) x‖ ≤ ∑ x ∈ f.range, ‖T (↑f ⁻¹' {x})‖ * ‖x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F' →L[ℝ] F<VAR>f : α →ₛ F'<VAR>b : F'<VAR>x✝ : b ∈ f.range<GOAL>‖(T (↑f ⁻¹' {b})) b‖ ≤ ‖T (↑f ⁻¹' {b})‖ * ‖b‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>a * b⁻¹ < c ↔ a < b * c
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>((monomial s) a).degrees ≤ toMultiset s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>adj3 : F ⊣ G''<VAR>x : D<GOAL>(adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x = (adj1.rightAdjointUniq adj3).hom.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F ⊣ G'<VAR>adj3 : F ⊣ G''<VAR>x : D<GOAL>(adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x = ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q✝ R✝ : Prop<VAR>inst✝² : Decidable P<VAR>inst✝¹ : Decidable Q✝<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<VAR>Q : P → Prop<VAR>R : ¬P → Prop<VAR>inst✝ : Decidable P<GOAL>dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>f : α → WSeq β<VAR>g : β → WSeq γ<GOAL>(s.bind f).bind g ~ʷ s.bind fun x => (f x).bind g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>f : α → WSeq β<VAR>g : β → WSeq γ<GOAL>(map (map g) (map f s)).join.join ~ʷ (map (fun x => (map g (f x)).join) s).join
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>f : α → WSeq β<VAR>g : β → WSeq γ<GOAL>(map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Abelian C<VAR>K : ChainComplex C ℕ<VAR>X : C<VAR>φ : K.X 0 ⟶ X<VAR>inst✝ : HomologicalComplex.HasHomology K 0<VAR>hφ✝ : K.d 1 0 ≫ φ = 0<VAR>hφ : K.d ((ComplexShape.down ℕ).prev 0) 0 ≫ φ = 0<VAR>α : HomologicalComplex.sc K 0 ⟶ ShortComplex.mk 0 0 ⋯ := { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }<GOAL>IsIso (HomologicalComplex.descOpcycles K φ ((ComplexShape.down ℕ).prev 0) ⋯ hφ) ↔ (ShortComplex.mk (K.d ((ComplexShape.down ℕ).prev 0) 0) φ hφ).Exact ∧ Epi φ
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>M : Matroid α<GOAL>{I | M.Indep I} = ↑(lowerClosure {B | M.Base B})
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>M : Matroid α<GOAL>{I | ∃ B, M.Base B ∧ I ⊆ B} = ↑(lowerClosure {B | M.Base B})
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<GOAL>n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ofSuppBddBelow f ⋯ = 0<GOAL>n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ¬ofSuppBddBelow f ⋯ = 0<GOAL>n ≤ if h : ofSuppBddBelow f ⋯ = 0 then 0 else ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ¬ofSuppBddBelow f ⋯ = 0<GOAL>n ≤ ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ¬ofSuppBddBelow f ⋯ = 0<GOAL>∀ b ∈ (ofSuppBddBelow f ⋯).support, n ≤ b
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ¬ofSuppBddBelow f ⋯ = 0<VAR>m : Γ<VAR>hm : m ∈ (ofSuppBddBelow f ⋯).support<GOAL>n ≤ m
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<VAR>h : ¬ofSuppBddBelow f ⋯ = 0<VAR>m : Γ<VAR>hm : ¬(ofSuppBddBelow f ⋯).coeff m = 0<GOAL>n ≤ m
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>C : ℝ<VAR>f g : α →C₀ β<GOAL>IsClosed (range toBCF)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>C : ℝ<VAR>f✝ g : α →C₀ β<VAR>f : α →ᵇ β<VAR>hf : ClusterPt f (𝓟 (range toBCF))<GOAL>f ∈ range toBCF
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>C : ℝ<VAR>f✝ g : α →C₀ β<VAR>f : α →ᵇ β<VAR>hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty<GOAL>f ∈ range toBCF
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetricSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroAtInftyContinuousMapClass F α β<VAR>C : ℝ<VAR>f✝ g : α →C₀ β<VAR>f : α →ᵇ β<VAR>hf : ∀ U ∈ 𝓝 f, (U ∩ range toBCF).Nonempty<VAR>this : Tendsto (⇑f) (cocompact α) (𝓝 0)<GOAL>f ∈ range toBCF
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>e₃ : A₃ ≃ₐ[R] A₃'<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₃<VAR>x✝ : A₁'<GOAL>((e₁.arrowCongr e₃) (g.comp f)) x✝ = (((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)) x✝
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>e₃ : A₃ ≃ₐ[R] A₃'<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₃<VAR>x✝ : A₁'<GOAL>↑e₃ (g (f (↑e₁.symm x✝))) = ↑e₃ (g (↑e₂.symm (↑e₂ (f (↑e₁.symm x✝)))))
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e : A₁ ≃ₐ[R] A₂<VAR>e₁ : A₁ ≃ₐ[R] A₁'<VAR>e₂ : A₂ ≃ₐ[R] A₂'<VAR>e₃ : A₃ ≃ₐ[R] A₃'<VAR>f : A₁ →ₐ[R] A₂<VAR>g : A₂ →ₐ[R] A₃<VAR>x✝ : A₁'<GOAL>f (↑e₁.symm x✝) = ↑e₂.symm (↑e₂ (f (↑e₁.symm x✝)))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y<VAR>g₁ g₂ : Π₀ (i : ι), β₁ i<VAR>i✝ : ι<GOAL>(mapRange f hf (g₁ + g₂)) i✝ = (mapRange f hf g₁ + mapRange f hf g₂) i✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace β<VAR>x y : β<VAR>h : y ∈ measurableAtom x<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hxs : x ∈ s<GOAL>y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace β<VAR>x y : β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hxs : x ∈ s<VAR>h : ∀ (i : Set β), x ∈ i → MeasurableSet i → y ∈ i<GOAL>y ∈ s
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B : C<VAR>c₁✝ c₂✝ : BinaryCofan A B<VAR>hc₁✝ : IsColimit c₁✝<VAR>hc₂✝ : IsColimit c₂✝<VAR>c₁ c₂ : BinaryCofan A B<VAR>hc₁ : IsColimit c₁<VAR>hc₂ : IsColimit c₂<VAR>x✝ : Mono c₁.inl<GOAL>Mono c₂.inl
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝¹ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>J : Type u_4<VAR>inst✝ : Fintype J<VAR>i : J ≃ I<GOAL>CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (hurwitzZetaEven (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : HasSum (fun i => s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)<GOAL>HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDeriv 𝕜 n f x) m = (∏ i : Fin n, m i) • iteratedDeriv n f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDeriv 𝕜 n f x) m = (iteratedFDeriv 𝕜 n f x) fun i => m i • 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α →. σ<VAR>h : α → ℕ × σ →. σ<VAR>hf : Computable f<VAR>hg : Partrec g<VAR>hh : Partrec₂ h<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<VAR>m : ℕ<VAR>IH : Nat.rec (Part.map encode (g a)) (fun y IH => IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) m = Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)<GOAL>((Nat.rec (Part.map encode (g a)) (fun y IH => IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) m).bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) = (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α →. σ<VAR>h : α → ℕ × σ →. σ<VAR>hf : Computable f<VAR>hg : Partrec g<VAR>hh : Partrec₂ h<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<VAR>m : ℕ<VAR>IH : Nat.rec (Part.map encode (g a)) (fun y IH => IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) m = Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)<GOAL>((Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) = (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α →. σ<VAR>h : α → ℕ × σ →. σ<VAR>hf : Computable f<VAR>hg : Partrec g<VAR>hh : Partrec₂ h<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<VAR>m : ℕ<VAR>IH : Nat.rec (Part.map encode (g a)) (fun y IH => IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) m = Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)<GOAL>(fun y => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) = fun y => Part.map encode (h a (m, y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α →. σ<VAR>h : α → ℕ × σ →. σ<VAR>hf : Computable f<VAR>hg : Partrec g<VAR>hh : Partrec₂ h<VAR>n : ℕ<VAR>a : α<VAR>e : decode n = Option.some a<VAR>m : ℕ<VAR>IH : Nat.rec (Part.map encode (g a)) (fun y IH => IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) m = Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)<VAR>s : σ<GOAL>((↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode s)))).bind fun a => Part.map encode (h a.1 a.2)) = Part.map encode (h a (m, s))
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g✝ : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>‖f v‖ ≤ ‖f‖ * ‖v‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g✝ : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>v : V₁<GOAL>‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * ‖f‖ * ‖v‖
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : SemilatticeSup α<VAR>f : α → X<GOAL>(∀ (ib : Set X), x ∈ ib ∧ IsOpen ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ ib) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points = (univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)<VAR>k : ZMod (minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>↑((toEquiv ⋯) (g ^ k.cast • Quotient.out' q)) = if k = 0 then g ^ minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) else g ^ k.cast * Quotient.out' (Quotient.out' q)
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : G<VAR>q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)<VAR>k : ZMod (minimalPeriod (fun x => g • x) (Quotient.out' q))<GOAL>(g ^ if k = 0 then ↑(minimalPeriod (fun x => g • x) (Quotient.out' ⟨q, k - 1⟩.fst)) else k.cast) * Quotient.out' (Quotient.out' ⟨q, k - 1⟩.fst) = if k = 0 then g ^ minimalPeriod (fun x => g • x) (Quotient.out' q) * Quotient.out' (Quotient.out' q) else g ^ k.cast * Quotient.out' (Quotient.out' q)
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<VAR>h✝ : IsEmpty ι<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>inst✝¹ : CompleteLinearOrder δ<VAR>inst✝ : ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x<VAR>h✝ : Nonempty ι<GOAL>LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_5, u_2} D<VAR>inst✝² : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E E' : L.RightExtension F<VAR>X : C<VAR>h : E.IsPointwiseRightKanExtensionAt (L.obj X)<VAR>inst✝¹ : L.Full<VAR>inst✝ : L.Faithful<GOAL>IsIso (E.hom.app X)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>A B : C<VAR>hB : B ∈ i.essImage<VAR>f : i.obj ((reflector i).obj A) ⟶ B<GOAL>(unitCompPartialBijective A hB).symm f = (reflectorAdjunction i).unit.app A ≫ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>I : Type u_3<VAR>f : I → Type u_4<VAR>i' : I<VAR>inst : ∀ (i : I), Nonempty (f i)<VAR>inst✝ : Nontrivial (f i')<VAR>this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)<GOAL>Nontrivial ((i : I) → f i)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.195705}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Injective f<GOAL>lift.{v, u} #α ≤ lift.{u, v} #β
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.195705}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Injective f<GOAL>lift.{u, v} #↑(range f) ≤ lift.{u, v} #β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<GOAL>MeasurableSet (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>this : t n = ⋃ u ∈ memPartition t n, u ∩ t n<GOAL>MeasurableSet (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>this : t n = ⋃ u ∈ memPartition t n, u ∩ t n<GOAL>MeasurableSet (⋃ u ∈ memPartition t n, u ∩ t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>this : t n = ⋃ u ∈ memPartition t n, u ∩ t n<VAR>v : Set α<VAR>hv : v ∈ memPartition t n<GOAL>MeasurableSet (v ∩ t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>this : t n = ⋃ u ∈ memPartition t n, u ∩ t n<VAR>v : Set α<VAR>hv : v ∈ memPartition t n<GOAL>v ∩ t n ∈ memPartition t (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : ℕ → Set α<VAR>n : ℕ<VAR>this : t n = ⋃ u ∈ memPartition t n, u ∩ t n<VAR>v : Set α<VAR>hv : v ∈ memPartition t n<GOAL>v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>x y z : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>(C x * X ^ k + C y * X ^ m + C z * X ^ n).support.card = 3