ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ iSup K ↔ ∃ i, x ∈ K i
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ iSup K → ∃ i, x ∈ K i
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<GOAL>x ∈ closure (⋃ i, ↑(K i)) → ∃ i, x ∈ K i
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<VAR>hx : x ∈ closure (⋃ i, ↑(K i))<GOAL>∃ i, 1 ∈ K i
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<VAR>hx : x ∈ closure (⋃ i, ↑(K i))<GOAL>∀ (x y : G), (∃ i, x ∈ K i) → (∃ i, y ∈ K i) → ∃ i, x * y ∈ K i
<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>H K✝ : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>hι : Nonempty ι<VAR>K : ι → Subgroup G<VAR>hK : Directed (fun x x_1 => x ≤ x_1) K<VAR>x : G<VAR>hx : x ∈ closure (⋃ i, ↑(K i))<GOAL>∀ (x : G), (∃ i, x ∈ K i) → ∃ i, x⁻¹ ∈ K i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>∃ x, ∫⁻ (a : α), f a ∂μ ≤ f x
<VAR>x : ℝ*<VAR>hx : x.Infinitesimal<GOAL>(-x).Infinitesimal
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<VAR>this : p * C p.leadingCoeff⁻¹ ≠ 1<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<VAR>this : p * C p.leadingCoeff⁻¹ ≠ 1<GOAL>(∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p * C p.leadingCoeff⁻¹) ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>u : ↥(center G₀ˣ)<VAR>r : G₀<GOAL>r * ↑↑u = ↑↑u * r
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>u : ↥(center G₀ˣ)<GOAL>0 * ↑↑u = ↑↑u * 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>u : ↥(center G₀ˣ)<VAR>r : G₀<VAR>hr : r ≠ 0<GOAL>r * ↑↑u = ↑↑u * r
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<VAR>g : PresentedGroup rels →* G<VAR>hg : ∀ (x : α), g (PresentedGroup.of x) = f x<VAR>x : PresentedGroup rels<GOAL>g x = (toGroup h) x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Group G<VAR>f : α → G<VAR>rels : Set (FreeGroup α)<VAR>h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1<VAR>g : PresentedGroup rels →* G<VAR>hg : ∀ (x : α), g (PresentedGroup.of x) = f x<VAR>x : PresentedGroup rels<GOAL>∀ (z : FreeGroup α), g ↑z = (toGroup h) ↑z
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : LocalizedModule S M<VAR>m : M<VAR>s : ↥S<GOAL>mk m s + 0 = mk m s
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : LocalizedModule S M<VAR>m : M<VAR>s : ↥S<GOAL>∃ u, u • s • s • m = u • (s * s) • m
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<GOAL>∃ A f a, IsGalois A ∧ F.map f a = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>A : C<VAR>a : ↑(F.obj A)<VAR>h1 : IsGalois A<VAR>h2 : Function.Bijective fun f => F.map f a<GOAL>∃ A f a, IsGalois A ∧ F.map f a = x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>A : C<VAR>a : ↑(F.obj A)<VAR>h1 : IsGalois A<VAR>h2 : Function.Bijective fun f => F.map f a<VAR>f : A ⟶ X<VAR>hf : (fun f => F.map f a) f = x<GOAL>∃ A f a, IsGalois A ∧ F.map f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>h : IsSFiniteKernel η<GOAL>κ ⊗ₖ η = Kernel.sum fun n => κ.seq n ⊗ₖ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>h : IsSFiniteKernel η<GOAL>(Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) = Kernel.sum fun n => κ.seq n ⊗ₖ η
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>h : IsSFiniteKernel η<VAR>n : ℕ<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s = ((κ.seq n ⊗ₖ η) a) s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f g : α → α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>f ∘ g ⁻¹' s = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace X<VAR>s₁ s₂ t₁ t₂ : Set X<VAR>s_sub : s₁ ⊆ s₂<VAR>t_sub : t₁ ⊆ t₂<VAR>u : ℕ → Set X<VAR>u_cov : s₂ ⊆ ⋃ n, u n<VAR>u_props : ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t₂<GOAL>HasSeparatingCover s₁ t₁
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<VAR>ha : 0 ≤ ⅟↑da<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<VAR>ha : 0 ≤ ⅟↑da<VAR>hb : 0 ≤ ⅟↑db<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<VAR>ha : 0 ≤ ⅟↑da<VAR>hb : 0 ≤ ⅟↑db<VAR>h : ⅟↑db * (↑(num✝¹.mul (Int.ofNat db)) * ⅟↑da) ≤ ⅟↑db * (↑(num✝.mul (Int.ofNat da)) * ⅟↑da)<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<VAR>ha : 0 ≤ ⅟↑da<VAR>hb : 0 ≤ ⅟↑db<VAR>h : ↑(num✝¹.mul (Int.ofNat db)) * ⅟↑db * ⅟↑da ≤ ⅟↑db * (↑(num✝.mul (Int.ofNat da)) * ⅟↑da)<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>num✝¹ num✝ : ℤ<VAR>da db : ℕ<VAR>inv✝¹ : Invertible ↑da<VAR>inv✝ : Invertible ↑db<VAR>h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true<VAR>h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))<VAR>ha : 0 ≤ ⅟↑da<VAR>hb : 0 ≤ ⅟↑db<VAR>h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝<GOAL>↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq α<GOAL>image2 f (↑s ∩ ↑s') ↑t ⊆ image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝¹ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>x✝ : E<VAR>x : E × E<GOAL>0 = e x.1 - e x.2 - e (x.1 - x.2)
<VAR>k : ℕ<VAR>c : Code<VAR>n x : ℕ<VAR>h : x ∈ evaln (k + 1) c n<GOAL>x ∈ c.eval n
<VAR>k n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : 0 = x<GOAL>x ∈ pure 0 n
<VAR>k n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : n + 1 = x<GOAL>x = n + 1
<VAR>k n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : (unpair n).1 = x<GOAL>x = (unpair n).1
<VAR>k n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : (unpair n).2 = x<GOAL>x = (unpair n).2
<VAR>k : ℕ<VAR>cf cg : Code<VAR>hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n<VAR>hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n<VAR>n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x<GOAL>∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x
<VAR>k : ℕ<VAR>cf cg : Code<VAR>hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n<VAR>hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n<VAR>n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x<GOAL>∃ a ∈ cg.eval n, x ∈ cf.eval a
<VAR>k : ℕ<VAR>cf cg : Code<VAR>hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n<VAR>hg : ∀ (n x : ℕ), x ∈ evaln (k + 1) cg n → x ∈ cg.eval n<VAR>n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : Nat.rec (evaln (k + 1) cf (unpair n).1) (fun n_1 n_ih => (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i => evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i))) (unpair n).2 = some x<GOAL>x ∈ Nat.rec (cf.eval (unpair n).1) (fun y IH => IH.bind fun i => cg.eval (Nat.pair (unpair n).1 (Nat.pair y i))) (unpair n).2
<VAR>k : ℕ<VAR>cf : Code<VAR>hf : ∀ (n x : ℕ), x ∈ evaln (k + 1) cf n → x ∈ cf.eval n<VAR>n x : ℕ<VAR>left✝ : n ≤ k<VAR>h : ∃ a, evaln (k + 1) cf n = some a ∧ (if a = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x<GOAL>∃ a, (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧ ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧ a + (unpair n).2 = x
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : Epi (homologyMap φ.τ₁ i)<VAR>h₂ : IsIso (homologyMap φ.τ₂ i)<VAR>h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)<VAR>h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)<GOAL>IsIso (homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : Epi (homologyMap φ.τ₁ i)<VAR>h₂ : IsIso (homologyMap φ.τ₂ i)<VAR>h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)<VAR>h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)<VAR>this : Mono (homologyMap φ.τ₃ i)<GOAL>IsIso (homologyMap φ.τ₃ i)
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Abelian C<VAR>c : ComplexShape ι<VAR>S S₁ S₂ : ShortComplex (HomologicalComplex C c)<VAR>φ : S₁ ⟶ S₂<VAR>hS₁ : S₁.ShortExact<VAR>hS₂ : S₂.ShortExact<VAR>i : ι<VAR>h₁ : Epi (homologyMap φ.τ₁ i)<VAR>h₂ : IsIso (homologyMap φ.τ₂ i)<VAR>h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)<VAR>h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)<VAR>this✝ : Mono (homologyMap φ.τ₃ i)<VAR>this : Epi (homologyMap φ.τ₃ i)<GOAL>IsIso (homologyMap φ.τ₃ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a⁻¹ ⊔ 1 = (fun x x_1 => x ⊔ x_1) 1 a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddGroup α<VAR>h1 : Periodic f c₁<VAR>h2 : Periodic f c₂<VAR>x : α<GOAL>f (x + (c₁ - c₂)) = f x
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.7894, u_1} C<VAR>inst✝⁸ : Category.{u_10, u_2} C₁<VAR>inst✝⁷ : Category.{u_9, u_3} C₂<VAR>inst✝⁶ : Category.{?u.7906, u_4} C₃<VAR>inst✝⁵ : Category.{u_11, u_5} D₁<VAR>inst✝⁴ : Category.{u_8, u_6} D₂<VAR>inst✝³ : Category.{?u.7918, u_7} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>Ψ : LocalizerMorphism W₂ W₃<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>L₃ : C₃ ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W₃<VAR>X Y Z : C₁<GOAL>Φ.homMap L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj (Φ.functor.obj X))
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>Continuous toProbabilityMeasure
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>SeqContinuous toProbabilityMeasure
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<GOAL>Tendsto (toProbabilityMeasure ∘ μs) atTop (𝓝 P)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<GOAL>∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑((toProbabilityMeasure ∘ μs) i)) atTop (𝓝 (∫ (ω : Ω), f ω ∂↑P))
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f : Ω →ᵇ ℝ<GOAL>∀ (f : Ω →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<GOAL>limsup (fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<VAR>norm_f_pos : 0 < ‖f‖<GOAL>limsup (fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<VAR>norm_f_pos : 0 < ‖f‖<GOAL>∀ (ε : ℝ), 0 < ε → limsup (fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<VAR>norm_f_pos : 0 < ‖f‖<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<GOAL>limsup (fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P + δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<VAR>norm_f_pos : 0 < ‖f‖<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<GOAL>∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)<VAR>ν : LevyProkhorov (ProbabilityMeasure Ω)<VAR>hμs : Tendsto μs atTop (𝓝 ν)<VAR>P : ProbabilityMeasure Ω := ν.toProbabilityMeasure<VAR>Ps : ℕ → ProbabilityMeasure Ω := fun n => (μs n).toProbabilityMeasure<VAR>f✝ f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>f_zero : ¬‖f‖ = 0<VAR>norm_f_pos : 0 < ‖f‖<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop fun i => ∫ (x : Ω), f x ∂↑((toProbabilityMeasure ∘ μs) i)
<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<GOAL>IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<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>n : R<VAR>hn : n ≠ 0<VAR>d : ↥R⁰<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = spanSingleton R⁰ (mk' K n d)
<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>n : R<VAR>hn : n ≠ 0<VAR>d : ↥R⁰<VAR>hd_ne_zero : (algebraMap R K) ↑d ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = spanSingleton R⁰ (mk' K n d)
<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>n : R<VAR>hn : n ≠ 0<VAR>d : ↥R⁰<VAR>hd_ne_zero : (algebraMap R K) ↑d ≠ 0<VAR>h0 : spanSingleton R⁰ (mk' K n d) ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = spanSingleton R⁰ (mk' K n d)
<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>n : R<VAR>hn : n ≠ 0<VAR>d : ↥R⁰<VAR>hd_ne_zero : (algebraMap R K) ↑d ≠ 0<VAR>h0 : spanSingleton R⁰ (mk' K n d) ≠ 0<VAR>hI : spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ ((algebraMap R K) ↑d)⁻¹ * ↑(Ideal.span {n})<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = spanSingleton R⁰ (mk' K n d)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>μ : Measure X<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>h : ∀ (s : Set X), diam s ≤ ε → μ s ≤ m (diam s)<GOAL>μ ≤ mkMetric m