ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : 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 M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h₁ : I ≤ J<VAR>h₂ : N ≤ N'<VAR>m : M<VAR>h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1<GOAL>m ∈ ⁅J, N'⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M₂ : 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 M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N₂ : LieSubmodule R L M₂<VAR>h₁ : I ≤ J<VAR>h₂ : N ≤ N'<VAR>m : M<VAR>h : ∀ (N_1 : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N_1 → m ∈ N_1<GOAL>∀ (N : LieSubmodule R L M), {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑N → m ∈ 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>inst✝⁶ : Algebra E K✝<VAR>inst✝⁵ : IsScalarTower F E K✝<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>Module.rank F E * sepDegree E K = sepDegree F K
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Finite m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n R<GOAL>Function.Surjective A.mulVec ↔ ∃ B, A * B = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Finite m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n R<VAR>val✝ : Fintype m<GOAL>Function.Surjective A.mulVec ↔ ∃ B, A * B = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Finite m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n R<VAR>val✝ : Fintype m<VAR>h : Function.Surjective A.mulVec<VAR>cols : m → n → R<VAR>hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1<GOAL>∃ B, A * B = 1
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Finite m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n R<VAR>val✝ : Fintype m<VAR>h : Function.Surjective A.mulVec<VAR>cols : m → n → R<VAR>hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1<VAR>i j : m<GOAL>(A * (of cols)ᵀ) i j = 1 i j
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Finite m<VAR>inst✝ : Fintype n<VAR>A : Matrix m n R<VAR>val✝ : Fintype m<VAR>h : Function.Surjective A.mulVec<VAR>cols : m → n → R<VAR>hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1<VAR>i j : m<GOAL>(A * (of cols)ᵀ) i j = (A *ᵥ cols j) i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>u v : UniformSpace β<VAR>F : Filter β<GOAL>F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>i j : A<VAR>h : i + j = 0<GOAL>j + i = 0
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>i j : A<VAR>h : i + j = 0<VAR>X : C<GOAL>(shiftFunctor C i).map ((shiftFunctorCompIsoId C i j h).symm.hom.app X) ≫ (shiftFunctorCompIsoId C j i ⋯).hom.app ((shiftFunctor C i).obj X) = 𝟙 ((shiftFunctor C i).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>i j : A<VAR>h : i + j = 0<VAR>X : C<VAR>e_1✝ : ((shiftFunctor C i).obj ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) = ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj X))<VAR>e_3✝ : (shiftFunctor C i).obj ((𝟭 C).obj X) = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj ((𝟭 C).obj X)<VAR>e_4✝¹ : (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse).obj X)<VAR>e_7✝ : (shiftFunctor C i ⋙ shiftFunctor C j).obj X = ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse).obj X<VAR>e_6✝ : shiftFunctor C i ⋙ shiftFunctor C j = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse<VAR>e_4✝ : shiftFunctor C i ⋙ shiftFunctor C j = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse<GOAL>(shiftFunctorCompIsoId C i j h).symm = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).unitIso
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>i j : A<VAR>h : i + j = 0<VAR>X : C<VAR>e_1✝ : ((shiftFunctor C i).obj ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((shiftFunctor C i).obj X)) = ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj ((𝟭 C).obj X) ⟶ (𝟭 C).obj ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj X))<VAR>e_4✝ : (shiftFunctor C i).obj ((shiftFunctor C i ⋙ shiftFunctor C j).obj X) = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj (((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse).obj X)<VAR>e_5✝¹ : (𝟭 C).obj ((shiftFunctor C i).obj X) = (𝟭 C).obj ((equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor.obj X)<VAR>e_5✝ : shiftFunctor C j ⋙ shiftFunctor C i = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor<VAR>e_3✝ : shiftFunctor C j ⋙ shiftFunctor C i = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).inverse ⋙ (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).functor<GOAL>shiftFunctorCompIsoId C j i ⋯ = (equivOfTensorIsoUnit (shiftMonoidalFunctor C A) { as := i } { as := j } (Discrete.eqToIso h) (Discrete.eqToIso ⋯) ⋯).counitIso
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : HasContDiffBump E<VAR>inst✝⁴ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : μ.IsOpenPosMeasure<GOAL>(μ (closedBall c f.rIn)).toReal ≤ ∫ (x : E), ↑f x ∂μ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : Monoid α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid β<VAR>s t : Finset α<GOAL>ThreeGPFree ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<GOAL>⋂ i, ⋂ j, s i j = ∅ ↔ ∀ (a : α), ∃ i j, a ∉ s i j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : Summable fun n => ‖p n‖ * ↑r ^ n<GOAL>Summable fun n => ‖p n‖₊ * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h : Summable fun n => ↑‖p n‖₊ * ↑r ^ n<GOAL>Summable fun n => ‖p n‖₊ * r ^ n
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>a b : n<VAR>hb : b ≠ j<VAR>c : R<VAR>M : Matrix n n R<GOAL>(M * transvection i j c) a b = M a b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G H : C ⥤ Type w<VAR>X Y Z : C<VAR>σ : F ⟶ G<VAR>τ : G ⟶ H<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a : F.obj X<GOAL>F.map (f ≫ g) a = F.map g (F.map f a)
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : MulPosReflectLT α<VAR>a0 : 0 < a<GOAL>a < b * a ↔ 1 * a < b * a
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<GOAL>M ^ n = span R (↑M ^ n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>G : Cᵒᵖ ⥤ Grp<VAR>X : C<VAR>I : Type w'<VAR>U : I → C<VAR>γ : OneCocycle G U<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>γ.ev i j a b = (γ.ev j i b a)⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List M<VAR>m : M<VAR>h : ∀ x ∈ l, x = m<GOAL>l.prod = m ^ l.length
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<GOAL>cfcₙHom ha = cfcₙHom_of_cfcHom R ha
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>cfcₙHom ha = cfcₙHom_of_cfcHom R ha
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>Continuous ⇑(cfcₙHom ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>Continuous ⇑(cfcₙHom_of_cfcHom R ha)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Field R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : CompleteSpace R<VAR>inst✝⁷ : TopologicalRing R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>h_cpct : ∀ (a : A), CompactSpace ↑(spectrum R a)<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>a : A<VAR>ha : p a<VAR>h_cpct' : CompactSpace ↑(σₙ R a)<GOAL>(cfcₙHom ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ?refine_1 } = (cfcₙHom_of_cfcHom R ha) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ?refine_1 }
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>inst✝¹ : Fintype V<VAR>G' : G.Subgraph<VAR>inst✝ : Fintype ↑G'.verts<VAR>h : G'.IsSpanning<GOAL>G'.verts.toFinset.card = Fintype.card V
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>inst✝¹ : Fintype V<VAR>G' : G.Subgraph<VAR>inst✝ : Fintype ↑G'.verts<VAR>h : G'.IsSpanning<GOAL>Finset.univ.card = Fintype.card V
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a x : R<GOAL>x ∈ nthRoots n a ↔ x ^ n = a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>cyclotomic p R = ∑ i ∈ range p, X ^ i
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>cyclotomic p ℤ = ∑ i ∈ range p, X ^ i
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ v : E<GOAL>HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ v : E<VAR>h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0<GOAL>HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ v : E<VAR>h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0<VAR>h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0<GOAL>HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ v : E<VAR>h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0<VAR>h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0<VAR>h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0<GOAL>HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v✝ v : E<VAR>h₀ : HasFDerivAt (fun w => ‖w‖ ^ 2) 0 0<VAR>h₁ : HasFDerivAt (fun w => (‖w‖ ^ 2 + 4)⁻¹) 0 0<VAR>h₂ : HasFDerivAt (fun w => 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0<GOAL>ContinuousLinearMap.id ℝ E = (‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G.obj Y'<VAR>h : X' ⟶ G.obj Y<VAR>k : Y ⟶ Y'<VAR>w : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k<GOAL>f ≫ g = h ≫ G.map k
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>h : Reflexive r<VAR>a b : α<VAR>hab : r a b<GOAL>DirectedOn r {b, a}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s : α → α → Prop<VAR>h : Reflexive r<VAR>a b : α<VAR>hab : r a b<GOAL>DirectedOn r {a, b}
<VAR>x : ℝ<GOAL>x + 1 ≤ rexp x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>x + 1 ≤ rexp x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>f g : Filter α<VAR>s : Set α → Set β<VAR>hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂<GOAL>(f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>f g : Filter α<VAR>s : Set α → Set β<VAR>hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂<GOAL>⨅ i, (bif i then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>f g : Filter α<VAR>s : Set α → Set β<VAR>hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂<GOAL>∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι'✝ : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t✝ : ι✝ → α<VAR>ht✝ : Independent t✝<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : Independent t<VAR>hf : Injective f<VAR>i : ι'<GOAL>⨆ j, ⨆ (_ : j ≠ i), (t ∘ f) j ≤ ⨆ j, ⨆ (_ : j ≠ f i), t j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι'✝ : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t✝ : ι✝ → α<VAR>ht✝ : Independent t✝<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : Independent t<VAR>hf : Injective f<VAR>i✝ i : ι'<GOAL>⨆ (_ : i ≠ i✝), (t ∘ f) i ≤ ⨆ (_ : f i ≠ f i✝), t (f i)
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget LightProfinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>a z = b z
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget LightProfinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>↑(a z) = ↑(b z)
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget LightProfinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).1 = (↑(b z)).1
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>Z : LightProfinite<VAR>a b : Z ⟶ pullback f g<VAR>z : (forget LightProfinite).obj Z<VAR>hfst : (a ≫ fst f g) z = (b ≫ fst f g) z<VAR>hsnd : (a ≫ snd f g) z = (b ≫ snd f g) z<GOAL>(↑(a z)).2 = (↑(b z)).2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>p : V × V<VAR>h : G.Adj p.1 p.2<GOAL>∀ {p_1 : V × V}, { toProd := p, adj := h }.edge = Sym2.mk p_1 ↔ { toProd := p, adj := h }.toProd = p_1 ∨ { toProd := p, adj := h }.toProd = p_1.swap
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<GOAL>s⁻¹ = ∅ ↔ s = ∅
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X : C<GOAL>Triangle.mk 0 (𝟙 X) 0 ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X : C<GOAL>Triangle.mk 0 (𝟙 X) 0 ≅ (contractibleTriangle X).invRotate
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.250887, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>n' m' : ℤ<VAR>α' : Cochain F L m'<VAR>β' : Cochain G L n'<VAR>h : n + 1 = m<VAR>h' : m' + 1 = n'<VAR>p : ℤ<VAR>hp : n + n' = p<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + n = p₂<VAR>h₂₃ : p₂ + n' = p₃<VAR>q : ℤ<VAR>hq : p₁ + m = q<GOAL>(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ = α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.250887, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>n' m' : ℤ<VAR>α' : Cochain F L m'<VAR>β' : Cochain G L n'<VAR>h : n + 1 = m<VAR>h' : m' + 1 = n'<VAR>p : ℤ<VAR>hp : n + n' = p<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + n = p₂<VAR>h₂₃ : p₂ + n' = p₃<VAR>q : ℤ<VAR>hq : p₁ + m = q<VAR>eq : ((liftCochain φ α β h).comp (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ = (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯<GOAL>(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ = α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x₀ : E<VAR>n : ℕ<VAR>h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : 1 < n<GOAL>HasFDerivAt f 0 x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x₀ : E<VAR>n : ℕ<VAR>h : f =O[𝓝[univ] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : 1 < n<GOAL>HasFDerivAt f 0 x₀