ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝⁵ : TopologicalSpace X<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)<GOAL>φ f - φ 0 = φ f
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<GOAL>Pi.topologicalSpace = Pi.topologicalSpace
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>s t : Set α<VAR>hs : AnalyticSet s<VAR>ht : AnalyticSet t<VAR>h : Disjoint s t<GOAL>MeasurablySeparable s t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>s t : Set α<VAR>hs : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s<VAR>ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t<VAR>h : Disjoint s t<GOAL>MeasurablySeparable s t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : T2Space α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>f : (ℕ → ℕ) → α<VAR>f_cont : Continuous f<VAR>g : (ℕ → ℕ) → α<VAR>g_cont : Continuous g<VAR>h : Disjoint (range f) (range g)<GOAL>MeasurablySeparable (range f) (range g)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : α → β<GOAL>(∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} ⊆ {p | edist p.1 p.2 < i'}) ↔ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : α → β<GOAL>(∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 E F<VAR>p : FormalMultilinearSeries 𝕜 E E<VAR>v : Fin 0 → E<GOAL>(q.comp p 0) v = (q 0) v
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>frontier s ⊆ s ↔ IsClosed s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<GOAL>(fun x => (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} = (fun p => p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x₁ x₂ : E<VAR>y : F<VAR>a : 𝕜 × 𝕜<VAR>ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}<GOAL>(a.1 • x₁ + a.2 • x₂, y) = a.1 • (x₁, y) + a.2 • (x₂, y)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<VAR>this : DecidableEq α<VAR>s' : Finset α := {a, b}<GOAL>∏ x ∈ s, f x = f a * f b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<VAR>this : DecidableEq α<VAR>s' : Finset α := {a, b}<VAR>hu : s' ⊆ s<GOAL>∏ x ∈ s, f x = f a * f b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<VAR>this : DecidableEq α<VAR>s' : Finset α := {a, b}<VAR>hu : s' ⊆ s<VAR>hf : ∀ c ∈ s, c ∉ s' → f c = 1<GOAL>∏ x ∈ s, f x = f a * f b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hn : a ≠ b<VAR>h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1<VAR>this : DecidableEq α<VAR>s' : Finset α := {a, b}<VAR>hu : s' ⊆ s<VAR>hf : ∀ c ∈ s, c ∉ s' → f c = 1<GOAL>∏ x ∈ s', f x = f a * f b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A : Cᵒᵖ ⥤ Type v<VAR>F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : YonedaCollection F Y<GOAL>(map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst
<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>n.dist m = m - n
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>β : α → Type u_3<VAR>inst✝ : Fintype α<GOAL>Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod n<GOAL>orderOf (r i) = n / n.gcd i.val
<VAR>n : ℕ<VAR>inst✝ : NeZero n<VAR>i : ZMod n<GOAL>orderOf (r ↑i.val) = n / n.gcd i.val
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>IsClosed (Set.range ⇑(comap f))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>hf : Surjective ⇑f<GOAL>IsClosed (zeroLocus ↑(ker f))
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F E<GOAL>⊥ = ⊤ ↔ finrank F E = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F E<VAR>this : Module.Free F ↥⊤<GOAL>⊥ = ⊤ ↔ finrank F E = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>x✝ x : E<GOAL>x ∈ support (fderiv 𝕜 f) → x ∈ tsupport f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>x✝ x : E<GOAL>x ∉ tsupport f → fderiv 𝕜 f x = 0
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<GOAL>EqOn f Gamma (Ioi 0)
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<GOAL>EqOn (log ∘ f) (log ∘ Gamma) (Ioi 0)
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>(log ∘ f) x = (log ∘ Gamma) x
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - (log ∘ f) 1))<GOAL>(log ∘ f) x = (log ∘ Gamma) x
<VAR>f : ℝ → ℝ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y<VAR>hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y<VAR>hf_one : f 1 = 1<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y
<VAR>c : Char<VAR>it : Iterator<VAR>h : it.Valid<GOAL>(it.setCurr c).Valid
<VAR>c : Char<VAR>it : Iterator<VAR>h✝ : it.Valid<VAR>l r : List Char<VAR>h : ValidFor l r it<GOAL>(it.setCurr c).Valid
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>a : R<VAR>k : ℕ<GOAL>0 ≤ a ^ (k + k)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a✝ b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>a : R<VAR>k : ℕ<GOAL>0 ≤ a ^ k * a ^ k
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>m n : ℕ<GOAL>(fun z => z ^ m * cexp (↑b₁ * z)) =o[l] fun z => z ^ n * cexp (↑b₂ * z)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(ofZeros S hf hg).f' = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ 0<GOAL>(a - b) / c = a / c - b / c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : 0 < b → b < a → c ≠ 0<GOAL>(a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
<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>f : α → β<VAR>s : Set α<VAR>b : β<GOAL>b ∈ f '' s ↔ b ∈ ⋃ i ∈ s, {f i}
<VAR>f : Char → Char<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.modify { byteIdx := utf8Len cs } f = { data := cs ++ List.modifyHead f cs' }
<VAR>f : Char → Char<VAR>cs cs' : List Char<GOAL>{ data := cs ++ List.modifyHead (fun x => f (cs'.headD default)) cs' } = { data := cs ++ List.modifyHead f cs' }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<GOAL>(M.map f hf).Base (f '' B) ↔ M.Base B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<GOAL>(∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀) ↔ M.Base B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<VAR>x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀<VAR>J : Set α<VAR>hJ : M.Base J<VAR>hIJ : f '' B = f '' J<GOAL>M.Base B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<VAR>x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀<VAR>J : Set α<VAR>hJ : M.Base J<VAR>hIJ : B = J<GOAL>M.Base B
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y Z✝ X Z : C<GOAL>eqToHom ⋯ ▷ Z = eqToHom ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>inst✝ : AddGroup β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>f - g =ᶠ[l] 0
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y a b c d : E<GOAL>convexJoin 𝕜 (segment 𝕜 a b) (segment 𝕜 c d) = (convexHull 𝕜) {a, b, c, d}
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.57581, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.57588, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.57595, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.57647, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ℱ.obj X<GOAL>(ℱ.map f ≫ (fun X => appHom α (unop X)) Y) x = ((fun X => appHom α (unop X)) X ≫ ℱ'.val.map f) x
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.57581, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.57588, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.57595, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.57647, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ℱ.obj X<GOAL>∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ unop Y), ℱ'.val.map f_1.op ((ℱ.map f ≫ (fun X => appHom α (unop X)) Y) x) = ℱ'.val.map f_1.op (((fun X => appHom α (unop X)) X ≫ ℱ'.val.map f) x)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.57581, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.57588, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.57595, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.57647, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>ℱ : Dᵒᵖ ⥤ Type v<VAR>ℱ' : SheafOfTypes K<VAR>α✝ α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ℱ.obj X<VAR>Y' : C<VAR>f' : G.obj Y' ⟶ unop Y<GOAL>ℱ'.val.map f'.op ((ℱ.map f ≫ (fun X => appHom α (unop X)) Y) x) = ℱ'.val.map f'.op (((fun X => appHom α (unop X)) X ≫ ℱ'.val.map f) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 (μ {b}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<GOAL>∀ s ∈ 𝓝 (μ {b}), μ (Icc (b - 0) (b + 0)) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure ℝ<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>b : ℝ<VAR>s : Set ℝ≥0∞<VAR>hs : s ∈ 𝓝 (μ {b})<GOAL>μ (Icc (b - 0) (b + 0)) ∈ s
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<GOAL>(map ι f) x = x
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>f : M ≃ₗ[R] M<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<GOAL>(map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>f : M ≃ₗ[R] M<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<GOAL>rayOfNeZero R (g.compLinearMap ↑f.symm) ⋯ = rayOfNeZero R g hg
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>f : M ≃ₗ[R] M<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<VAR>i : ι → M<GOAL>(g.compLinearMap ↑f.symm) i = g i
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>f : M ≃ₗ[R] M<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<VAR>i : ι → M<GOAL>(g fun i_1 => ↑f.symm (i i_1)) = g i
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : IsEmpty ι<VAR>f : M ≃ₗ[R] M<VAR>g : M [⋀^ι]→ₗ[R] R<VAR>hg : g ≠ 0<VAR>i : ι → M<GOAL>(fun i_1 => ↑f.symm (i i_1)) = i
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>c : F<VAR>x : E<GOAL>iteratedFDeriv 𝕜 (n + 1) (fun x => c) x = 0 x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<GOAL>((toEnd R L M) f ^ (n + 1)) m = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h✝ e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h✝ e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<VAR>h : ¬((toEnd R L M) f ^ (n + 1)) m = 0<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h✝ e f : L<VAR>m : M<VAR>μ : R<VAR>t : IsSl2Triple h✝ e f<VAR>P : t.HasPrimitiveVectorWith m μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<VAR>h : ¬((toEnd R L M) f ^ (n + 1)) m = 0<VAR>this : t.HasPrimitiveVectorWith (((toEnd R L M) f ^ (n + 1)) m) (↑n - 2 * (↑n + 1))<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h✝ e f : L<VAR>m✝ : M<VAR>μ : R<VAR>t : IsSl2Triple h✝ e f<VAR>P : t.HasPrimitiveVectorWith m✝ μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<VAR>h : ¬((toEnd R L M) f ^ (n + 1)) m✝ = 0<VAR>this : t.HasPrimitiveVectorWith (((toEnd R L M) f ^ (n + 1)) m✝) (↑n - 2 * (↑n + 1))<VAR>m : ℕ<VAR>hm : ↑n - 2 * (↑n + 1) = ↑m<GOAL>False
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>h✝ e f : L<VAR>m✝ : M<VAR>μ : R<VAR>t : IsSl2Triple h✝ e f<VAR>P : t.HasPrimitiveVectorWith m✝ μ<VAR>inst✝³ : IsNoetherian R M<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>hn : μ = ↑n<VAR>h : ¬((toEnd R L M) f ^ (n + 1)) m✝ = 0<VAR>this✝ : t.HasPrimitiveVectorWith (((toEnd R L M) f ^ (n + 1)) m✝) (↑n - 2 * (↑n + 1))<VAR>m : ℕ<VAR>hm : ↑n - 2 * (↑n + 1) = ↑m<VAR>this : ↑n < ↑m + 2 * (↑n + 1)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsScott β<VAR>f : α → β<VAR>hf : Continuous f<VAR>x✝ b : α<VAR>hab : x✝ ≤ b<GOAL>f x✝ ≤ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : IsScott α<VAR>s : Set α<VAR>a : α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : IsScott β<VAR>f : α → β<VAR>hf : Continuous f<VAR>x✝ b : α<VAR>hab : x✝ ≤ b<VAR>h : ¬f x✝ ≤ f b<GOAL>False
<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>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>g : G →L[𝕜] E<GOAL>IsBoundedLinearMap 𝕜 fun f => f.compContinuousLinearMap fun x => g
<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>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>g : G →L[𝕜] E<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => E) F<GOAL>‖f.compContinuousLinearMap fun x => g‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖
<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>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>g : G →L[𝕜] E<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => E) F<GOAL>0 ≤ ‖g‖ ^ Fintype.card ι * ‖f‖
<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>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>g : G →L[𝕜] E<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => E) F<GOAL>∀ (m : ι → G), ‖(f.compContinuousLinearMap fun x => g) m‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i : ι, ‖m i‖
<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>ι : Type u_5<VAR>inst✝ : Fintype ι<VAR>g : G →L[𝕜] E<VAR>f : ContinuousMultilinearMap 𝕜 (fun x => E) F<VAR>m : ι → G<GOAL>‖(f.compContinuousLinearMap fun x => g) m‖ ≤ ‖g‖ ^ Fintype.card ι * ‖f‖ * ∏ i : ι, ‖m i‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 5 → β<GOAL>∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 5 → β<GOAL>f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4