ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<GOAL>∀ {x : ℂ}, x ∈ stolzSet M → ‖x - 1‖ < ε / 4 / (F + 1) → ‖∑' (n : ℕ), f n * x ^ n - l‖ < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<GOAL>‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>p : Tendsto (fun n => (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))<GOAL>‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>p : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε<GOAL>‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>B₂ : ℕ<VAR>hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2<GOAL>‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>B₂ : ℕ<VAR>hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2<GOAL>‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>B₂ : ℕ<VAR>hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2<GOAL>‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 2
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>B₂ : ℕ<VAR>hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2<VAR>S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4<GOAL>‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 2
<VAR>f : ℕ → ℂ<VAR>l : ℂ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>M : ℝ<VAR>hM : 1 < M<VAR>s : ℕ → ℂ := fun n => ∑ i ∈ range n, f i<VAR>g : ℂ → ℂ := fun z => ∑' (n : ℕ), f n * z ^ n<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>B₁ : ℕ<VAR>hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M<VAR>F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖<VAR>z : ℂ<VAR>zn : ‖z‖ < 1<VAR>zm : ‖1 - z‖ < M * (1 - ‖z‖)<VAR>zd : ‖z - 1‖ < ε / 4 / (F + 1)<VAR>B₂ : ℕ<VAR>hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2<VAR>S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4<VAR>S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4<GOAL>‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 2
<VAR>x : ℝ<GOAL>Tendsto (fun y => Icc y x) (𝓝[<] x) ((vitaliFamily volume 1).filterAt x)
<VAR>x : ℝ<GOAL>∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ (vitaliFamily volume 1).setsAt x
<VAR>x : ℝ<GOAL>∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>t : Finset V<VAR>h : ¬AffineIndependent k Subtype.val<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>H₁ H₂ : Subgroup G<GOAL>H₁ ⊓ H₂ ≤ ⊥ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>z : ↑((Proj.structureSheaf 𝒜).presheaf.stalk x)<GOAL>homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x) z) = z
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<GOAL>homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x) (((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s)) = ((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), (fun x => ↑s ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<GOAL>homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x) (((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s)) = ((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<GOAL>homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x) (((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s)) = ((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<GOAL>((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, ⋯⟩) (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) = ((Proj.structureSheaf 𝒜).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<GOAL>((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op) (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) = ((Proj.structureSheaf 𝒜).presheaf.map i.op) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<GOAL>↑(((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op) (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ })) = ↑(((Proj.structureSheaf 𝒜).presheaf.map i.op) s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<VAR>t : ↑(ProjectiveSpectrum.top 𝒜)<VAR>ht : t ∈ unop (op V)<GOAL>HomogeneousLocalization.val (↑(((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op) (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ })) ⟨t, ht⟩) = HomogeneousLocalization.val (↑(((Proj.structureSheaf 𝒜).presheaf.map i.op) s) ⟨t, ht⟩)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>U : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((Proj.structureSheaf 𝒜).presheaf.obj (op U))<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>hxV : ↑⟨x, hxU⟩ ∈ V<VAR>i : V ⟶ unop (op U)<VAR>n : ℕ<VAR>a b : ↥(𝒜 n)<VAR>h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal<VAR>e : ∀ (x : ↥V), ↑s ⟨↑x, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }<VAR>t : ↑(ProjectiveSpectrum.top 𝒜)<VAR>ht : t ∈ unop (op V)<GOAL>HomogeneousLocalization.val (↑(sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) ((fun x_1 => ⟨↑x_1, ⋯⟩) ⟨t, ht⟩)) = HomogeneousLocalization.val (↑s ((fun x => ⟨↑x, ⋯⟩) ⟨t, ht⟩))
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s t : Multiset α<GOAL>map f s = map f t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s t : Multiset α<GOAL>Rel (fun a b => f a = f b) s t ↔ Rel (fun x x_1 => x = x_1) s t
<VAR>p q : ℕ+ → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>h : ∃ n, p n<VAR>n✝ m n : ℕ+<GOAL>n < PNat.find h ↔ ∀ m ≤ n, ¬p m
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1<VAR>hf : HasConstantSpeedOnWith f (φ '' s) 1<VAR>x : ℝ<VAR>xs : x ∈ s<GOAL>EqOn φ (fun y => y - x + φ x) s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>φ : ℝ → ℝ<VAR>φm : MonotoneOn φ s<VAR>hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1<VAR>hf : HasConstantSpeedOnWith f (φ '' s) 1<VAR>x : ℝ<VAR>xs : x ∈ s<VAR>x✝ : ℝ<GOAL>x✝ - x = ↑1 / ↑1 * (x✝ - x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<VAR>e : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm<GOAL>∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : V<VAR>e : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm<GOAL>∫ (x : EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ V))), cexp (-b * ↑‖e x‖ ^ 2 + c * ↑⟪w, e x⟫_ℝ) ∂volume = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝³ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : NonUnitalNonAssocSemiring T<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>a : R<GOAL>a ∈ Set.center R ↔ AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝³ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : NonUnitalNonAssocSemiring T<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>a : R<GOAL>((∀ (a_1 : R), a * a_1 = a_1 * a) ∧ (∀ (b c : R), a * (b * c) = a * b * c) ∧ (∀ (a_1 c : R), a_1 * a * c = a_1 * (a * c)) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔ AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧ AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g✝ : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>B : ι →ᵇᵃ[↑I] ℝ<VAR>hB0 : ∀ (J : Box ι), 0 ≤ B J<VAR>g : ι →ᵇᵃ[↑I] F<VAR>H : ℝ≥0 → ∀ x ∈ Box.Icc I, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J<GOAL>∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ ∅, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → (McShane.bHenstock = true → x ∈ Box.Icc J) → (McShane.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>⟪x, x⟫_𝕜 = ↑‖x‖ ^ 2
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>s : Set N<VAR>f : G ≃* N<GOAL>normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>s : Set N<VAR>f : G ≃* N<VAR>this : ⇑f.toEquiv ⁻¹' s = ⇑f.symm '' s<GOAL>normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq k<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Semiring α<VAR>b₁ b₂ : n<VAR>hb : b₁ ≠ b₂<VAR>a : m<VAR>c : k<GOAL>(single a b₁).toMatrix * (single b₂ c).toMatrix = 0
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>inst✝ : Epi f<GOAL>Function.Surjective ⇑f
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>inst✝ : Epi f<VAR>r : ¬Function.Surjective ⇑f<GOAL>False
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>inst✝ : Epi f<VAR>b : ↑B<VAR>hb : ∀ (a : ↑A), f a ≠ b<GOAL>False
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<GOAL>K.sieves (G.obj X) (Sieve.functorPushforward G ⊤)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X : C<GOAL>K.sieves (G.obj X) ⊤
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<GOAL>Sieve.pullback iYX S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) Y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<GOAL>∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj Y⦄, (Sieve.functorPushforward G (Sieve.functorPullback G ↑⟨Sieve.pullback (G.map iYX) (Sieve.functorPushforward G S), ⋯⟩)).arrows f → Sieve.pullback f (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ K.sieves Y_1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>Z : D<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>iZU : Z ⟶ G.obj U<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<GOAL>Sieve.pullback (iZU ≫ G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ K.sieves Z
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>Z : D<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>iZU : Z ⟶ G.obj U<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<GOAL>Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈ K.sieves Z
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>Z : D<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>iZU : Z ⟶ G.obj U<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<GOAL>Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ K.sieves (G.obj U)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.2513, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.2520, u_2} D<VAR>G : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type v<VAR>inst✝³ : Category.{u, v} A<VAR>inst✝² : G.LocallyCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>inst✝ : G.IsLocallyFaithful K<VAR>X Y : C<VAR>S : Sieve X<VAR>iYX : Y ⟶ X<VAR>hS : S ∈ (fun X S => K.sieves (G.obj X) (Sieve.functorPushforward G S)) X<VAR>U : C<VAR>iUY : U ⟶ Y<VAR>W : C<VAR>iWX : W ⟶ X<VAR>iUW : G.obj U ⟶ G.obj W<VAR>hiWX : S.arrows iWX<VAR>e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX<GOAL>Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)) ∈ K.sieves (G.obj U)