ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>h : ∀ (a : α) (f : β → ℝ≥0∞), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>(κ a) s = (η a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h : ∫⁻ (b : β), s.indicator (fun x => 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x => 1) b ∂η a<GOAL>(κ a) s = (η a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>h : (κ a) s = (η a) s<GOAL>(κ a) s = (η a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<GOAL>HasSum (fun n => (1 / 2) ^ n) 2
<VAR>n : ℕ<GOAL>(n + 0).descFactorial 0 = (n + 1).ascFactorial 0
<VAR>n k : ℕ<GOAL>(n + k.succ).descFactorial k.succ = (n + 1).ascFactorial k.succ
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<GOAL>Aᵀ.cramer b i = (A.updateRow i b).det
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 F<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z : E<GOAL>StrictConvex 𝕜 ((fun x => x + z) '' s)
<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>F : ι → X → α<VAR>S : Set X<GOAL>Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq M<VAR>x✝ : M →ₗ[A] M<GOAL>LinearMap.det x✝ = (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>κ : Type u_6<VAR>inst✝¹ : Fintype κ<VAR>inst✝ : DecidableEq M<VAR>x✝ : M →ₗ[A] M<GOAL>(if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝ = (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ Y₁ Z₁ : ModuleCat R<VAR>X₂ Y₂ Z₂ : ModuleCat R<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ Y₁ Z₁ : ModuleCat R<VAR>X₂ Y₂ Z₂ : ModuleCat R<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>(TensorProduct.mk R ↑X₁ ↑X₂).compr₂ (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) = (TensorProduct.mk R ↑X₁ ↑X₂).compr₂ (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>M✝ : ModuleCat R<VAR>M M' : ModuleCat R<VAR>g : M ⟶ M'<VAR>s : S<VAR>h : ↑(obj' f M)<VAR>t : S<GOAL>g ((s • h) t) = (s • g ∘ₗ h) t
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>M✝ : ModuleCat R<VAR>M M' : ModuleCat R<VAR>g : M ⟶ M'<VAR>s : S<VAR>h : ↑(obj' f M)<VAR>t : S<GOAL>g (h (t * s)) = (g ∘ₗ h) (t * s)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ (N₂ ⋙ Γ₂).map ((toKaroubi (SimplicialObject C)).obj X).decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app ((toKaroubi (SimplicialObject C)).obj X).X ≫ ((toKaroubi (SimplicialObject C)).obj X).decompId_p
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = (Γ₂N₂ToKaroubiIso.app X).inv ≫ Γ₂.map (N₂.map (𝟙 ((toKaroubi (SimplicialObject C)).obj X))) ≫ (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫ Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫ 𝟙 { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X, idem := ⋯ }
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = Γ₂N₂ToKaroubiIso.inv.app X ≫ 𝟙 (Γ₂.obj (N₂.obj ((toKaroubi (SimplicialObject C)).obj X))) ≫ (Γ₂N₂ToKaroubiIso.hom.app ((toKaroubi (SimplicialObject C)).obj X).X ≫ Γ₂N₁.natTrans.app ((toKaroubi (SimplicialObject C)).obj X).X) ≫ 𝟙 { X := ((toKaroubi (SimplicialObject C)).obj X).X, p := 𝟙 ((toKaroubi (SimplicialObject C)).obj X).X, idem := ⋯ }
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = Γ₂N₂ToKaroubiIso.inv.app X ≫ 𝟙 (Γ₂.obj (N₂.obj { X := X, p := 𝟙 X, idem := ⋯ })) ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>Γ₂N₁.natTrans.app X = Γ₂N₂ToKaroubiIso.inv.app X ≫ (Γ₂N₂ToKaroubiIso.hom.app X ≫ Γ₂N₁.natTrans.app X) ≫ 𝟙 { X := X, p := 𝟙 X, idem := ⋯ }
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>SS : WSeq (WSeq (WSeq α))<VAR>s1 s2 : WSeq α<VAR>h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)<GOAL>Computation.LiftRel (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)) s1.destruct s2.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>SS : WSeq (WSeq (WSeq α))<VAR>s1 s2 : WSeq α<VAR>h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)<GOAL>∀ {ca cb : Computation (Option (α × WSeq α))}, (fun c1 c2 => ∃ s S SS, c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct) ca cb → LiftRelAux (LiftRelO (fun x x_1 => x = x_1) fun s1 s2 => ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)) (fun c1 c2 => ∃ s S SS, c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct) ca.destruct cb.destruct
<VAR>x : ℝ<GOAL>evenKernel 0 x = cosKernel 0 x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p q : R[X]<VAR>x : A<GOAL>Algebra.adjoin R {X} = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<VAR>_hp : p ∈ ⊤<GOAL>p ∈ Algebra.adjoin R {X}
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<VAR>_hp : p ∈ ⊤<VAR>S : Subalgebra R R[X] := Algebra.adjoin R {X}<GOAL>p ∈ S
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<VAR>_hp : p ∈ ⊤<VAR>S : Subalgebra R R[X] := Algebra.adjoin R {X}<GOAL>(p.sum fun n a => (monomial n) a) ∈ S
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : CommSemiring A'<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R B<VAR>p✝ q : R[X]<VAR>x : A<VAR>p : R[X]<VAR>_hp : p ∈ ⊤<VAR>S : Subalgebra R R[X] := Algebra.adjoin R {X}<GOAL>(p.sum fun n a => a • X ^ n) ∈ S
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t✝ : Set α<VAR>a✝ b a : α<VAR>s t : Set α<GOAL>IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<GOAL>(X ^ n - C ↑u).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>u : Rˣ<VAR>a✝ : Nontrivial R<VAR>hn : IsUnit ↑0<GOAL>(X ^ 0 - C ↑u).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<VAR>hpos : n > 0<GOAL>(X ^ n - C ↑u).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<VAR>hpos : n > 0<GOAL>∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<VAR>hpos : n > 0<VAR>n' : R<VAR>hn' : n' * ↑n = 1<GOAL>∃ a b, a * (X ^ n - C ↑u) + b * derivative (X ^ n - C ↑u) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<VAR>hpos : n > 0<VAR>n' : R<VAR>hn' : n' * ↑n = 1<GOAL>-C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * derivative (X ^ n - C ↑u) = 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>u : Rˣ<VAR>hn : IsUnit ↑n<VAR>a✝ : Nontrivial R<VAR>hpos : n > 0<VAR>n' : R<VAR>hn' : n' * ↑n = 1<GOAL>-C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (C ↑n * X ^ (n - 1)) = 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<VAR>f : Fin (n + 1) → M → N<VAR>h : ∀ (x : Fin (n + 1)), f x 0 = 0<GOAL>(cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<VAR>f : Fin (n + 1) → M → N<VAR>h : ∀ (x : Fin (n + 1)), f x 0 = 0<GOAL>∑ i_1 : Fin (n + 1), f i_1 ((cons i σ) i_1) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>σ : Fin n →₀ M<VAR>i : M<VAR>f : Fin (n + 1) → M → N<VAR>h : ∀ (x : Fin (n + 1)), f x 0 = 0<GOAL>f 0 i + ∑ x : Fin n, f x.succ (σ x) = f 0 i + ∑ i : Fin n, Fin.tail f i (σ i)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<GOAL>f.degree = ⊥ ↔ f = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>h : f.degree = ⊥<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>h : f.support.sup WithBot.some = ⊥<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>h : f.support.sup WithBot.some = ⊥<VAR>n : ℤ<GOAL>f n = 0 n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>h : f.support.sup WithBot.some = ⊥<VAR>n : ℤ<VAR>f0 : ¬f n = 0 n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[T;T⁻¹]<VAR>n : ℤ<VAR>f0 : ¬f n = 0 n<VAR>h : ∀ (s : ℤ), ¬f s = 0 → False<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<GOAL>u ~[l] v ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<GOAL>(∃ φ, Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopologyEither E F<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E → 𝕜 → F := fun x t => f (x + t • v)<VAR>hg : Continuous (Function.uncurry g)<GOAL>StronglyMeasurable fun x => lineDeriv 𝕜 f x v
<VAR>R : Type u_1<VAR>inst✝¹³ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid M'<VAR>inst✝¹⁰ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module A M'<VAR>inst✝⁶ : IsLocalization S A<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M''<VAR>inst✝² : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>R' : Type u_6<VAR>inst✝¹ : CommSemiring R'<VAR>inst✝ : Algebra R R'<GOAL>IsLocalizedModule S (Algebra.ofId R R').toLinearMap ↔ IsLocalization S R'
<VAR>R : Type u_1<VAR>inst✝¹³ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid M'<VAR>inst✝¹⁰ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁹ : CommSemiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module A M'<VAR>inst✝⁶ : IsLocalization S A<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M''<VAR>inst✝² : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>R' : Type u_6<VAR>inst✝¹ : CommSemiring R'<VAR>inst✝ : Algebra R R'<GOAL>S = Algebra.algebraMapSubmonoid R S
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<VAR>P : Type u_1 := { E // Perfect E ∧ E.Nonempty }<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<VAR>P : Type u_1 := { E // Perfect E ∧ E.Nonempty }<VAR>C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α<VAR>h0 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C0 hC hnonempty hε) ∧ (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ EMetric.diam (C0 hC hnonempty hε) ≤ ε<VAR>h1 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C1 hC hnonempty hε) ∧ (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ EMetric.diam (C1 hC hnonempty hε) ≤ ε<VAR>hdisj : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<VAR>P : Type u_1 := { E // Perfect E ∧ E.Nonempty }<VAR>C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α<VAR>h0 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C0 hC hnonempty hε) ∧ (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ EMetric.diam (C0 hC hnonempty hε) ≤ ε<VAR>h1 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C1 hC hnonempty hε) ∧ (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ EMetric.diam (C1 hC hnonempty hε) ≤ ε<VAR>hdisj : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)<VAR>DP : List Bool → P := fun l => List.rec ⟨C, ⋯⟩ (fun a l ih => Bool.casesOn (motive := fun t => a = t → P) a (fun h => ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h => ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l<VAR>D : List Bool → Set α := fun l => ↑(DP l)<VAR>hanti : ClosureAntitone D<VAR>hdiam : VanishingDiam D<VAR>hdisj' : CantorScheme.Disjoint D<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<VAR>P : Type u_1 := { E // Perfect E ∧ E.Nonempty }<VAR>C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α<VAR>h0 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C0 hC hnonempty hε) ∧ (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ EMetric.diam (C0 hC hnonempty hε) ≤ ε<VAR>h1 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C1 hC hnonempty hε) ∧ (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ EMetric.diam (C1 hC hnonempty hε) ≤ ε<VAR>hdisj : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)<VAR>DP : List Bool → P := fun l => List.rec ⟨C, ⋯⟩ (fun a l ih => Bool.casesOn (motive := fun t => a = t → P) a (fun h => ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h => ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l<VAR>D : List Bool → Set α := fun l => ↑(DP l)<VAR>hanti : ClosureAntitone D<VAR>hdiam : VanishingDiam D<VAR>hdisj' : CantorScheme.Disjoint D<VAR>hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst<GOAL>∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ℝ≥0∞<VAR>hnonempty : C.Nonempty<VAR>inst✝ : CompleteSpace α<VAR>u : ℕ → ℝ≥0∞<VAR>upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>hu : Tendsto u atTop (nhds 0)<VAR>upos : ∀ (n : ℕ), 0 < u n<VAR>P : Type u_1 := { E // Perfect E ∧ E.Nonempty }<VAR>C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α<VAR>h0 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C0 hC hnonempty hε) ∧ (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ EMetric.diam (C0 hC hnonempty hε) ≤ ε<VAR>h1 : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Perfect (C1 hC hnonempty hε) ∧ (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ EMetric.diam (C1 hC hnonempty hε) ≤ ε<VAR>hdisj : ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε), Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)<VAR>DP : List Bool → P := fun l => List.rec ⟨C, ⋯⟩ (fun a l ih => Bool.casesOn (motive := fun t => a = t → P) a (fun h => ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h => ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l<VAR>D : List Bool → Set α := fun l => ↑(DP l)<VAR>hanti : ClosureAntitone D<VAR>hdiam : VanishingDiam D<VAR>hdisj' : CantorScheme.Disjoint D<VAR>hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst<VAR>x y : ℕ → Bool<VAR>hxy : (fun x => (inducedMap D).snd ⟨x, ⋯⟩) x = (fun x => (inducedMap D).snd ⟨x, ⋯⟩) y<GOAL>x = y
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<GOAL>Nonempty (IsColimit c'')
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.23191, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.23198, u_2} D<VAR>F : J ⥤ C<VAR>c c' : Cocone F<VAR>hc : IsUniversalColimit c<VAR>e : c ≅ c'<VAR>F' : J ⥤ C<VAR>c'' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c''.pt ⟶ c'.pt<VAR>h : α ≫ c'.ι = c''.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)<VAR>this : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι<GOAL>Nonempty (IsColimit c'')