ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<GOAL>(Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩ ≫ LocalRing.residue ↑(Y.presheaf.stalk (f.val.base ↑x))) ≫ LocalRing.ResidueField.map (Hom.stalkMap f ↑x) = f.val.c.app (op V) ≫ X.presheaf.germ x ≫ LocalRing.residue ↑(X.presheaf.stalk ↑x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<GOAL>Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩ ≫ LocalRing.residue ↑(Y.presheaf.stalk (f.val.base ↑x)) ≫ LocalRing.ResidueField.map (Hom.stalkMap f ↑x) = f.val.c.app (op V) ≫ X.presheaf.germ x ≫ LocalRing.residue ↑(X.presheaf.stalk ↑x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<VAR>a : (forget CommRingCat).obj (Y.presheaf.obj (op V))<GOAL>(Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩ ≫ LocalRing.residue ↑(Y.presheaf.stalk (f.val.base ↑x)) ≫ LocalRing.ResidueField.map (Hom.stalkMap f ↑x)) a = (f.val.c.app (op V) ≫ X.presheaf.germ x ≫ LocalRing.residue ↑(X.presheaf.stalk ↑x)) a
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<VAR>a : (forget CommRingCat).obj (Y.presheaf.obj (op V))<GOAL>(LocalRing.ResidueField.map (Hom.stalkMap f ↑x)) ((LocalRing.residue ↑(Y.presheaf.stalk (f.val.base ↑x))) ((Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩) a)) = (X.presheaf.germ x ≫ LocalRing.residue ↑(X.presheaf.stalk ↑x)) ((f.val.c.app (op V)) a)
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : Opens ↑Y.toTopCat<VAR>x : ↥((Opens.map f.val.base).obj V)<VAR>a : (forget CommRingCat).obj (Y.presheaf.obj (op V))<GOAL>(LocalRing.residue ↑(X.presheaf.stalk ↑x)) ((X.presheaf.germ ⟨↑x, ⋯⟩) ((f.val.c.app (op V)) a)) = (X.presheaf.germ x ≫ LocalRing.residue ↑(X.presheaf.stalk ↑x)) ((f.val.c.app (op V)) a)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<GOAL>∃ y ∈ s, infDist x s = dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<GOAL>∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t✝ u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<VAR>t : Set α := s ∩ closedBall x (dist z x)<GOAL>∃ y ∈ s, infDist x t = dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t✝ u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<VAR>t : Set α := s ∩ closedBall x (dist z x)<VAR>htc : IsCompact t<GOAL>∃ y ∈ s, infDist x t = dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t✝ u : Set α<VAR>x✝ y : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<VAR>t : Set α := s ∩ closedBall x (dist z x)<VAR>htc : IsCompact t<VAR>htne : t.Nonempty<GOAL>∃ y ∈ s, infDist x t = dist x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>s t✝ u : Set α<VAR>x✝ y✝ : α<VAR>Φ : α → β<VAR>inst✝ : ProperSpace α<VAR>h : IsClosed s<VAR>x z : α<VAR>hz : z ∈ s<VAR>t : Set α := s ∩ closedBall x (dist z x)<VAR>htc : IsCompact t<VAR>htne : t.Nonempty<VAR>y : α<VAR>hyd : infDist x t = dist x y<VAR>hys : y ∈ s<GOAL>∃ y ∈ s, infDist x t = dist x y
<VAR>p q : ℚ≥0<GOAL>0 < q.num ↔ 0 < q
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<GOAL>span {↑(absNorm I)} ≤ I
<VAR>α : Type u_1<VAR>rels : Set (FreeGroup α)<VAR>this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of<GOAL>Subgroup.closure (Set.range of) = ⊤
<VAR>α : Type u_1<VAR>rels : Set (FreeGroup α)<VAR>this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of<GOAL>(QuotientGroup.mk' (Subgroup.normalClosure rels)).range = ⊤
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, IsOpen (s a)<GOAL>IsOpen (i.pi s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>i : Set ι<VAR>s : (a : ι) → Set (π a)<VAR>hi : i.Finite<VAR>hs : ∀ a ∈ i, IsOpen (s a)<GOAL>IsOpen (⋂ a ∈ i, eval a ⁻¹' s a)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>c : ℝ<VAR>hf : Martingale f ℱ μ<GOAL>Martingale (c • f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>c : ℝ<VAR>hf : Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>μ[(c • f) j|↑ℱ i] =ᶠ[ae μ] (c • f) i
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>c : ℝ<VAR>hf : Martingale f ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : Ω<VAR>hx : (μ[f j|↑ℱ i]) x = f i x<GOAL>(c • μ[f j|↑ℱ i]) x = (c • f) i x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>f : β → ↑(Ici a)<VAR>l : Filter β<GOAL>Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ Fin.last n<VAR>x : { x // x ≠ p }<GOAL>(finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
<VAR>m n : ℕ<VAR>p : Fin (n + 1)<VAR>h : p ≠ Fin.last n<VAR>x : { x // x ≠ p }<GOAL>some ((finSuccAboveEquiv p).symm x) = some ((p.castLT ⋯).predAbove ↑x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ∆ c = a ∆ (b ∆ c)
<VAR>M : Type u_1<VAR>inst✝ : Distrib M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<VAR>x✝ : M<GOAL>(a + b) * x✝ = x✝ * (a + b)
<VAR>M : Type u_1<VAR>inst✝ : Distrib M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<VAR>x✝¹ x✝ : M<GOAL>(a + b) * (x✝¹ * x✝) = (a + b) * x✝¹ * x✝
<VAR>M : Type u_1<VAR>inst✝ : Distrib M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * (a + b) * x✝ = x✝¹ * ((a + b) * x✝)
<VAR>M : Type u_1<VAR>inst✝ : Distrib M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>hb : b ∈ center M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * x✝ * (a + b) = x✝¹ * (x✝ * (a + b))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>Disjoint (Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))) (LinearMap.ker (commMap K))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding.latticeBasis K))<VAR>h_zero : (commMap K) x = 0<GOAL>x = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>h_zero : (commMap K) x = 0<VAR>h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<GOAL>x = 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>h_zero : (commMap K) x = 0<VAR>h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<VAR>φ : K →+* ℂ<GOAL>x φ = 0 φ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (K →+* ℂ) → ℂ<VAR>h_zero : (commMap K) x = 0<VAR>h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<VAR>φ : K →+* ℂ<GOAL>x φ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>t 𝒰 f g i i = 𝟙 (v 𝒰 f g i i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map i) = pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map i) = pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<VAR>i : ℤ<GOAL>WittVector.ghostFun i.castDef = ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>inst✝ : One β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : ∀ᶠ (x : α) in l, f x ≠ 1<VAR>s t : Set α<VAR>h : s.mulIndicator f =ᶠ[l] t.mulIndicator f<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>E : Type u_4<VAR>inst✝ : One β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : ∀ᶠ (x : α) in l, f x ≠ 1<VAR>s t : Set α<VAR>h : s.mulIndicator f =ᶠ[l] t.mulIndicator f<VAR>this : ∀ {s : Set α}, Function.mulSupport (s.mulIndicator f) =ᶠ[l] s<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<GOAL>↑s = univ ↔ s = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<GOAL>Tendsto (fun n => eLpNorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<GOAL>Tendsto (fun n => eLpNorm (↑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<VAR>hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<VAR>hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal<VAR>h_bound : ∀ (n : ℕ), (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal) ≤ᶠ[ae μ] fun x => ↑‖f x - y₀‖₊ ^ p.toReal<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<VAR>hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal<VAR>h_bound : ∀ (n : ℕ), (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal) ≤ᶠ[ae μ] fun x => ↑‖f x - y₀‖₊ ^ p.toReal<VAR>h_fin : ∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ p.toReal ∂μ ≠ ⊤<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : eLpNorm (fun x => f x - y₀) p μ < ⊤<VAR>hp_zero : ¬p = 0<VAR>hp : 0 < p.toReal<VAR>hF_meas : ∀ (n : ℕ), Measurable fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal<VAR>h_bound : ∀ (n : ℕ), (fun x => ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal) ≤ᶠ[ae μ] fun x => ↑‖f x - y₀‖₊ ^ p.toReal<VAR>h_fin : ∫⁻ (a : β), ↑‖f a - y₀‖₊ ^ p.toReal ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun n => ↑‖↑(approxOn f hf s y₀ h₀ n) a - f a‖₊ ^ p.toReal) atTop (𝓝 0)<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ^ p.toReal ∂μ) atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousAt f x<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>inst✝ : TopologicalSpace β<VAR>k : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f univ x<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ IsBounded (f '' t)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s • t).IsPWO
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : PartialOrder G<VAR>inst✝² : PartialOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>((fun x => x.1 • x.2) '' s ×ˢ t).IsPWO
<VAR>p : ℕ<VAR>q : ℚ<VAR>hq : ¬q = 0<GOAL>0 ≤ ↑p ^ (-padicValRat p q)
<VAR>p : ℕ<VAR>q : ℚ<VAR>hq : ¬q = 0<GOAL>0 ≤ ↑p
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(AddOpposite.unop (addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : AddOpposite.unop (addOppositeEquiv x) = 0 then 0 else (AddOpposite.unop (addOppositeEquiv x)).coeff (⋯.min ⋯)) = AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : (fun a => AddOpposite.unop (x.coeff a)) = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) = AddOpposite.unop (if h : x = 0 then 0 else x.coeff (⋯.min ⋯))
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : ∀ (a : Γ), AddOpposite.unop (x.coeff a) = 0 a then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) = AddOpposite.unop (if h : ∀ (a : Γ), x.coeff a = coeff 0 a then 0 else x.coeff (⋯.min ⋯))
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(if h : ∀ (a : Γ), x.coeff a = 0 then 0 else AddOpposite.unop (x.coeff (⋯.min ⋯))) = AddOpposite.unop (if h : ∀ (a : Γ), x.coeff a = 0 then 0 else x.coeff (⋯.min ⋯))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p : P<VAR>v : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>s.secondInter p (r • v) = s.secondInter p v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p : P<VAR>v : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>(-2 * (r * ⟪v, p -ᵥ s.center⟫_ℝ) / r / r / ⟪v, v⟫_ℝ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ) • v +ᵥ p
<VAR>F✝ : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommMonoid β<VAR>s : Multiset ι<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>(map (fun i => f (g i)) s).prod = f (map g s).prod
<VAR>F✝ : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f✝ g✝ : ι → α<VAR>inst✝² : CommMonoid β<VAR>s : Multiset ι<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>map (fun i => f (g i)) s = map (⇑f) (map g s)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>hJ_ne_zero : J ≠ 0<VAR>hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J<VAR>ha_ne_zero : Ideal.span {a} ≠ 0<VAR>ha : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = ↑(Ideal.span {a})<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I