ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>k : κ<VAR>hk : UniformContinuous (⇑UniformFun.ofFun ∘ swap F)<GOAL>UniformContinuous (⇑UniformFun.ofFun ∘ swap F)
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : Nontrivial R<VAR>p : ℕ<VAR>hc : CharP R p<VAR>hp : p = 1<GOAL>1 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>x : M<VAR>y : N<GOAL>(LinearMap.fst R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inr R M N)
<VAR>x : ℂ<GOAL>(log x).im ≤ π
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β<VAR>m : ι → OuterMeasure α<VAR>s : Set β<GOAL>((map f) (⨆ i, m i)) s = (⨆ i, (map f) (m i)) s
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I J : Ideal A<VAR>HI : IsHomogeneous 𝒜 I<VAR>HJ : IsHomogeneous 𝒜 J<GOAL>IsHomogeneous 𝒜 (I ⊔ J)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I J : Ideal A<VAR>HI : ∃ S, I = span (Subtype.val '' S)<VAR>HJ : ∃ S, J = span (Subtype.val '' S)<GOAL>∃ S, I ⊔ J = span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)<GOAL>span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' (s₁ ∪ s₂))
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>s₁ s₂ : Set ↥(homogeneousSubmonoid 𝒜)<GOAL>span (Subtype.val '' s₁) ⊔ span (Subtype.val '' s₂) = span (Subtype.val '' s₁ ∪ Subtype.val '' s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (μ + ν) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (μ + ν) s = (μ + ν) t<GOAL>ν s = ν t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ s t : Set α<VAR>h : (ν + μ) t ≠ ⊤<VAR>h' : s ⊆ t<VAR>h'' : (ν + μ) s = (ν + μ) t<GOAL>ν s = ν t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>i : I<GOAL>A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>i : I<VAR>this : ((preservesLimitIso A (F ⋙ π A)).inv ≫ A.map (limit.π (F ⋙ π A) i)) (liftedConeElement' F) = limit.π ((F ⋙ π A) ⋙ A) i (liftedConeElement' F)<GOAL>A.map (limit.π (F ⋙ π A) i) (liftedConeElement F) = (F.obj i).snd
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : J ⥤ C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>(f ⊗ g).app j ≫ (snd F₁' F₂').app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_1} J<VAR>inst✝¹ : Category.{u_4, u_2} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : J ⥤ C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>(snd F₁ F₂).app j ≫ g.app j = snd (F₁.obj j) (F₂.obj j) ≫ g.app j
<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>φ : G ≃g G'<VAR>v : V<VAR>v' : V'<VAR>C : G.ConnectedComponent<GOAL>G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom C ↔ G.connectedComponentMk v = C
<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>φ : G ≃g G'<VAR>v : V<VAR>v' : V'<VAR>C : G.ConnectedComponent<VAR>u : V<GOAL>G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u) ↔ G.connectedComponentMk v = G.connectedComponentMk u
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Nontrivial R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Module R M'<VAR>v✝ : ι → M<VAR>s t : Set M<VAR>x y z : M<VAR>v : ι → M<VAR>inst✝ : Unique ι<GOAL>LinearIndependent R v ↔ v default ≠ 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Nontrivial R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Module R M'<VAR>v✝ : ι → M<VAR>s t : Set M<VAR>x y z : M<VAR>v : ι → M<VAR>inst✝ : Unique ι<GOAL>(∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0) ↔ v default ≠ 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Nontrivial R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Module R M'<VAR>v✝ : ι → M<VAR>s t : Set M<VAR>x y z : M<VAR>v : ι → M<VAR>inst✝ : Unique ι<VAR>h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0<VAR>hv : v default = 0<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Nontrivial R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : Module R M'<VAR>v✝ : ι → M<VAR>s t : Set M<VAR>x y z : M<VAR>v : ι → M<VAR>inst✝ : Unique ι<VAR>h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0<VAR>hv : v default = 0<VAR>this : Finsupp.single default 1 = 0<GOAL>False
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>D₃ : Type u₆<VAR>inst✝⁸ : Category.{v₁, u₁} C₁<VAR>inst✝⁷ : Category.{v₂, u₂} C₂<VAR>inst✝⁶ : Category.{v₃, u₃} C₃<VAR>inst✝⁵ : Category.{v₄, u₄} D₁<VAR>inst✝⁴ : Category.{v₅, u₅} D₂<VAR>inst✝³ : Category.{v₆, u₆} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>G : D₁ ⥤ D₂<VAR>h : Φ.IsLocalizedEquivalence<VAR>inst✝ : CatCommSq Φ.functor L₁ L₂ G<GOAL>G.IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>D₃ : Type u₆<VAR>inst✝⁸ : Category.{v₁, u₁} C₁<VAR>inst✝⁷ : Category.{v₂, u₂} C₂<VAR>inst✝⁶ : Category.{v₃, u₃} C₃<VAR>inst✝⁵ : Category.{v₄, u₄} D₁<VAR>inst✝⁴ : Category.{v₅, u₅} D₂<VAR>inst✝³ : Category.{v₆, u₆} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>G : D₁ ⥤ D₂<VAR>h : Φ.IsLocalizedEquivalence<VAR>inst✝ : CatCommSq Φ.functor L₁ L₂ G<GOAL>(Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.54716, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasCokernel S.f<GOAL>S.Exact ↔ Mono (cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.54716, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasCokernel S.f<GOAL>Mono S.fromOpcycles ↔ Mono (cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.54716, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasCokernel S.f<GOAL>Arrow.mk (cokernel.desc S.f S.g ⋯) ≅ Arrow.mk S.fromOpcycles
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>x + t • y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y : E<VAR>s t✝ : Set E<VAR>hs : StarConvex 𝕜 x s<VAR>hy : x + y ∈ s<VAR>t : 𝕜<VAR>ht₀ : 0 ≤ t<VAR>ht₁ : t ≤ 1<VAR>h : x + t • y = (1 - t) • x + t • (x + y)<GOAL>(1 - t) • x + t • (x + y) ∈ s
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n✝ : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : DecidableEq n✝<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>n : ℕ<VAR>A : Matrix m m 𝔸<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>exp 𝕂 (n • A) = exp 𝕂 A ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq β<VAR>ht : s.Nonempty<VAR>i : β<GOAL>i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<GOAL>f = g
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<VAR>a : ↥(adjoin R s)<VAR>x : A<VAR>hx : x ∈ s<GOAL>(fun y => f y = g y) ⟨x, ⋯⟩
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<VAR>a : ↥(adjoin R s)<VAR>r : R<GOAL>(fun y => f y = g y) ((algebraMap R ↥(adjoin R s)) r)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<VAR>a x y : ↥(adjoin R s)<VAR>hx : (fun y => f y = g y) x<VAR>hy : (fun y => f y = g y) y<GOAL>(fun y => f y = g y) (x + y)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<VAR>a x y : ↥(adjoin R s)<VAR>hx : (fun y => f y = g y) x<VAR>hy : (fun y => f y = g y) y<GOAL>(fun y => f y = g y) (x * y)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : StarModule R B<VAR>inst✝⁵ : FunLike F A B<VAR>inst✝⁴ : AlgHomClass F R A B<VAR>inst✝³ : StarAlgHomClass F R A B<VAR>f✝ g✝ : F<VAR>s : Set A<VAR>inst✝² : FunLike F (↥(adjoin R s)) B<VAR>inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B<VAR>inst✝ : StarAlgHomClass F R (↥(adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x<VAR>a x : ↥(adjoin R s)<VAR>hx : (fun y => f y = g y) x<GOAL>(fun y => f y = g y) (star x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq (Option α)<VAR>s : Finset (Option α)<GOAL>map Embedding.some (eraseNone s) = s.erase none
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Ico a b ↔ x ∈ Ico (r • a) (r • b)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y, (a ≤ y ∧ y < b) ∧ r * y = x) ↔ r * a ≤ x ∧ x < r * b
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype p<VAR>inst✝² : AddCommMonoid R<VAR>o : Type u_8<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq o<VAR>d : o → R<GOAL>(diagonal d).trace = ∑ i : o, d i
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>v : M<GOAL>(LinearIndependent R fun n => (f ^ n) v) ↔ ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>v : M<GOAL>(∀ (l : ℕ →₀ R), (Finsupp.total ℕ M R fun n => (f ^ n) v) l = 0 → l = 0) ↔ ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>v : M<GOAL>(∀ (l : ℕ →₀ R), (l.sum fun i a => a • (f ^ i) v) = 0 → l = 0) ↔ ∀ (q : AddMonoidAlgebra R ℕ), ({ toFinsupp := q }.sum fun n b => b • (f ^ n) v) = 0 → q = 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x ≤ y<GOAL>f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>(periodicOrbit f x).length = minimalPeriod f x
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<GOAL>J(-a | b) = χ₄ ↑b * J(a | b)
<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>f : α → M<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>(1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h1 : s.Gammaℝ ≠ 0<GOAL>(1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<VAR>h1 : s.Gammaℝ ≠ 0<VAR>h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)<GOAL>(1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>u : ℙ K V<GOAL>u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>u : ℙ K V<GOAL>u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<GOAL>cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<VAR>hδ : δ ≤ 0<GOAL>cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<VAR>hδ : 0 ≤ δ<GOAL>cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<VAR>hδ : 0 ≤ δ<VAR>x : α<GOAL>x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<VAR>hδ : 0 ≤ δ<VAR>x : α<GOAL>infEdist x (thickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>ι : Type u_9<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>f' : M →ₗ[R] M<VAR>p : Submodule R M<VAR>n : ℕ<VAR>h : ∀ x ∈ p, f' x ∈ p<VAR>h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯<VAR>x : ↥p<GOAL>↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>ι : Type u_9<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : Semiring R₃<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>f' : M →ₗ[R] M<VAR>p : Submodule R M<VAR>n : ℕ<VAR>h : ∀ x ∈ p, f' x ∈ p<VAR>h' : optParam (∀ x ∈ p, (f' ^ n) x ∈ p) ⋯<VAR>x : ↥p<VAR>this : Semiconj Subtype.val ⇑(f'.restrict h) ⇑f'<GOAL>↑((f'.restrict h ^ n) x) = ↑(((f' ^ n).restrict h') x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.comp X = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>(p.sum fun e a => (monomial e) a) = p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X X' : SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>h : Z ⟶ Z'<GOAL>PInfty.f (n + 1) ≫ { a := g.app (op [n + 1]) ≫ f.a, b := fun i => g.app (op [n]) ≫ f.b i }.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X'.δ i.rev.succ ≫ { a := g.app (op [n + 1]) ≫ f.a, b := fun i => g.app (op [n]) ≫ f.b i }.b i.rev = g.app (op [n + 1]) ≫ (PInfty.f (n + 1) ≫ f.a + ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X X' : SimplicialObject C<VAR>n : ℕ<VAR>Z Z' : C<VAR>f : MorphComponents X n Z<VAR>g : X' ⟶ X<VAR>h : Z ⟶ Z'<GOAL>(P (n + 1)).f (n + 1) ≫ g.app (op [n + 1]) ≫ f.a + ∑ x : Fin (n + 1), (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op [n]) ≫ f.b x.rev = g.app (op [n + 1]) ≫ (P (n + 1)).f (n + 1) ≫ f.a + g.app (op [n + 1]) ≫ ∑ i : Fin (n + 1), (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<GOAL>S.RightHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯<VAR>hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' ⋯<GOAL>S.RightHomologyData