ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i k' : ℕ<VAR>hi : abv (∑ i ∈ range (k' + max n i), f i - ∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + max n i), a k - ∑ k ∈ range (max n i), a k<GOAL>abv (f (k' + max n i) + ∑ x ∈ range (k' + max n i), f x - ∑ x ∈ range (max n i), f x) ≤ a (k' + max n i) + ∑ x ∈ range (k' + max n i), a x - ∑ x ∈ range (max n i), a x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i k' : ℕ<VAR>hi : abv (∑ i ∈ range (k' + max n i), f i - ∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + max n i), a k - ∑ k ∈ range (max n i), a k<GOAL>abv (f (k' + max n i) + (∑ x ∈ range (k' + max n i), f x + -∑ x ∈ range (max n i), f x)) ≤ a (k' + max n i) + (∑ x ∈ range (k' + max n i), a x + -∑ x ∈ range (max n i), a x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i k' : ℕ<VAR>hi : abv (∑ i ∈ range (k' + max n i), f i - ∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + max n i), a k - ∑ k ∈ range (max n i), a k<GOAL>abv (f (k' + max n i)) + abv (∑ x ∈ range (k' + max n i), f x + -∑ x ∈ range (max n i), f x) ≤ a (k' + max n i) + (∑ x ∈ range (k' + max n i), a x + -∑ x ∈ range (max n i), a x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i k' : ℕ<VAR>hi : abv (∑ i ∈ range (k' + max n i), f i + -∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + max n i), a k + -∑ k ∈ range (max n i), a k<GOAL>abv (f (k' + max n i)) + abv (∑ x ∈ range (k' + max n i), f x + -∑ x ∈ range (max n i), f x) ≤ a (k' + max n i) + (∑ x ∈ range (k' + max n i), a x + -∑ x ∈ range (max n i), a x)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Ici b = Iic (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ici b = Iic (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ici b = Iic (a - b)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : ArithmeticFunction R<VAR>h_mult : f.IsMultiplicative<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>(ArithmeticFunction.prodPrimeFactors fun p => (↑ζ + f) p) n = ∑ d ∈ n.divisors, f d
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>inst✝ : Nontrivial α<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>inst✝ : Nontrivial α<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ Associates.mk p ≤ Associates.mk a
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>inst✝ : Nontrivial α<VAR>h : Associates.mk p ≤ Associates.mk a<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>inst✝ : Nontrivial α<VAR>h : 1 ≤ (Associates.mk p).count (Associates.mk a).factors<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsIntegrallyClosedIn A B<VAR>inst✝ : Algebra.IsIntegral R A<GOAL>IsIntegralClosure A R B
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsIntegrallyClosedIn A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>x : B<GOAL>(∃ y, (algebraMap A B) y = x) → IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsIntegrallyClosedIn A B<VAR>inst✝ : Algebra.IsIntegral R A<VAR>y : A<GOAL>IsIntegral R ((algebraMap A B) y)
<VAR>x : PGame<GOAL>x.birthday = 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs₀ : IsClosed s<VAR>hs₁ : StrictConvex 𝕜 s<VAR>a : E<VAR>ha : a ∈ frontier s<VAR>b : E<VAR>hb : b ∈ frontier s<VAR>c : E<VAR>hc : c ∈ frontier s<VAR>habc : a + c = b + b<GOAL>a = b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs₀ : IsClosed s<VAR>hs₁ : StrictConvex 𝕜 s<VAR>a : E<VAR>ha : a ∈ frontier s<VAR>c : E<VAR>hc : c ∈ frontier s<VAR>hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s<VAR>habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)<GOAL>a = (1 / 2) • a + (1 / 2) • c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs₀ : IsClosed s<VAR>hs₁ : StrictConvex 𝕜 s<VAR>a : E<VAR>ha : a ∈ frontier s<VAR>c : E<VAR>hc : c ∈ frontier s<VAR>hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s<VAR>habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)<VAR>this : a = c<GOAL>a = (1 / 2) • a + (1 / 2) • c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs₀ : IsClosed s<VAR>hs₁ : StrictConvex 𝕜 s<VAR>a : E<VAR>ha : a ∈ frontier s<VAR>c : E<VAR>hc : c ∈ frontier s<VAR>hb : (1 / 2) • a + (1 / 2) • c ∈ frontier s<VAR>habc : a + c = (1 / 2) • a + (1 / 2) • c + ((1 / 2) • a + (1 / 2) • c)<VAR>this : a = c<GOAL>c = (2⁻¹ + 2⁻¹) • c
<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>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋂ b ∈ s, f b)ᶜ
<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>m : MeasurableSpace α<VAR>f : β → Set α<VAR>s : Set β<VAR>hs : s.Countable<VAR>h : ∀ b ∈ s, MeasurableSet (f b)<GOAL>MeasurableSet (⋃ i ∈ s, (f i)ᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k✝ : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>k : β → α<VAR>l : Filter β<GOAL>f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>IsSeparator G ↔ (preadditiveCoyonedaObj (op G)).Faithful
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>(preadditiveCoyonedaObj (op G) ⋙ forget₂ (ModuleCat (End (op G))) AddCommGrp).Faithful ↔ (preadditiveCoyonedaObj (op G)).Faithful
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>x y : (forget D).obj ((J.plusObj P).obj (op X))<VAR>h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) x = ((J.plusObj P).map I.f.op) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>y : (forget D).obj ((J.plusObj P).obj (op X))<VAR>Sx : J.Cover X<VAR>x : Meq P Sx<VAR>h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) (mk x) = ((J.plusObj P).map I.f.op) y<GOAL>mk x = y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), ((J.plusObj P).map I.f.op) (mk x) = ((J.plusObj P).map I.f.op) (mk y)<GOAL>mk x = mk y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<GOAL>mk x = mk y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<GOAL>mk x = mk y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<GOAL>∃ W h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<VAR>B : J.Cover X := S.bind W<GOAL>∃ W h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<VAR>B : J.Cover X := S.bind W<GOAL>∃ h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<VAR>B : J.Cover X := S.bind W<VAR>ex : B ⟶ Sx := homOfLE ⋯<GOAL>∃ h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<VAR>B : J.Cover X := S.bind W<VAR>ex : B ⟶ Sx := homOfLE ⋯<VAR>ey : B ⟶ Sy := homOfLE ⋯<GOAL>∃ h1 h2, x.refine h1 = y.refine h2
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S Sx : J.Cover X<VAR>x : Meq P Sx<VAR>Sy : J.Cover X<VAR>y : Meq P Sy<VAR>h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)<VAR>W : (I : S.Arrow) → J.Cover I.Y<VAR>h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx<VAR>h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy<VAR>hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)<VAR>B : J.Cover X := S.bind W<VAR>ex : B ⟶ Sx := homOfLE ⋯<VAR>ey : B ⟶ Sy := homOfLE ⋯<GOAL>x.refine ex = y.refine ey
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<VAR>A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<VAR>A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n<VAR>g_cont : Continuous g<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<VAR>A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n<VAR>g_cont : Continuous g<VAR>g_surj : Surjective g<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<VAR>A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n<VAR>g_cont : Continuous g<VAR>g_surj : Surjective g<VAR>s_closed : IsClosed s<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>inst✝³ : MetricSpace α<VAR>inst✝² : CompleteSpace α<VAR>inst✝¹ : SecondCountableTopology α<VAR>inst✝ : Nonempty α<VAR>this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat<VAR>I0 : 0 < 1 / 2<VAR>I1 : 1 / 2 < 1<VAR>u : ℕ → α<VAR>hu : DenseRange u<VAR>s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}<VAR>g : ↑s → α := fun x => Set.Nonempty.some ⋯<VAR>A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n<VAR>g_cont : Continuous g<VAR>g_surj : Surjective g<VAR>s_closed : IsClosed s<VAR>f : (ℕ → ℕ) → ↑s<VAR>f_surj : Surjective f<VAR>f_cont : Continuous f<GOAL>∃ f, Continuous f ∧ Surjective f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝¹ : IsFiniteMeasure ℙ<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>f : E → ℝ≥0∞<VAR>hmf : AEMeasurable f μ<GOAL>ℙ Set.univ ≠ ⊤
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<GOAL>psum σ R 0 = ↑(Fintype.card σ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Fintype τ<GOAL>↑univ.card = ↑(Fintype.card σ)