ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x + r) a = cfc f a + (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f x + r) a = (algebraMap R A) r + cfc f a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => r + f x) a = (algebraMap R A) r + cfc f a
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>C : Type u_1<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>h : IsCyclotomicExtension S A B<VAR>f : B ≃ₐ[A] C<VAR>this : Algebra B C := (↑f).toAlgebra<GOAL>IsCyclotomicExtension S A C
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>C : Type u_1<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>h : IsCyclotomicExtension S A B<VAR>f : B ≃ₐ[A] C<VAR>this✝ : Algebra B C := (↑f).toAlgebra<VAR>this : IsCyclotomicExtension {1} B C<GOAL>IsCyclotomicExtension S A C
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>C : Type u_1<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>h : IsCyclotomicExtension S A B<VAR>f : B ≃ₐ[A] C<VAR>this✝¹ : Algebra B C := (↑f).toAlgebra<VAR>this✝ : IsCyclotomicExtension {1} B C<VAR>this : IsScalarTower A B C<GOAL>IsCyclotomicExtension S A C
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.48727, u_1} C<VAR>inst✝³ : Category.{?u.48731, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>d e : ℤ<VAR>γ : Cochain G K d<VAR>he : 0 + d = e<GOAL>0 + e = d
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.48731, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>d : ℤ<VAR>γ : Cochain G K d<VAR>he : 0 + d = d<GOAL>(Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝¹ : Set α<VAR>v₁ : Trunc ↑s✝¹<VAR>s✝ : Set α<VAR>v₂ : Trunc ↑s✝<VAR>h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s<GOAL>HEq v₁ v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>h : ¬Pairwise (Disjoint on f)<GOAL>∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>h : ¬univ.Pairwise (Disjoint on f)<GOAL>∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>h✝ : ¬univ.Pairwise (Disjoint on f)<VAR>i : ι<VAR>_hi : i ∈ univ<VAR>j : ι<VAR>_hj : j ∈ univ<VAR>h : i ≠ j ∧ ∃ x, x ∈ f i ∩ f j<GOAL>∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a : α<VAR>u : αˣ<GOAL>a /ₚ u = a / ↑u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : OrderedCommSemiring α<VAR>inst✝³ : StrictOrderedSemiring β<VAR>inst✝² : Algebra α β<VAR>inst✝¹ : SMulPosStrictMono α β<VAR>a a₁ a₂ : α<VAR>inst✝ : SMulPosReflectLT α β<GOAL>(algebraMap α β) a₁ < (algebraMap α β) a₂ ↔ a₁ < a₂
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this : IsNoetherian R ↥(torsion R N)<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝ : IsNoetherian R ↥(torsion R N)<VAR>this : Finite R (N ⧸ torsion R N)<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝ : IsNoetherian R ↥(torsion R N)<VAR>this : Finite R (N ⧸ torsion R N)<VAR>I : Type u<VAR>fI : Fintype I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝ : IsNoetherian R ↥(torsion R N)<VAR>this : Finite R (N ⧸ torsion R N)<VAR>I : Type u<VAR>fI : Fintype I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}<VAR>n : ℕ<VAR>g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝¹ : IsNoetherian R ↥(torsion R N)<VAR>this✝ : Finite R (N ⧸ torsion R N)<VAR>I : Type u<VAR>fI : Fintype I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}<VAR>n : ℕ<VAR>g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R<VAR>this : Projective R (N ⧸ torsion R N)<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝¹ : IsNoetherian R ↥(torsion R N)<VAR>this✝ : Finite R (N ⧸ torsion R N)<VAR>I : Type u<VAR>fI : Fintype I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}<VAR>n : ℕ<VAR>g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R<VAR>this : Projective R (N ⧸ torsion R N)<VAR>f : N ⧸ torsion R N →ₗ[R] N<VAR>hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>this✝¹ : IsNoetherian R ↥(torsion R N)<VAR>this✝ : Finite R (N ⧸ torsion R N)<VAR>I : Type u<VAR>fI : Fintype I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}<VAR>n : ℕ<VAR>g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R<VAR>this : Projective R (N ⧸ torsion R N)<VAR>f : N ⧸ torsion R N →ₗ[R] N<VAR>hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id<GOAL>LinearMap.range (torsion R N).subtype = LinearMap.ker (torsion R N).mkQ
<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>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>v : Basis ι 𝕜 E<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
<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>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>v : Basis ι 𝕜 E<VAR>C : ℝ≥0<VAR>hC : C > 0<VAR>h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M<GOAL>∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Unique αˣ<VAR>x✝¹ x✝ : α<GOAL>x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | f w = r}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>h : IsLinearMap 𝕜 f<VAR>r : β<GOAL>Convex 𝕜 {w | f w ≤ r ∧ r ≤ f w}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>dist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<GOAL>(∑ i : Fin (n + 1 + 2), (-1) ^ ↑i • X.δ i) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<GOAL>∑ x ∈ Finset.univ ×ˢ Finset.univ, ((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<GOAL>∑ x ∈ Finset.univ ×ˢ Finset.univ, ((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<GOAL>∑ i ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) = ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<VAR>φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)<GOAL>∑ i ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) = ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<VAR>φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)<GOAL>∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<VAR>φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)<GOAL>∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<VAR>φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)<GOAL>∀ b ∈ Sᶜ, ∃ a, ∃ (ha : a ∈ S), φ a ha = b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X Y : SimplicialObject C<VAR>n : ℕ<VAR>P : Type := Fin (n + 2) × Fin (n + 3)<VAR>S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ<VAR>φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)<GOAL>∀ (a : P) (ha : a ∈ S), ((-1) ^ ↑a.2 • X.δ a.2) ≫ ((-1) ^ ↑a.1 • X.δ a.1) = -((-1) ^ ↑(φ a ha).2 • X.δ (φ a ha).2) ≫ ((-1) ^ ↑(φ a ha).1 • X.δ (φ a ha).1)
<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>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p2) (p4 -ᵥ p2)
<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>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<VAR>left✝ : p2 -ᵥ p3 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p4 -ᵥ p3 = r • (p2 -ᵥ p3)<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p2) (p4 -ᵥ p2)
<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>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<VAR>left✝ : p2 -ᵥ p3 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p4 -ᵥ p3 = r • (p2 -ᵥ p3)<GOAL>InnerProductGeometry.angle (p1 -ᵥ p2) (p4 -ᵥ p2) = InnerProductGeometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2)
<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>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<VAR>left✝ : p2 -ᵥ p3 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p4 -ᵥ p3 = r • (p2 -ᵥ p3)<GOAL>p4 -ᵥ p2 = (-r + 1) • (p3 -ᵥ p2)
<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>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<VAR>left✝ : p2 -ᵥ p3 ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hpr : p4 -ᵥ p3 = r • (p2 -ᵥ p3)<GOAL>p4 -ᵥ p2 = - -(p4 -ᵥ p3) + 1 • -(p2 -ᵥ p3)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>n : Γ<GOAL>((ofPowerSeries Γ R) PowerSeries.X).coeff n = ((single 1) 1).coeff n
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : StrictOrderedSemiring Γ<VAR>n : Γ<GOAL>(embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (toPowerSeries.symm PowerSeries.X)).coeff n = if n = 1 then 1 else 0
<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 s : Set α<GOAL>generateFrom {s} = MeasurableSpace.comap (fun x => x ∈ s) ⊤
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x
<VAR>x : ℂ<GOAL>cexp x = NormedSpace.exp ℂ x
<VAR>x : ℂ<GOAL>(exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
<VAR>x : ℂ<VAR>this : CauSeq.IsComplete ℂ norm<GOAL>(exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>x : α<VAR>y : β<GOAL>r.inv.inv x y ↔ r x y
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ f.domain<GOAL>y = ↑f ⟨x, hx⟩ ↔ (x, y) ∈ f.graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ f.domain<GOAL>y = ↑f ⟨x, hx⟩ ↔ ∃ y_1, ↑y_1 = (x, y).1 ∧ ↑f y_1 = (x, y).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>h1 : ↑⟨x', hx'⟩ = (x, y).1<VAR>h2 : ↑f ⟨x', hx'⟩ = (x, y).2<GOAL>y = ↑f ⟨x, hx⟩
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>x : E<VAR>y : F<VAR>hx : x ∈ f.domain<VAR>x' : E<VAR>hx' : x' ∈ f.domain<VAR>h1 : x' = x<VAR>h2 : ↑f ⟨x', hx'⟩ = y<GOAL>y = ↑f ⟨x, hx⟩
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>x : Localization I.primeCompl<GOAL>IsNilpotent x ↔ x ∈ LocalRing.maximalIdeal (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>x : Localization I.primeCompl<GOAL>(∀ (J : Ideal (Localization I.primeCompl)), J.IsPrime → x ∈ J) ↔ x ∈ LocalRing.maximalIdeal (Localization I.primeCompl)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>AntitoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ AntitoneOn f s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>ι : Type u_3<VAR>F : ι → α → E<VAR>p : Filter ι<VAR>f : α → E<VAR>s : Set α<VAR>Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))<VAR>v : ℝ≥0∞<VAR>hv : v < eVariationOn f s<GOAL>∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>ι : Type u_3<VAR>F : ι → α → E<VAR>p : Filter ι<VAR>f : α → E<VAR>s : Set α<VAR>Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))<VAR>v : ℝ≥0∞<VAR>hv : v < eVariationOn f s<VAR>n : ℕ<VAR>u : ℕ → α<VAR>um : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))<GOAL>∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>ι : Type u_3<VAR>F : ι → α → E<VAR>p : Filter ι<VAR>f : α → E<VAR>s : Set α<VAR>Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))<VAR>v : ℝ≥0∞<VAR>hv : v < eVariationOn f s<VAR>n : ℕ<VAR>u : ℕ → α<VAR>um : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>hlt : v < ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i))<VAR>this : Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))))<GOAL>∀ᶠ (n : ι) in p, v < eVariationOn (F n) s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<GOAL>P.toPoly.degree ≤ 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformSpace.comap f inst✝¹ = inst✝²
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<GOAL>(∀ (s : Set (α × α)), s ∈ comap (fun x => (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<GOAL>∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Subsingleton S<GOAL>∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>hlifts : p ∈ lifts f<VAR>hp : p.Monic<VAR>hR : Nontrivial S<GOAL>∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic