ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤<VAR>hinv : ↑I * ↑I⁻¹ = 1<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<VAR>w : A<VAR>hw : w ∈ ↑↑I<VAR>hvw : w * v = 1<GOAL>(↑↑I).IsPrincipal
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<VAR>w : A<VAR>hw : w ∈ ↑↑I<VAR>hvw : w * v = 1<GOAL>↑↑I = Submodule.span R {w}
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<VAR>w : A<VAR>hw : w ∈ ↑↑I<VAR>hvw : w * v = 1<GOAL>↑(spanSingleton S w) = ↑↑I⁻¹⁻¹
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<VAR>w : A<VAR>hw : w ∈ ↑↑I<VAR>hvw : w * v = 1<GOAL>↑I⁻¹ * spanSingleton S w ≤ 1
<VAR>R✝ : Type u_1<VAR>inst✝⁴ : CommRing R✝<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>hinv : ↑I * ↑I⁻¹ = 1<VAR>J : Submodule R R := Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v})<VAR>h : J = ⊤<VAR>hJ : IsLocalization.coeSubmodule A J = ↑↑I * Submodule.span R {v}<VAR>this : 1 ∈ ↑↑I * Submodule.span R {v}<VAR>w : A<VAR>hw : w ∈ ↑↑I<VAR>hvw : w * v = 1<GOAL>1 ≤ ↑I⁻¹ * spanSingleton S w
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>h : ∀ (g : α), g • ↑s = op g • ↑s<VAR>a : α<VAR>ha : a ∈ s<VAR>g : α<GOAL>g * a * g⁻¹ ∈ ↑s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>h : ∀ (g : α), g • ↑s = op g • ↑s<VAR>a : α<VAR>ha : a ∈ s<VAR>g : α<GOAL>g * a ∈ g • ↑s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>M : MeasurableSet (Set.Ioc (-A) A)<GOAL>∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>M : MeasurableSet (Set.Ioc (-A) A)<GOAL>∫ (x : α), (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>M : MeasurableSet (Set.Ioc (-A) A)<GOAL>∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ = ∫ (x : ℝ), (Set.Ioc (-A) A).indicator (fun x => x ^ n) x ∂Measure.map f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>M : MeasurableSet (Set.Ioc (-A) A)<GOAL>-A ≤ A
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<VAR>hA : 0 ≤ A<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>M : MeasurableSet (Set.Ioc (-A) A)<GOAL>AEStronglyMeasurable (fun z => (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x : E<GOAL>IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<GOAL>x ^ z ≤ x
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : x ≤ 1<VAR>h_one_le : 1 ≤ z<GOAL>x ^ z ≤ x ^ 1
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n + ℵ₀ = ℵ₀
<VAR>x✝ y z a x : ℝ<VAR>ha : a < 0<GOAL>HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - rexp (log a * x) * sin (x * π) * π) x
<VAR>n : ℕ<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>f : ((i : Fin n) → p i) → τ<VAR>args : (i : Fin n) → p i<GOAL>(curry f).uncurry args = f args
<VAR>α : Type u_1<VAR>xs : LazyList α<GOAL>xs.append (Thunk.pure nil) = xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : Monoid β<VAR>inst✝ : LipschitzMul β<GOAL>∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : Monoid β<VAR>inst✝ : LipschitzMul β<GOAL>LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>hy : M ≤ Submonoid.comap g T<VAR>Q : Type u_4<VAR>inst✝³ : CommRing Q<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization T Q<VAR>inst✝ : IsLocalization M S<VAR>h : IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁴ : CommRing P<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>hy : M ≤ Submonoid.comap g T<VAR>Q : Type u_4<VAR>inst✝³ : CommRing Q<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization T Q<VAR>inst✝ : IsLocalization M S<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>K✝ : Type u<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f g : K[X]<VAR>hg : g ≠ 0<GOAL>(idealX K).valuation (RatFunc.mk f g) = (idealX K).intValuation f / (idealX K).intValuation g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(𝟭 C).map f✝ ≫ (fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X))) Y✝ = (fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X))) X✝ ≫ (F ⋙ G).map f✝
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(adj.homEquiv ((𝟭 C).obj X✝) (F.obj Y✝)) (F.map ((𝟭 C).map f✝) ≫ 𝟙 (F.obj Y✝)) = (adj.homEquiv ((𝟭 C).obj X✝) (F.obj Y✝)) (𝟙 (F.obj X✝) ≫ F.map f✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X✝ Y✝ : D<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(G ⋙ F).map f✝ ≫ (fun Y => (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y))) Y✝ = (fun Y => (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y))) X✝ ≫ (𝟭 D).map f✝
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X✝ Y✝ : D<VAR>f✝ : X✝ ⟶ Y✝<GOAL>(adj.homEquiv (G.obj X✝) ((𝟭 D).obj Y✝)).symm (G.map f✝ ≫ 𝟙 (G.obj Y✝)) = (adj.homEquiv (G.obj X✝) ((𝟭 D).obj Y✝)).symm (𝟙 (G.obj X✝) ≫ G.map ((𝟭 D).map f✝))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>(adj.homEquiv X Y) f = { app := fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X)), naturality := ⋯ }.app X ≫ G.map f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>(adj.homEquiv X Y) f = (adj.homEquiv ((𝟭 C).obj X) Y) (𝟙 (F.obj X) ≫ f)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X : C<VAR>Y : D<VAR>f : X ⟶ G.obj Y<GOAL>(adj.homEquiv X Y).symm f = F.map f ≫ { app := fun Y => (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y)), naturality := ⋯ }.app Y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : CoreHomEquiv F G<VAR>X : C<VAR>Y : D<VAR>f : X ⟶ G.obj Y<GOAL>(adj.homEquiv X Y).symm f = (adj.homEquiv X ((𝟭 D).obj Y)).symm (f ≫ 𝟙 (G.obj Y))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>h : ∀ (a b : α), b ∈ f a → a = b<VAR>l : List α<GOAL>lookmap f l = l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>h : ∀ (a b : α), b ∈ f a → a = b<VAR>l : List α<GOAL>∀ (a b : α), b ∈ f a → id a = id b
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n i : ℕ<GOAL>((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i) 1 = ((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i) 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n i : ℕ<GOAL>∑ x ∈ Finset.range (i + 1), (lcoeff R n) (X ^ x * C r ^ (i - x) * ↑(i.choose x)) = ↑(i.choose n) * r ^ (i - n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n i : ℕ<GOAL>(if n < i + 1 then r ^ (i - n) * ↑(i.choose n) else 0) = r ^ (i - n) * ↑(i.choose n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>n i : ℕ<VAR>h : i + 1 ≤ n<GOAL>0 = r ^ (i - n) * ↑(i.choose n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>i : LocallyConnectedSpace Y<VAR>h : X ≃ₜ Y<VAR>this : ∀ (x : X), (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x<GOAL>LocallyConnectedSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>i : LocallyConnectedSpace Y<VAR>h : X ≃ₜ Y<VAR>this : ∀ (x : X), (𝓝 x).HasBasis (fun s => IsOpen s ∧ h x ∈ s ∧ IsConnected s) fun x => ⇑h.symm '' x<VAR>x✝¹ : X<VAR>x✝ : Set Y<VAR>hs : IsOpen x✝ ∧ h x✝¹ ∈ x✝ ∧ IsConnected x✝<GOAL>IsPreconnected (⇑h.symm '' x✝)
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>Continuous ⇑(toWOT 𝕜 E F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 F<GOAL>Continuous fun a => y (((toWOT 𝕜 E F) a) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : E<VAR>y : NormedSpace.Dual 𝕜 F<GOAL>Continuous fun a => y (a x)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<GOAL>Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<GOAL>∀ (X : C) (S : J.Cover X) (x y : (forget D).obj ((J.plusObj P).obj (op X))), (∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y) → x = y
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : J.Cover X<VAR>x y : (forget D).obj ((J.plusObj P).obj (op X))<GOAL>(∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y) → x = y
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>β : Type u_1<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>hf : Inducing f<GOAL>FirstCountableTopology α
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<VAR>hIX : M.Basis I X<GOAL>M.Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<VAR>hIX : M.Basis I X<VAR>h : ¬M.Base I<GOAL>False
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e✝ : α<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<VAR>hIX : M.Basis I X<VAR>h : ¬M.Base I<VAR>e : α<VAR>heBI : e ∈ B \ I<VAR>he : M.Indep (insert e I)<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>(c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>(c ∈ Set.Ico a (a + p) ∧ ∃ z, b - z • p = c) → toIcoMod hp a b = c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>n✝ n : ℤ<VAR>hc : b - n • p ∈ Set.Ico a (a + p)<GOAL>toIcoMod hp a b = b - n • p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfm : Monotone f<VAR>k : ℕ<VAR>ha : Antitone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log (abs z)) - ↑π * I))
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>𝓝 (↑(Real.log (abs z)) - ↑π * I) = 𝓝 ((ofReal' ∘ fun x => Real.log (abs x)) z + ↑(-π) * I)
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>abs z ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>convexBodySumFun x = ∑ w : { w // w.IsReal }, ‖x.1 w‖ + 2 * ∑ w : { w // w.IsComplex }, ‖x.2 w‖
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>∑ x_1 ∈ Finset.subtype IsReal Finset.univ, ↑(↑x_1).mult * (normAtPlace ↑x_1) x + ∑ x_1 ∈ Finset.subtype (fun x => x.IsComplex) Finset.univ, ↑(↑x_1).mult * (normAtPlace ↑x_1) x = ∑ x_1 ∈ Finset.subtype IsReal Finset.univ, ‖x.1 x_1‖ + ∑ i ∈ Finset.subtype IsComplex Finset.univ, 2 * ‖x.2 i‖
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ✝ : Type u_3<VAR>inst✝ : Preorder α<VAR>β γ : Type u_4<VAR>f : α → Part (β → γ)<VAR>g : α → Part β<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => Seq.seq (f x) fun x_1 => g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>ha : (Iio a).Nonempty<GOAL>frontier (Iio a) = {a}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G✝ : Type u_4<VAR>inst✝¹² : Mul G✝<VAR>inst✝¹¹ : TopologicalSpace G✝<VAR>inst✝¹⁰ : ChartedSpace H G✝<VAR>inst✝⁹ : SmoothMul I G✝<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>g✝ h✝ : G✝<VAR>G : Type u_8<VAR>inst✝³ : Semigroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : ChartedSpace H G<VAR>inst✝ : SmoothMul I G<VAR>g h x✝ : G<GOAL>(𝑳 I (g * h)) x✝ = ((𝑳 I g).comp (𝑳 I h)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : DivisionSemiring γ<VAR>inst✝ : Module γ α<VAR>h : Periodic f c<VAR>a : γ<GOAL>Periodic (fun x => f (a⁻¹ • x)) (a • c)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o.card ↔ 1 ≤ o
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>ι : Type u_1<VAR>inst✝ : T0Space α<VAR>V₀ : Set (α × α)<VAR>V₀_in : V₀ ∈ 𝓤 α<VAR>f : ι → α<VAR>hf : Pairwise fun x y => (f x, f y) ∉ V₀<VAR>x y : ι<VAR>h : f x ≠ f y<GOAL>(f x, f y) ∉ V₀
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiff ℝ ⊤ (stereoInvFunAux v)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>h₀ : ContDiff ℝ ⊤ fun w => ‖w‖ ^ 2<GOAL>ContDiff ℝ ⊤ (stereoInvFunAux v)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>h₀ : ContDiff ℝ ⊤ fun w => ‖w‖ ^ 2<VAR>h₁ : ContDiff ℝ ⊤ fun w => (‖w‖ ^ 2 + 4)⁻¹<GOAL>ContDiff ℝ ⊤ (stereoInvFunAux v)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>h₀ : ContDiff ℝ ⊤ fun w => ‖w‖ ^ 2<VAR>h₁ : ContDiff ℝ ⊤ fun w => (‖w‖ ^ 2 + 4)⁻¹<VAR>h₂ : ContDiff ℝ ⊤ fun w => 4 • w + (‖w‖ ^ 2 - 4) • v<GOAL>ContDiff ℝ ⊤ (stereoInvFunAux v)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>x ⊓ y ⊔ x ⊓ yᶜ = x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * ‖a • x + b • y‖ ^ 2 = a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * (a ^ 2 * ‖x‖ ^ 2 + 2 * (a * (b * ⟪x, y⟫_ℝ)) + b ^ 2 * ‖y‖ ^ 2) = a * f x + b * f y - m / 2 * a * b * (‖x‖ ^ 2 - 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2)