ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X₁ : Type u₁<VAR>inst✝⁵ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝² : TopologicalSpace Y✝<VAR>inst✝¹ : TietzeExtension Y✝<VAR>Y : Type v<VAR>inst✝ : TopologicalSpace Y<VAR>f : C(X₁, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : X₁), f x ∈ t<VAR>ht : TietzeExtension ↑t<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ g.comp { toFun := e, continuous_toFun := ⋯ } = f
<VAR>X₁ : Type u₁<VAR>inst✝⁵ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝² : TopologicalSpace Y✝<VAR>inst✝¹ : TietzeExtension Y✝<VAR>Y : Type v<VAR>inst✝ : TopologicalSpace Y<VAR>f : C(X₁, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : X₁), f x ∈ t<VAR>ht : TietzeExtension ↑t<VAR>g : C(X, ↑t)<VAR>hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ g.comp { toFun := e, continuous_toFun := ⋯ } = f
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a✝ b a : α<VAR>s t : Multiset α<GOAL>a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
<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>p q : X → Prop<VAR>hp : IsOpen {x | p x}<VAR>hq : IsClosed {x | q x}<GOAL>IsClosed {x | p x → q x}
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)<GOAL>abscissaOfAbsConv f ≤ ↑x + 1
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)<VAR>H : ↑x + 1 < abscissaOfAbsConv f<GOAL>False
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>h : f =O[atTop] fun n => ↑n ^ (x + 1 - 1)<VAR>H : ↑x + 1 < abscissaOfAbsConv f<VAR>y : ℝ<VAR>hy₁ : ↑x + 1 < ↑y<VAR>hy₂ : ↑y < abscissaOfAbsConv f<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>R : β → β → Prop<VAR>l : List α<VAR>f : α → List β<GOAL>Pairwise R (l.bind f) ↔ (∀ (a : α), a ∈ l → Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ (x : β), x ∈ f a₁ → ∀ (y : β), y ∈ f a₂ → R x y) l
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>j : Fin B'.dim<GOAL>IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>j : Fin B'.dim<GOAL>IsIntegral R ((B.basis.repr ((fun i => B'.gen ^ ↑i) j)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i✝ : Fin B.dim<VAR>j : Fin B'.dim<VAR>i : Fin B.dim<GOAL>IsIntegral R ((B.basis.repr B'.gen) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i✝ : Fin B.dim<VAR>j : Fin B'.dim<VAR>i : Fin B.dim<GOAL>IsIntegral R (∑ k ∈ Finset.range (P.natDegree + 1), (B.basis.repr (P.coeff k • B.gen ^ k)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i✝ : Fin B.dim<VAR>j : Fin B'.dim<VAR>i : Fin B.dim<VAR>n : ℕ<VAR>x✝ : n ∈ Finset.range (P.natDegree + 1)<GOAL>IsIntegral R ((B.basis.repr (P.coeff n • B.gen ^ n)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra K S<VAR>R : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsScalarTower R K S<VAR>A : Type u_4<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : IsScalarTower R S A<VAR>B✝ : PowerBasis S A<VAR>hB✝ : IsIntegral R B✝.gen<VAR>B B' : PowerBasis K S<VAR>P : R[X]<VAR>h : (aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i✝ : Fin B.dim<VAR>j : Fin B'.dim<VAR>i : Fin B.dim<VAR>n : ℕ<VAR>x✝ : n ∈ Finset.range (P.natDegree + 1)<GOAL>IsIntegral R ((P.coeff n • B.basis.repr (B.gen ^ n)) i)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<GOAL>P.RespectsIso
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<GOAL>∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>f g : Arrow C<VAR>e : f ≅ g<GOAL>P f.hom → P g.hom
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝¹ v✝¹ w x y u v : V<VAR>n : ℕ<VAR>p : G.Walk u v<VAR>hnp : ¬p.Nil<VAR>u✝ v✝ w✝ : V<VAR>x✝¹ : G.Adj u✝ v✝<VAR>x✝ : G.Walk v✝ w✝<GOAL>((cons x✝¹ x✝).tail ⋯).getVert n = (cons x✝¹ x✝).getVert (n + 1)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>biproduct.ι (fun j => f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ▷ X
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>inst✝ : CompactSpace ↑s<GOAL>↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = closure ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>inst✝ : CompactSpace ↑s<GOAL>↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>inst✝ : CompactSpace ↑s<GOAL>closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) = Set.univ
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>inst✝ : CompactSpace ↑s<GOAL>closure ↑(polynomialFunctions s).starClosure = Set.univ
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasColimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>j : J<GOAL>colimit.ι F j ≫ (isoOfEquivalence e w).hom = F.map (e.unit.app j) ≫ w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>hs : Finite ↑s<VAR>ht : Finite ↑t<GOAL>(s ∪ t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonAssocRing α<VAR>a b : α<GOAL>a * (b - 1) = a * b - a
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivAtFilter g₁ g₁' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hy : y = h x<VAR>hL : Tendsto h L L'<GOAL>HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.114300<VAR>inst✝ : MulAction R X<VAR>p r : R<VAR>s : ↥S<GOAL>p /ₒ s * (r /ₒ 1) = p * r /ₒ s
<VAR>C : Type ?u.28028<VAR>inst✝⁵ : Category.{?u.28032, ?u.28028} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>φ.τ₂ ≫ S₂.g = 0
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<GOAL>QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>hf₁ : S₁.f = 0<VAR>hg₁ : S₁.g = 0<VAR>hf₂ : S₂.f = 0<VAR>H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁) (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι S₂.iCycles ⋯) S₂.cyclesIsKernel) := { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }<GOAL>QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>ha : IsFundamental a<VAR>hb : IsFundamental b<GOAL>a = b
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>ha : IsFundamental a<VAR>hb : IsFundamental b<VAR>hx : a.x = b.x<GOAL>a = b
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>ha : IsFundamental a<VAR>hb : IsFundamental b<VAR>hx : a.x = b.x<GOAL>a.y = b.y
<VAR>d : ℤ<VAR>a b : Solution₁ d<VAR>ha : IsFundamental a<VAR>hb : IsFundamental b<VAR>hx : a.x = b.x<VAR>this : d * a.y ^ 2 = d * b.y ^ 2<GOAL>a.y = b.y
<VAR>x✝ y x : ℝ<GOAL>√x⁻¹ = (√x)⁻¹
<VAR>n✝ n : ℕ<GOAL>↑n ≡ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]
<VAR>n✝ n : ℕ<VAR>t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]<GOAL>↑n ≡ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>b : β<VAR>hf : Multipliable (update f b 1)<VAR>n : β<GOAL>f n = (if n = b then f n else 1) * update f b 1 n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>b : β<VAR>hf : Multipliable (update f b 1)<GOAL>(∏' (x : β), if x = b then f x else 1) = if b = b then f b else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : ContinuousMul α<VAR>inst✝ : DecidableEq β<VAR>f : β → α<VAR>b : β<VAR>hf : Multipliable (update f b 1)<GOAL>(if b = b then f b else 1) * ∏' (x : β), update f b 1 x = f b * ∏' (x : β), if x = b then 1 else f x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ κ a ⟂ₘ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a<GOAL>(η.withDensity (κ.rnDeriv η)) a = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a<GOAL>(η.withDensity (κ.rnDeriv η)) a ⟂ₘ (η.withDensity (κ.rnDeriv η)) a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>‖c • f‖ = ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>f : ↥(lp E p)<GOAL>‖0 • f‖ = ‖0‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<VAR>hc : c ≠ 0<GOAL>‖c • f‖ = ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<VAR>hc : c ≠ 0<GOAL>‖c‖ * ‖f‖ ≤ ‖c • f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝³ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : (i : α) → Module 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<VAR>hc : c ≠ 0<VAR>this : ‖c‖ * ‖c⁻¹ • c • f‖ ≤ ‖c‖ * (‖c⁻¹‖ * ‖c • f‖)<GOAL>‖c‖ * ‖f‖ ≤ ‖c • f‖
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>infSum 𝒜 = 1
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>h𝒜₁ : 𝒜.Nonempty<VAR>h𝒜₀ : ∅ ∉ 𝒜<GOAL>univ ∉ 𝒜ᶜˢ
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a < b⁻¹ ↔ b < a⁻¹
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>∃ u, ContDiff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ Icc 0 1) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>A : IsOpen (ball 0 1)<GOAL>∃ u, ContDiff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ Icc 0 1) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>A : IsOpen (ball 0 1)<VAR>f : E → ℝ<VAR>f_support : support f = ball 0 1<VAR>f_smooth : ContDiff ℝ ⊤ f<VAR>f_range : range f ⊆ Icc 0 1<GOAL>∃ u, ContDiff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ Icc 0 1) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>A : IsOpen (ball 0 1)<VAR>f : E → ℝ<VAR>f_support : support f = ball 0 1<VAR>f_smooth : ContDiff ℝ ⊤ f<VAR>f_range : range f ⊆ Icc 0 1<VAR>B : ∀ (x : E), f x ∈ Icc 0 1<GOAL>∃ u, ContDiff ℝ ⊤ u ∧ (∀ (x : E), u x ∈ Icc 0 1) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
<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>inst✝ : Infinite R<VAR>p q : R[X]<VAR>ext : ∀ (r : R), eval r p = eval r q<GOAL>p = q
<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>inst✝ : Infinite R<VAR>p q : R[X]<VAR>ext : ∀ (r : R), eval r p = eval r q<GOAL>p - q = 0
<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>inst✝ : Infinite R<VAR>p q : R[X]<VAR>ext : ∀ (r : R), eval r p = eval r q<GOAL>∀ (x : R), eval x (p - q) = 0
<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>inst✝ : Infinite R<VAR>p q : R[X]<VAR>ext : ∀ (r : R), eval r p = eval r q<VAR>x : R<GOAL>eval x (p - q) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<GOAL>ContMDiffOn 𝓘(𝕜, E) I n (↑(e.extend I).symm) (↑I '' e.target)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<GOAL>↑I '' e.target ⊆ ↑(I.restr e.target).symm ⁻¹' e.target
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : ChartedSpace H M<VAR>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<GOAL>e.target ⊆ e.target
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<GOAL>f.HasEigenvalue μ
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<GOAL>f.HasEigenvalue μ
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<VAR>u : (V →ₗ[K] V)ˣ<VAR>hu : ↑u = f - (algebraMap K (End K V)) μ<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<VAR>u : (V →ₗ[K] V)ˣ<VAR>hu : ↑u = f - (algebraMap K (End K V)) μ<VAR>p_ne_0 : p ≠ 0<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>μ : K<VAR>h : (minpoly K f).IsRoot μ<VAR>p : K[X]<VAR>hp : minpoly K f = (X - C μ) * p<VAR>con : LinearMap.ker (f - (algebraMap K (End K V)) μ) = ⊥<VAR>u : (V →ₗ[K] V)ˣ<VAR>hu : ↑u = f - (algebraMap K (End K V)) μ<VAR>p_ne_0 : p ≠ 0<VAR>this : (aeval f) p = 0<GOAL>False