ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op V))<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>hpW : ↑((fun x => ⟨↑x, ⋯⟩) p) ∈ W<VAR>iWU : W ⟶ unop (op U)<VAR>h : (isFractionPrelocal R).pred fun x => ↑s ((fun x => ⟨↑x, ⋯⟩) x)<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯) (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) = ↑(((structureSheaf R).val.map iVU.op) s) p
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op V))<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>hpW : ↑((fun x => ⟨↑x, ⋯⟩) p) ∈ W<VAR>iWU : W ⟶ unop (op U)<VAR>h : (isFractionPrelocal R).pred fun x => ↑s ((fun x => ⟨↑x, ⋯⟩) x)<VAR>a b : R<VAR>h' : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s ((fun x => ⟨↑x, ⋯⟩) x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯) (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) = ↑(((structureSheaf R).val.map iVU.op) s) p
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>p : ↥(unop (op V))<VAR>W : Opens ↑(PrimeSpectrum.Top R)<VAR>hpW : ↑((fun x => ⟨↑x, ⋯⟩) p) ∈ W<VAR>iWU : W ⟶ unop (op U)<VAR>h : (isFractionPrelocal R).pred fun x => ↑s ((fun x => ⟨↑x, ⋯⟩) x)<VAR>a b : R<VAR>h' : ∀ (x : ↥W), ∃ (hs : b ∉ (↑x).asIdeal), ↑s ((fun x => ⟨↑x, ⋯⟩) x) = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) a ⟨b, hs⟩<VAR>hb₁ : b ∉ (↑⟨↑p, hpW⟩).asIdeal<VAR>s_eq₁ : ↑s ⟨↑p, ⋯⟩ = IsLocalization.mk' (Localization.AtPrime (↑p).asIdeal) a ⟨b, hb₁⟩<VAR>hb₂ : b ∉ (↑⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, hpW⟩).asIdeal<VAR>s_eq₂ : ↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩ = IsLocalization.mk' (Localization.AtPrime ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal) a ⟨b, hb₂⟩<GOAL>(Localization.localRingHom ((PrimeSpectrum.comap (RingHom.id R)) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯) (↑s ⟨(PrimeSpectrum.comap (RingHom.id R)) ↑p, ⋯⟩) = ↑(((structureSheaf R).val.map iVU.op) s) p
<VAR>α✝ β α : Type u<VAR>n : ℕ<GOAL>#α = ↑n ↔ Nonempty (α ≃ Fin n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f μ<GOAL>Integrable f ((μ univ)⁻¹ • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f 0<GOAL>Integrable f ((0 univ)⁻¹ • 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f μ<VAR>hne : μ ≠ 0<GOAL>Integrable f ((μ univ)⁻¹ • μ)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>v : m → α<GOAL>‖col ι v‖₊ = ‖v‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<GOAL>⋂₀ S = (⋃₀ (compl '' S))ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b✝ : α<VAR>inst✝ : LE α<VAR>a : WithBot α<VAR>h : a ≠ ⊥<VAR>b : α<GOAL>a.unbot h ≤ b ↔ a ≤ ↑b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>mellin f s = ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>∫ (x : ℝ) in univ, |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (s - 1) • f ((rexp ∘ Neg.neg) x) = ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>u : ℝ<GOAL>-↑s.im * ↑u = ↑(-2 * π * (u * (s.im / (2 * π))))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>u : ℝ<GOAL>↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>u : ℝ<VAR>this : 2 * ↑π ≠ 0<GOAL>↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<GOAL>∫ (u : ℝ), cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u)) = 𝓕 (fun u => rexp (-s.re * u) • f (rexp (-u))) (s.im / (2 * π))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G'.neighborSet v)<VAR>inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)<GOAL>G'.spanningCoe.degree v = G'.degree v
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G'.neighborSet v)<VAR>inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)<GOAL>Fintype.card ↑(G'.spanningCoe.neighborSet v) = Fintype.card ↑(G'.neighborSet v)
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ 1 ≤ y ^ (1 / z) ↔ x ^ z ≤ y
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (z * z⁻¹) ≤ y ^ (1 / z) ↔ x ^ z ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a✝ : α<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>hr : RightUnique r<VAR>a : List α<VAR>b : List β<VAR>h₁ : Forall₂ r a b<VAR>c : List α<VAR>d : List β<VAR>h₂ : Forall₂ r c d<VAR>h : a ~ c<VAR>this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d<GOAL>((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>a b : WithTop α<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<GOAL>map f a ≤ map f b ↔ a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>a b : WithTop α<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<GOAL>∀ {a b : αᵒᵈ}, (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) a ≤ (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) b ↔ a ≤ b
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin (p.length + q.length + 1)<VAR>H : ¬↑i < p.length<GOAL>p.length ≤ ↑i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin (p.length + q.length + 1)<VAR>H : ¬↑i < p.length<GOAL>↑i < p.length + (q.length + 1)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin (p.length + q.length + 1)<VAR>H : ¬↑i < p.length<GOAL>↑i < p.length + q.length + 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>n : ℕ<VAR>y : F<VAR>h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<GOAL>(minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>n : ℕ<VAR>y : F<VAR>h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>hnezero : X ^ q ^ n - C y ≠ 0<GOAL>(minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>n : ℕ<VAR>y : F<VAR>h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>hnezero : X ^ q ^ n - C y ≠ 0<GOAL>1 ≤ (minpoly F x).natSepDegree
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>n : ℕ<VAR>y : F<VAR>h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0<VAR>hnezero : X ^ q ^ n - C y ≠ 0<GOAL>1 ≤ (minpoly F x).natDegree
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝³ : Category.{uD', uD} D<VAR>inst✝² : HasZeroMorphisms D<VAR>P Q W X Y Z : C<VAR>inst✝¹ : HasBinaryBiproduct W X<VAR>inst✝ : HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>inl ≫ map f g = f ≫ inl
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝³ : Category.{uD', uD} D<VAR>inst✝² : HasZeroMorphisms D<VAR>P Q W X Y Z : C<VAR>inst✝¹ : HasBinaryBiproduct W X<VAR>inst✝ : HasBinaryBiproduct Y Z<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>inl ≫ map' f g = f ≫ inl
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.homologyIsoSc' i j k hi hk).inv ≫ K.homologyι j = (K.sc' i j k).homologyι ≫ (K.opcyclesIsoSc' i j k hi hk).inv
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>a + -a ≡ b + -b [ZMOD n]
<VAR>m n a b c d : ℤ<VAR>h : a ≡ b [ZMOD n]<GOAL>0 ≡ 0 [ZMOD n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mod α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma % mb ∈ a % b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mod α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>∃ a_1 ∈ a, ∃ a ∈ b, a_1 % a = ma % mb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : R1Space α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.Regular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<GOAL>(μ.restrict A).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : R1Space α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.Regular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this : (μ.restrict A).WeaklyRegular<GOAL>(μ.restrict A).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : R1Space α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.Regular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this : (μ.restrict A).WeaklyRegular<VAR>V : Set α<VAR>hV : IsOpen V<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) V<GOAL>∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : R1Space α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : μ.Regular<VAR>A : Set α<VAR>h'A : μ A ≠ ⊤<VAR>this : (μ.restrict A).WeaklyRegular<VAR>V : Set α<VAR>hV : IsOpen V<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) V<VAR>R : (μ.restrict A) V ≠ ⊤<GOAL>∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>f : E →ₗ[𝕜] 𝕜<VAR>r : ℝ<GOAL>f.toSeminorm.ball 0 r = {x | ‖f x‖ < r}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℝ<GOAL>logDeriv rexp x✝ = 1 x✝
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>B : Set (α ⊕ β)<GOAL>(M.sum N).Base B ↔ M.Base (Sum.inl ⁻¹' B) ∧ N.Base (Sum.inr ⁻¹' B)
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>B : Set (α ⊕ β)<GOAL>M.Base ((fun a => a.down) '' (Sigma.mk false ⁻¹' ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) '' ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ∧ N.Base ((fun a => a.down) '' (Sigma.mk true ⁻¹' ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) '' ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' B)))) ↔ M.Base (Sum.inl ⁻¹' B) ∧ N.Base (Sum.inr ⁻¹' B)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimalPrimes R<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsLocalization.AtPrime S I<VAR>J K : Ideal S<VAR>inst✝¹ : J.IsPrime<VAR>inst✝ : K.IsPrime<VAR>i₁ i₂ : { i // i.IsPrime ∧ i ≤ I }<GOAL>↑i₁ = ↑i₂
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hMin : I ∈ minimals (fun x x_1 => x ≤ x_1) (setOf Ideal.IsPrime)<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsLocalization.AtPrime S I<VAR>J K : Ideal S<VAR>inst✝¹ : J.IsPrime<VAR>inst✝ : K.IsPrime<VAR>i₁ i₂ : { i // i.IsPrime ∧ i ≤ I }<GOAL>↑i₁ = ↑i₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : HasDistribNeg M<VAR>l : List M<GOAL>(map Neg.neg l).prod = (-1) ^ l.length * l.prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort u_6<VAR>s✝ t u : Set α<VAR>ι : Sort u_7<VAR>m : ι → MeasurableSpace α<VAR>s : Set α<GOAL>MeasurableSet s ↔ GenerateMeasurable {s | ∃ i, MeasurableSet s} s
<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>b : ℝ<VAR>hb : 0 < b<GOAL>∫ (v : V), rexp (-b * ‖v‖ ^ 2) = (π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)
<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>b : ℝ<VAR>hb : 0 < b<GOAL>↑(∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ↑((π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2))
<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>b : ℝ<VAR>hb : 0 < b<GOAL>↑(∫ (v : V), rexp (-b * ‖v‖ ^ 2)) = ∫ (v : V), cexp (-↑b * ↑‖v‖ ^ 2)
<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>b : ℝ<VAR>hb : 0 < b<GOAL>↑((π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)) = (↑π / ↑b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)
<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 : Ideal R<VAR>hI : I ≠ 0<GOAL>{x | ↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) ≠ 1}.Finite
<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 : Ideal R<VAR>hI : I ≠ 0<GOAL>{x | ¬x.asIdeal ^ (Associates.mk x.asIdeal).count (Associates.mk I).factors = 1}.Finite
<VAR>X : CondensedSet<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<GOAL>∀ (i : (T : CompHaus) × X.val.obj (Opposite.op T)), Continuous fun a => CondensedSet.coinducingCoprod X ⟨i, a⟩
<VAR>X : CondensedSet<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous (CondensedSet.coinducingCoprod X)
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddBelow S<GOAL>∃ x, IsGLB S x
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddBelow S<VAR>hne' : (-S).Nonempty<GOAL>∃ x, IsGLB S x
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddBelow S<VAR>hne' : (-S).Nonempty<VAR>hbdd' : BddAbove (-S)<GOAL>∃ x, IsGLB S x
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddBelow S<VAR>hne' : (-S).Nonempty<VAR>hbdd' : BddAbove (-S)<GOAL>IsGLB S (-Classical.choose ⋯)
<VAR>S : Set ℝ<VAR>hne : S.Nonempty<VAR>hbdd : BddBelow S<VAR>hne' : (-S).Nonempty<VAR>hbdd' : BddAbove (-S)<GOAL>IsLUB (-S) (Classical.choose ⋯)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : α → E<VAR>a : Filter α<VAR>b : E<GOAL>Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0)
<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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' 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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, ↑f_1 ≤ 𝓝 x
<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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>𝒰 : Ultrafilter X<VAR>h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)<GOAL>∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
<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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>𝒰 : Ultrafilter X<VAR>h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K<GOAL>∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
<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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>𝒰 : Ultrafilter X<VAR>h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K<VAR>y : Y<VAR>hyK : y ∈ K<VAR>hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y<GOAL>∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
<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>h : IsProperMap f<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>𝒰 : Ultrafilter X<VAR>h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K<VAR>x : X<VAR>hx : ↑𝒰 ≤ 𝓝 x<VAR>hyK : f x ∈ K<VAR>hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 (f x)<GOAL>∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x
<VAR>a b c d m n : ℤ<VAR>P : ℤ → Sort u_1<VAR>lt : (n : ℤ) → n < m → P n<VAR>ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n<GOAL>∀ (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k
<VAR>a b c d m n✝ : ℤ<VAR>P : ℤ → Sort u_1<VAR>lt : (n : ℤ) → n < m → P n<VAR>ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n<VAR>n : ℤ<VAR>x✝ : n ≥ m<VAR>ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1<VAR>hn : m ≤ n<GOAL>Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k
<VAR>a b c d m n✝ : ℤ<VAR>P : ℤ → Sort u_1<VAR>lt : (n : ℤ) → n < m → P n<VAR>ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n<VAR>n : ℤ<VAR>x✝ : n ≥ m<VAR>ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1<VAR>hn : m ≤ n<GOAL>ge n ⋯ (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯) fun n_1 x hn l x => hn l ⋯) = ge n hn fun k x => Int.strongRec lt ge k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>(B.restrict (B.orthogonal (Submodule.span K {x}))).Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>m : ↥(B.orthogonal (Submodule.span K {x}))<VAR>hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0<VAR>n : V<GOAL>(B ↑m) n = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁷ : CommRing R₁<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>m : ↥(B.orthogonal (Submodule.span K {x}))<VAR>hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0<VAR>n : V<VAR>this : n ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})<GOAL>(B ↑m) n = 0