ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝² : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝¹ : NormalSpace X<VAR>inst✝ : ParacompactSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hsV : s ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : ι), V i ⊆ U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝² : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝¹ : NormalSpace X<VAR>inst✝ : ParacompactSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hsV : s ⊆ ⋃ i, V i<VAR>hVf : LocallyFinite V<VAR>hVU : ∀ (i : ι), V i ⊆ U i<VAR>f : BumpCovering ι X s<VAR>hfp : ∀ (i : ι), p ⇑(f i)<VAR>hf : f.IsSubordinate V<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b✝ a b : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<GOAL>a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p : P<VAR>l : L<VAR>q : P<VAR>hq : q ∉ l<GOAL>lineCount L q = pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p : P<VAR>l : L<VAR>q : P<VAR>hq : q ∉ l<VAR>val✝ : Fintype P<GOAL>lineCount L q = pointCount P l
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p : P<VAR>l : L<VAR>q : P<VAR>hq : q ∉ l<VAR>val✝¹ : Fintype P<VAR>val✝ : Fintype L<GOAL>lineCount L q = pointCount P l
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g✝ : Filter α<VAR>s t : Set α<VAR>f g : Filter α<GOAL>(f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝¹¹ : CommRing R✝<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Ring B<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R✝ A<VAR>inst✝⁶ : Algebra R✝ B<VAR>f✝¹ : R✝ →+* S<VAR>f✝ : R✝ →+* B<VAR>f : R✝ →+* S<VAR>R : Type u_5<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Algebra S B<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsScalarTower R S B<VAR>x : B<VAR>r : R<VAR>hx : IsIntegral S x<GOAL>r • x ∈ Algebra.adjoin S {x}
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝¹¹ : CommRing R✝<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Ring B<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R✝ A<VAR>inst✝⁶ : Algebra R✝ B<VAR>f✝¹ : R✝ →+* S<VAR>f✝ : R✝ →+* B<VAR>f : R✝ →+* S<VAR>R : Type u_5<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Algebra S B<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsScalarTower R S B<VAR>x : B<VAR>r : R<VAR>hx : IsIntegral S x<GOAL>(algebraMap R S) r • x ∈ Algebra.adjoin S {x}
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝¹¹ : CommRing R✝<VAR>inst✝¹⁰ : CommRing A<VAR>inst✝⁹ : Ring B<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R✝ A<VAR>inst✝⁶ : Algebra R✝ B<VAR>f✝¹ : R✝ →+* S<VAR>f✝ : R✝ →+* B<VAR>f : R✝ →+* S<VAR>R : Type u_5<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R B<VAR>inst✝² : Algebra S B<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsScalarTower R S B<VAR>x : B<VAR>r : R<VAR>hx : IsIntegral S x<GOAL>x ∈ Algebra.adjoin S {x}
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Preorder α<VAR>a b c : α<GOAL>Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>h4v : x + 4 • v ∈ interior s<VAR>h4w : x + 4 • w ∈ interior s<GOAL>(f'' w) v = (f'' v) w
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>h4v : x + 4 • v ∈ interior s<VAR>h4w : x + 4 • w ∈ interior s<VAR>A : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2<GOAL>(f'' w) v = (f'' v) w
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx : HasFDerivWithinAt f' f'' (interior s) x<VAR>v w : E<VAR>h4v : x + 4 • v ∈ interior s<VAR>h4w : x + 4 • w ∈ interior s<VAR>A : (fun h => h ^ 2 • ((f'' w) v - (f'' v) w)) =o[𝓝[>] 0] fun h => h ^ 2<VAR>B : (fun x => (f'' w) v - (f'' v) w) =o[𝓝[>] 0] fun x => 1<GOAL>(f'' w) v = (f'' v) w
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>m : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>f : (a : α) → a ∈ m → β a<GOAL>f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>t : (a : α) → Multiset (β a)<VAR>f : (a : α) → a ∈ 0 → β a<GOAL>f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>m : Multiset α<VAR>ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a<VAR>f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1<GOAL>f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>m : Multiset α<VAR>ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a<VAR>f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1<GOAL>(∃ a_1 ∈ t a, ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<GOAL>∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<GOAL>∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<GOAL>∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<VAR>c : E<VAR>hc : c ∈ Cᶜ<GOAL>∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<VAR>c : E<VAR>hc : c ∈ Cᶜ<VAR>h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<VAR>c : E<VAR>hc : c ∈ Cᶜ<VAR>h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅<GOAL>Disjoint ((convexHull 𝕜) (insert c C)) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<VAR>c : E<VAR>hc : c ∈ Cᶜ<VAR>h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅<GOAL>Disjoint (⋃ y ∈ (convexHull 𝕜) C, segment 𝕜 c y) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>hst : Disjoint s t<VAR>S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}<VAR>C : Set E<VAR>hC : C ∈ S<VAR>hsC : s ⊆ C<VAR>hCmax : ∀ a ∈ S, C ⊆ a → a = C<VAR>x : E<VAR>hx : x ∈ Cᶜ<VAR>y : E<VAR>hy : y ∈ Cᶜ<VAR>z : E<VAR>hz : z ∈ segment 𝕜 x y<VAR>hzC : z ∈ C<VAR>c : E<VAR>hc : c ∈ Cᶜ<VAR>h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅<VAR>a : E<VAR>ha : a ∈ (convexHull 𝕜) C<GOAL>a ∈ C
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>hf : S.W f<VAR>n : ℤ<GOAL>S.W ((shiftFunctor C n).map f)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>hf : S.W f<VAR>n : ℤ<GOAL>S.W (n.negOnePow • (shiftFunctor C n).map f)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>n : ℤ<VAR>X₃ : C<VAR>g : X₂ ⟶ X₃<VAR>h : X₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>hT : Triangle.mk f g h ∈ distinguishedTriangles<VAR>mem : S.P X₃<GOAL>S.W (n.negOnePow • (shiftFunctor C n).map f)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x y : E ⟶ P.obj (op S)<VAR>h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op<GOAL>x = y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x y : E ⟶ P.obj (op S)<VAR>h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op<GOAL>∀ (I_1 : GrothendieckTopology.Cover.Arrow ⟨ofArrows X f, hf⟩), x ≫ P.map I_1.f.op = y ≫ P.map I_1.f.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : IsSheaf J P<VAR>I : Type u_1<VAR>S : C<VAR>X : I → C<VAR>f : (i : I) → X i ⟶ S<VAR>hf : ofArrows X f ∈ J.sieves S<VAR>E : A<VAR>x y : E ⟶ P.obj (op S)<VAR>h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op<VAR>Z Y : C<VAR>i : I<VAR>g : Z ⟶ X i<GOAL>x ≫ P.map ((f i).op ≫ g.op) = y ≫ P.map ((f i).op ≫ g.op)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)).toFinsupp
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>toFinsupp✝¹ toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp = (∑ i ∈ { toFinsupp := toFinsupp✝¹ }.support, { toFinsupp := toFinsupp✝ }.sum fun j a => (monomial (i + j)) ({ toFinsupp := toFinsupp✝¹ }.coeff i * a)).toFinsupp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>stieltjesOfMeasurableRat (fun p => f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>{ toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p => f p.2) ((), a), mono' := ⋯, right_continuous' := ⋯ } = { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun p => toRatCDF f p.2) ((), a), mono' := ⋯, right_continuous' := ⋯ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<VAR>x : ℝ<VAR>p : Unit × α<GOAL>toRatCDF (fun p => f p.2) p = toRatCDF f p.2
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<GOAL>imageSieve f a ∈ K.sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<GOAL>∀ ⦃Y : D⦄ ⦃f_1 : Y ⟶ X⦄, (Sieve.coverByImage H X).arrows f_1 → Sieve.pullback f_1 (imageSieve f a) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback g (imageSieve f a) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback lift (Sieve.pullback map (imageSieve f a)) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<GOAL>Sieve.pullback map (imageSieve f a) ∈ K.sieves (H.obj Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<VAR>hh : Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a)) ∈ K.sieves (H.obj (Opposite.unop (Opposite.op Z)))<GOAL>Sieve.pullback map (imageSieve f a) ∈ K.sieves (H.obj Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<VAR>hh : Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a)) ∈ K.sieves (H.obj (Opposite.unop (Opposite.op Z)))<GOAL>Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))) ∈ K.sieves (H.obj Z)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<VAR>hh : Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a)) ∈ K.sieves (H.obj (Opposite.unop (Opposite.op Z)))<GOAL>imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a) ≤ Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<VAR>hh : Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a)) ∈ K.sieves (H.obj (Opposite.unop (Opposite.op Z)))<VAR>W : C<VAR>q : W ⟶ Z<VAR>x : (forget A).obj ((H.op ⋙ F).obj (Opposite.op W))<VAR>h : ((whiskerLeft H.op f).app (Opposite.op W)) x = ((H.op ⋙ G).map q.op) ((forget A).map (G.map map.op) a)<GOAL>(Sieve.functorPullback H (Sieve.pullback map (imageSieve f a))).arrows q
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : Category.{u_4, u_1} C<VAR>inst✝⁴ : Category.{u_5, u_2} D<VAR>inst✝³ : Category.{u_6, u_3} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>H : C ⥤ D<VAR>F G : Dᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>inst✝² : ConcreteCategory A<VAR>hH : CoverPreserving J K H<VAR>inst✝¹ : H.IsCoverDense K<VAR>inst✝ : IsLocallySurjective J (whiskerLeft H.op f)<VAR>X : D<VAR>a : (forget A).obj (G.obj (Opposite.op X))<VAR>Y : D<VAR>g : Y ⟶ X<VAR>Z : C<VAR>lift : Y ⟶ H.obj Z<VAR>map : H.obj Z ⟶ X<VAR>fac : lift ≫ map = g<VAR>hh : Sieve.functorPushforward H (imageSieve (whiskerLeft H.op f) ((forget A).map (G.map map.op) a)) ∈ K.sieves (H.obj (Opposite.unop (Opposite.op Z)))<VAR>W : C<VAR>q : W ⟶ Z<VAR>x : (forget A).obj ((H.op ⋙ F).obj (Opposite.op W))<VAR>h : ((whiskerLeft H.op f).app (Opposite.op W)) x = ((H.op ⋙ G).map q.op) ((forget A).map (G.map map.op) a)<GOAL>(imageSieve f a).arrows (H.map q ≫ map)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>w x y z : V<VAR>hwx : Submodule.span ℝ {w} = Submodule.span ℝ {x}<VAR>hyz : Submodule.span ℝ {y} = Submodule.span ℝ {z}<GOAL>2 • o.oangle w y = 2 • o.oangle x z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n✝ m✝ l n m : ℕ<GOAL>filter (fun x => x = m) (range n) = if m < n then {m} else ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n✝ m✝ l n m : ℕ<GOAL>(fun x => x = m) = Eq m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n✝ m✝ l n m : ℕ<GOAL>m < n ↔ m ∈ range n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C✝ C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : ∀ (i : ι), f.f i = g.f i<GOAL>f.f = g.f
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C✝ C D : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h : ∀ (i : ι), f.f i = g.f i<VAR>x✝ : ι<GOAL>f.f x✝ = g.f x✝