ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g ≫ h = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc (f ≫ h) (g ≫ h)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝⁹ : CommRing Rₛ<VAR>inst✝⁸ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup Mₛ<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ inst✝³ : Module R Mₛ<VAR>inst✝² : Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>i : ι<GOAL>(ofIsLocalizedModule Rₛ S f b) i = f (b i)
<VAR>a b c d m n : ℤ<VAR>hmn : m ∣ n<VAR>hnm : n.natAbs < m.natAbs<GOAL>n = 0
<VAR>a b c d m n : ℤ<VAR>hmn : m.natAbs ∣ n.natAbs<VAR>hnm : n.natAbs < m.natAbs<GOAL>n = 0
<VAR>a b c d m n : ℤ<VAR>hmn : m.natAbs ∣ n.natAbs<VAR>hnm : n.natAbs < m.natAbs<GOAL>n.natAbs = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>inst✝ : MulOneClass N<VAR>f : M →* N<VAR>hf : ∀ (x y : M), Commute (f x) (f y)<VAR>x y : M<GOAL>{ toFun := op ∘ ⇑f, map_one' := ⋯ }.toFun (x * y) = { toFun := op ∘ ⇑f, map_one' := ⋯ }.toFun x * { toFun := op ∘ ⇑f, map_one' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I X : Set β<GOAL>(M.mapEmbedding f).Basis I X ↔ M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I X : Set β<GOAL>(∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I X : Set β<VAR>x✝ : M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f<VAR>hb : M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' X)<VAR>hIX : I ⊆ X<VAR>hX : X ⊆ range ⇑f<GOAL>∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>I : Set β<VAR>X : Set α<VAR>x✝ : M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X)) ∧ I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f<VAR>hb : M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X))<VAR>hIX : I ⊆ ⇑f '' X<VAR>hX : ⇑f '' X ⊆ range ⇑f<GOAL>∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ↪ β<VAR>X : Set α<VAR>hX : ⇑f '' X ⊆ range ⇑f<VAR>I : Set α<VAR>x✝ : M.Basis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f<VAR>hb : M.Basis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X))<VAR>hIX : ⇑f '' I ⊆ ⇑f '' X<GOAL>∃ I₀ X₀, M.Basis I₀ X₀ ∧ ⇑f '' I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s<GOAL>IsInteger R (a • 0)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s<GOAL>IsInteger R 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s<VAR>x y : P<VAR>hx : IsInteger R (a • x)<VAR>hy : IsInteger R (a • y)<GOAL>IsInteger R (a • (x + y))
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s<VAR>x y : P<VAR>hx : IsInteger R (a • x)<VAR>hy : IsInteger R (a • y)<GOAL>IsInteger R (a • x + a • y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s✝ : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s✝, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s✝, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s✝<VAR>s : R<VAR>x : P<VAR>hx : IsInteger R (a • x)<GOAL>IsInteger R (a • s • x)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>s✝ : Set P<VAR>x✝ : ∃ a ∈ S, ∀ b ∈ s✝, IsInteger R (a • b)<VAR>a : R<VAR>a_mem : a ∈ S<VAR>h : ∀ b ∈ s✝, IsInteger R (a • b)<VAR>b : P<VAR>hb : b ∈ span R s✝<VAR>s : R<VAR>x : P<VAR>hx : IsInteger R (a • x)<GOAL>IsInteger R (s • a • x)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace α'<VAR>F : ι → X → α'<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>interior s ∈ 𝓤 α
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>interior s ∈ (𝓤 α).lift' interior
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>h : f.HasEigenvalue μ<VAR>n : ℕ<GOAL>(f ^ n).HasEigenvalue (μ ^ n)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>h : f.HasEigenvalue μ<VAR>n : ℕ<GOAL>∃ x ∈ (f ^ n).eigenspace (μ ^ n), x ≠ 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>h : f.HasEigenvalue μ<VAR>n : ℕ<VAR>m : M<VAR>hm : f.HasEigenvector μ m<GOAL>∃ x ∈ (f ^ n).eigenspace (μ ^ n), x ≠ 0
<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>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))<VAR>h₃ : EquicontinuousWithinAt F S x₀<VAR>U : Set α<VAR>hU : U ∈ 𝓝 (f x₀)<GOAL>U ∈ map f (𝓝[S] x₀)
<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>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))<VAR>h₃ : EquicontinuousWithinAt F S x₀<VAR>U : Set α<VAR>hU : U ∈ 𝓝 (f x₀)<GOAL>f ⁻¹' U ∈ 𝓝[S] x₀
<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>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))<VAR>h₃ : EquicontinuousWithinAt F S x₀<VAR>U : Set α<VAR>hU : U ∈ 𝓝 (f x₀)<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVU : ball (f x₀) V ⊆ U<GOAL>f ⁻¹' U ∈ 𝓝[S] x₀
<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>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : Tendsto (fun x => F x x₀) l (𝓝 (f x₀))<VAR>h₃ : EquicontinuousWithinAt F S x₀<VAR>U : Set α<VAR>hU : U ∈ 𝓝 (f x₀)<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVU : ball (f x₀) V ⊆ U<VAR>W : Set (α × α)<VAR>hW : W ∈ 𝓤 α<VAR>hWclosed : IsClosed W<VAR>hWV : W ⊆ V<GOAL>f ⁻¹' U ∈ 𝓝[S] x₀
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>update f i '' Ioc a (f i) = Ioc (update f i a) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>μs : ι → Measure α<VAR>i : ι<VAR>hνμ : ν ≪ μs i<GOAL>ν ≪ sum μs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>μs : ι → Measure α<VAR>i : ι<VAR>hνμ : ν ≪ μs i<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : (sum μs) s = 0<GOAL>ν s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>μs : ι → Measure α<VAR>i : ι<VAR>hνμ : ν ≪ μs i<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs0 : ∀ (i : ι), (μs i) s = 0<GOAL>ν s = 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), a * x * x + b * x + c ≤ 0<GOAL>∀ (x : K), 0 ≤ -a * x * x + -b * x + -c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hg : f.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>G : α<VAR>G0 : G > 0<VAR>hG : ∀ (i : ℕ), abv (↑g i) < G<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abv (↑f j) < ε / G<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>abv (↑(f * g) j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hg : f.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>G : α<VAR>G0 : G > 0<VAR>hG : ∀ (i : ℕ), abv (↑g i) < G<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abv (↑f j) < ε / G<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>this : abv (↑f j) * abv (↑g j) < ε / G * G<GOAL>abv (↑(f * g) j) < ε
<VAR>α✝ : Type<VAR>inst✝¹ : Finite α✝<VAR>B : Stonean<VAR>X : α✝ → Stonean<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Z : α → Stonean<VAR>a : α<GOAL>OpenEmbedding ⇑(Sigma.ι Z a)
<VAR>α✝ : Type<VAR>inst✝¹ : Finite α✝<VAR>B : Stonean<VAR>X : α✝ → Stonean<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Z : α → Stonean<VAR>a : α<GOAL>OpenEmbedding (⇑(CompHausLike.homeoOfIso (coproductIsoCoproduct Z).symm) ∘ ⇑(Sigma.ι Z a))
<VAR>α✝ : Type<VAR>inst✝¹ : Finite α✝<VAR>B : Stonean<VAR>X : α✝ → Stonean<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Z : α → Stonean<VAR>a : α<VAR>e_2✝ : ↑(finiteCoproduct Z).toTop = (forget Stonean).obj (finiteCoproduct Z)<GOAL>⇑(CompHausLike.homeoOfIso (coproductIsoCoproduct Z).symm) ∘ ⇑(Sigma.ι Z a) = ⇑(finiteCoproduct.ι Z a)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<VAR>m : ℕ<GOAL>((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<VAR>m : ℕ<VAR>H : ((X ^ p ^ 1 - C y) ^ m).roots = (m * p ^ 1) • {(iterateFrobeniusEquiv R p 1).symm y}<GOAL>((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<VAR>hr : r < 1<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ≥0∞<VAR>hr : 1 ≤ r<GOAL>∑' (n : ℕ), r ^ n = (1 - r)⁻¹
<VAR>R✝ : Type u<VAR>M : Type v<VAR>inst✝⁵ : Ring R✝<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝² : StrongRankCondition R✝<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : StrongRankCondition R<VAR>n m : ℕ<VAR>v : Fin m → Fin n → R<VAR>h : LinearIndependent R v<GOAL>m ≤ n
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<VAR>a : A<GOAL>ℑ (z • a) = z.re • ℑ a + z.im • ℜ a
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<VAR>a : A<VAR>this : ℑ (z • a) = ℑ ((↑z.re + ↑z.im * I) • a)<GOAL>ℑ (z • a) = z.re • ℑ a + z.im • ℜ a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>U : Opens ↑X<VAR>x : ↥U<VAR>V : Opens ↑Y<VAR>hV : unop (op U) ≤ (Opens.map f).obj V<GOAL>((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x ≫ stalkPullbackHom C f F ↑x = ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ((pullback C f).obj F).germ x
<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>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>t : Set F<VAR>hl : DifferentiableWithinAt 𝕜 l t (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hs : MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = f x<GOAL>derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)
<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✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsLeast s b<GOAL>IsLeast (insert a s) (min a b)
<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✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsLeast s b<GOAL>IsLeast ({a} ∪ s) (min a b)
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃ a, a ≠ 1 ∧ a ≠ -1
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>x y : ℤ<VAR>prop : x ^ 2 - d * y ^ 2 = 1<VAR>hy : y ≠ 0<GOAL>∃ a, a ≠ 1 ∧ a ≠ -1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<GOAL>(X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hd : d ∣ n<VAR>hdn : d < n<GOAL>(X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hd : d ∣ n<VAR>hdn : d < n<VAR>h0n : 0 < n<GOAL>(X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>d n : ℕ<VAR>h : d ∈ n.properDivisors<VAR>hd : d ∣ n<VAR>hdn : d < n<VAR>h0n : 0 < n<VAR>h0d : 0 < d<GOAL>(X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<GOAL>truncateFun n (m • x) = m • truncateFun n x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<GOAL>∀ {n : ℕ∞}, ContDiff 𝕜 n cexp
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>n : ℕ<GOAL>ContDiff 𝕜 ↑n cexp
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>n : ℕ<VAR>this : ContDiff ℂ ↑n cexp<GOAL>ContDiff 𝕜 ↑n cexp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>h₁ : a ≤ b<VAR>h₂ : ¬IsMax b<GOAL>Ico a (succ b) = insert b (Ico a b)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hμν : ν ≤ μ<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm f p ν ≤ eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hμν : ν ≤ μ<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>hX : s ∈ P.parts<GOAL>↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>hX : s ∈ P.parts<VAR>h✝ : IsEmpty α<GOAL>↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>hX : s ∈ P.parts<VAR>h✝ : Nonempty α<GOAL>↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>s t : Finset α<VAR>P : Finpartition univ<VAR>ε : ℝ<VAR>hP₁ : P.IsEquipartition<VAR>hP₃ : P.parts.card ≤ bound (ε / 8) ⌈4 / ε⌉₊<VAR>hX : s ∈ P.parts<VAR>h✝ : Nonempty α<VAR>this : 0 < P.parts.card<GOAL>↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑s.card
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>s : Set X<GOAL>IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<GOAL>∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<VAR>x : X<VAR>ℱ : Filter X<VAR>hℱ₁ : ℱ.NeBot<VAR>hℱ₂ : ℱ ≤ 𝓟 s<VAR>hℱ₃ : ℱ ≤ 𝓝 x<GOAL>x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝¹ : T2Space X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>s : Set X<VAR>h : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)<VAR>x : X<VAR>ℱ : Filter X<VAR>hℱ₁ : ℱ.NeBot<VAR>hℱ₂ : ℱ ≤ 𝓟 s<VAR>hℱ₃ : ℱ ≤ 𝓝 x<VAR>K : Set X<VAR>hK : IsCompact K<VAR>K_mem : K ∈ 𝓝 x<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : Filter α<VAR>s : Set α<GOAL>Disjoint f (𝓟 s) ↔ sᶜ ∈ f