ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b : ValueGroup A K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<VAR>xb yb : A<VAR>hyb : yb ∈ nonZeroDivisors A<VAR>this : (algebraMap A K) ya ≠ 0<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ∨ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b : ValueGroup A K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<VAR>xb yb : A<VAR>hyb : yb ∈ nonZeroDivisors A<VAR>this✝ : (algebraMap A K) ya ≠ 0<VAR>this : (algebraMap A K) yb ≠ 0<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ∨ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b : ValueGroup A K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<VAR>xb yb : A<VAR>hyb : yb ∈ nonZeroDivisors A<VAR>this✝ : (algebraMap A K) ya ≠ 0<VAR>this : (algebraMap A K) yb ≠ 0<VAR>c : A<VAR>h : xa * yb * c = xb * ya<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ∨ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)
<VAR>A : Type u<VAR>inst✝⁵ : CommRing A<VAR>K : Type v<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : ValuationRing A<VAR>inst✝ : IsFractionRing A K<VAR>a b : ValueGroup A K<VAR>xa ya : A<VAR>hya : ya ∈ nonZeroDivisors A<VAR>xb yb : A<VAR>hyb : yb ∈ nonZeroDivisors A<VAR>this✝ : (algebraMap A K) ya ≠ 0<VAR>this : (algebraMap A K) yb ≠ 0<VAR>c : A<VAR>h : xb * ya * c = xa * yb<GOAL>Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya) ≤ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ∨ Quot.mk Setoid.r ((algebraMap A K) xb / (algebraMap A K) yb) ≤ Quot.mk Setoid.r ((algebraMap A K) xa / (algebraMap A K) ya)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : TopologicalRing R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => (A x).det
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : TopologicalRing R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<GOAL>Continuous fun x => ∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, A x (σ i) i
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l✝ : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l✝ → Type u_9<VAR>n' : l✝ → Type u_10<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace R<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing R<VAR>inst✝ : TopologicalRing R<VAR>A : X → Matrix n n R<VAR>hA : Continuous A<VAR>l : Equiv.Perm n<VAR>x✝ : l ∈ Finset.univ<GOAL>Continuous fun x => ∏ i : n, A x (l i) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>s : Finset ℕ<VAR>a : ℕ<VAR>ha : a < n<GOAL>⟨a, ha⟩ ∈ Finset.fin n s ↔ ↑⟨a, ha⟩ ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' closure s \ f ⁻¹' s ⊆ closure (f ⁻¹' s) \ f ⁻¹' s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f : X → Y<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
<VAR>a b : ℤ<VAR>h : a ≤ b + 1<GOAL>↑(Icc a b).card = b + 1 - a
<VAR>X✝ Y✝ : LocallyRingedSpace<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>X Y : RingedSpace<VAR>f g : X ⟶ Y<VAR>H : f = g<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : IsLocalRingHom (PresheafedSpace.Hom.stalkMap f x)<GOAL>IsLocalRingHom (PresheafedSpace.Hom.stalkMap g x)
<VAR>X✝ Y✝ : LocallyRingedSpace<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>X Y : RingedSpace<VAR>f g : X ⟶ Y<VAR>H : f = g<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : IsLocalRingHom (PresheafedSpace.Hom.stalkMap f x)<GOAL>IsLocalRingHom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>h : x ∉ periodicPts f<GOAL>¬0 < minimalPeriod f x
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>f : F<VAR>x : A<GOAL>map f (adjoin R {x}) = adjoin R {f x}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F G F'✝ G' : C ⥤ D<VAR>α : F ⟶ G<VAR>β : F'✝ ⟶ G'<VAR>F' : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(tensorObj F F').map f ≫ (fun X => α.app X ▷ F'.obj X) Y = (fun X => α.app X ▷ F'.obj X) X ≫ (tensorObj G F').map f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F G F'✝ G' : C ⥤ D<VAR>α : F ⟶ G<VAR>β : F'✝ ⟶ G'<VAR>F' : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(tensorObj F F').map f ≫ (α.app Y ⊗ 𝟙 (F'.obj Y)) = (α.app X ⊗ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u<VAR>inst✝⁶ : NormedAddCommGroup E✝<VAR>inst✝⁵ : NormedSpace 𝕜 E✝<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝² : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝ : Fintype ι<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>n : ℕ∞<VAR>x : (i : ι) → E i<GOAL>x ∈ EMetric.ball 0 ⊤
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>val✝ : List α<VAR>property✝ : val✝.length = n<GOAL>(x ::ᵥ ⟨val✝, property✝⟩).reverse = (reverse ⟨val✝, property✝⟩).snoc x
<VAR>α : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>val✝ : List α<VAR>property✝ : val✝.length = n<GOAL>⟨val✝.reverse ++ [x], ⋯⟩ = append ⟨val✝.reverse, ⋯⟩ ⟨[x], ⋯⟩
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : S.HasLeftHomology<VAR>inst✝ : F.PreservesLeftHomologyOf S<GOAL>cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) = cyclesMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫ F.map (cyclesMap' (𝟙 S) hl S.leftHomologyData)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<GOAL>adjoin R (⋃ f ∈ S, of' R M '' ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<GOAL>⊤ ≤ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<GOAL>S ⊆ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<VAR>f : R[M]<VAR>hf : f ∈ S<GOAL>f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>S : Set R[M]<VAR>hS : adjoin R S = ⊤<VAR>f : R[M]<VAR>hf : f ∈ S<VAR>hincl : of' R M '' ↑f.support ⊆ ⋃ g ∈ S, of' R M '' ↑g.support<GOAL>f ∈ ↑(adjoin R (⋃ f ∈ S, of' R M '' ↑f.support))
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<GOAL>QuasiIso φ.τ₃
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<GOAL>∀ (i : ι), QuasiIsoAt φ.τ₃ i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>QuasiIsoAt φ.τ₃ i
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>IsIso (homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>Epi (homologyMap φ.τ₁ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>IsIso (homologyMap φ.τ₂ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>h₁ : QuasiIso φ.τ₁<VAR>h₂ : QuasiIso φ.τ₂<VAR>i : ι<GOAL>∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝³ : CommRing O<VAR>inst✝² : Algebra O R<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>x : O<VAR>hx : IsUnit x<VAR>H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1<VAR>u : Oˣ<VAR>hu : ↑u = x<GOAL>1 ≤ v ((algebraMap O R) x)
<VAR>R : Type u<VAR>Γ₀ : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>O : Type w<VAR>inst✝³ : CommRing O<VAR>inst✝² : Algebra O R<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O R<VAR>x : O<VAR>hx : IsUnit x<VAR>H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1<VAR>u : Oˣ<VAR>hu : ↑u = x<GOAL>v ((algebraMap O R) x) * v ((algebraMap O R) ↑u⁻¹) ≤ v ((algebraMap O R) x) * 1
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a✝ b✝ c a b : G<GOAL>a⁻¹ * (a * b) = b
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) ↑(φ * ψ) = (MvPowerSeries.coeff R n) (↑φ * ↑ψ)
<VAR>x : ℝ≥0∞<VAR>n : ℤ<GOAL>x ^ ↑n = x ^ n
<VAR>R : Type u<VAR>inst✝ : CommRing R<GOAL>range toPrimeSpectrum = {x | IsClosed {x}}
<VAR>R : Type u<VAR>inst✝ : CommRing R<GOAL>range toPrimeSpectrum = {x | x.asIdeal.IsMaximal}
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : Ideal R<VAR>isPrime✝ : x.IsPrime<GOAL>{ asIdeal := x, isPrime := isPrime✝ } ∈ range toPrimeSpectrum ↔ { asIdeal := x, isPrime := isPrime✝ } ∈ {x | x.asIdeal.IsMaximal}
<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>W X Y Z : C<VAR>f g : W ⟶ X<VAR>h : Y ⟶ Z<GOAL>(f + g) ⊗ h = f ⊗ h + g ⊗ h
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCancelCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n a b : μ<VAR>hab : (a, b) ∈ ↑(antidiagonal n)<VAR>c d : μ<VAR>hcd : (c, d) ∈ ↑(antidiagonal n)<GOAL>(a, b) ≠ (c, d) → (Disjoint on fun p => map (addRightEmbedding fun j => if j = i then p.1 else 0) (s.piAntidiag p.2)) (a, b) (c, d)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCancelCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>n a b : μ<VAR>hab : (a, b) ∈ ↑(antidiagonal n)<VAR>c d : μ<VAR>hcd : (c, d) ∈ ↑(antidiagonal n)<GOAL>¬b = d → ∀ ⦃a_2 : ι → μ⦄ (x : ι → μ), s.sum x = b → (∀ (i : ι), ¬x i = 0 → i ∈ s) → (x + fun j => if j = i then a else 0) = a_2 → ∀ (x : ι → μ), s.sum x = d → (∀ (i : ι), ¬x i = 0 → i ∈ s) → ¬(x + fun j => if j = i then c else 0) = a_2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>s : Set β<VAR>hs : s ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sSup s ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>t : Set α<VAR>ht : t ⊆ ↑L<VAR>hs : ⇑f '' t ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sSup (⇑f '' t) ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>t : Set α<VAR>ht : t ⊆ ↑L<VAR>hs : ⇑f '' t ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>f (sSup t) ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>s : Set β<VAR>hs : s ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sInf s ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>t : Set α<VAR>ht : t ⊆ ↑L<VAR>hs : ⇑f '' t ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>sInf (⇑f '' t) ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L✝ L : CompleteSublattice α<VAR>t : Set α<VAR>ht : t ⊆ ↑L<VAR>hs : ⇑f '' t ⊆ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier<GOAL>f (sInf t) ∈ { carrier := ⇑f '' ↑L, supClosed' := ⋯, infClosed' := ⋯ }.carrier
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<VAR>h : a / b = 0<GOAL>a < b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<VAR>h : a / b = 0<GOAL>a % b < b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<VAR>h : a < b<GOAL>a / b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>f₂ : N ≃ P<VAR>hf₂ : f₂ 0 = 0<VAR>hf₂' : f₂.symm 0 = 0<GOAL>(f.trans f₂) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>f₂ : N ≃ P<VAR>hf₂ : f₂ 0 = 0<VAR>hf₂' : f₂.symm 0 = 0<GOAL>(f.trans f₂).symm 0 = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} o.card < c<GOAL>lift.{v, u} o.card < c.ord.cof
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>μ (iUnionNotConvergentSeq hε hf hg hsm hs hfg) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∑' (a : ℕ), ENNReal.ofReal (ε / 2 * 2⁻¹ ^ a) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (2⁻¹ ^ a) ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝³ : MetricSpace β<VAR>μ : Measure α<VAR>n : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Countable ι<VAR>hε : 0 < ε<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Summable (HPow.hPow 2⁻¹)