ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y : D<VAR>j : CostructuredArrow L Y<GOAL>colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ colimit.desc (CostructuredArrow.proj L Y ⋙ F) { pt := colimit (CostructuredArrow.proj L Y ⋙ F), ι := { app := fun g => colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj g), naturality := ⋯ } } = colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y : D<VAR>j : CostructuredArrow L Y<GOAL>colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj j) = colimit.ι (CostructuredArrow.proj L Y ⋙ F) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y : D<VAR>j : CostructuredArrow L Y<GOAL>(CostructuredArrow.map (𝟙 Y)).obj j = j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : CostructuredArrow L Y₁<GOAL>colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫ colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F) { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F), ι := { app := fun g => colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g), naturality := ⋯ } } = colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫ colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F) { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F), ι := { app := fun g => colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g), naturality := ⋯ } } ≫ colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F) { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F), ι := { app := fun g => colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g), naturality := ⋯ } }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : CostructuredArrow L Y₁<GOAL>colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj j) = colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj ((CostructuredArrow.map f).obj j))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y₁ Y₂ Y₃ : D<VAR>f : Y₁ ⟶ Y₂<VAR>f' : Y₂ ⟶ Y₃<VAR>j : CostructuredArrow L Y₁<GOAL>(CostructuredArrow.map (f ≫ f')).obj j = (CostructuredArrow.map f').obj ((CostructuredArrow.map f).obj j)
<VAR>a✝ b c p q a : ℚ<GOAL>a.num ≤ 0 ↔ a ≤ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : SeminormedAddCommGroup F<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<VAR>x : E<GOAL>‖(f.prod g) x‖ ≤ ‖(f, g)‖ * ‖x‖
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<VAR>π₀ : Prepartition I<GOAL>(l.toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I✝ J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I✝<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>I : Box ι<VAR>π₀ : Prepartition I<VAR>this : ∀ (c : ℝ≥0), (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion}<GOAL>(l.toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion}
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hl₁ : l₁.Nodup<GOAL>a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂
<VAR>F✝¹ : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p : K[X]<VAR>F✝ : IntermediateField K L<VAR>x : L<VAR>int : IsIntegral K x<VAR>F : IntermediateField K L<VAR>h : Splits (algebraMap K ↥F) (minpoly K x)<GOAL>x ∈ F
<VAR>F✝¹ : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p : K[X]<VAR>F✝ : IntermediateField K L<VAR>x : L<VAR>int : IsIntegral K x<VAR>F : IntermediateField K L<VAR>h : Splits (algebraMap K ↥F) (minpoly K x)<GOAL>x ∈ F.val.fieldRange
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<GOAL>s.Disjoint (t ∪ u) ↔ s.Disjoint t ∧ s.Disjoint u
<VAR>x✝ y x : ℝ<VAR>hx : ¬x = 0<GOAL>log x⁻¹ = -log x
<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>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>s t : Set X<GOAL>IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t
<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>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>s t : Set X<GOAL>s ∩ closure (s ∩ t) ⊆ s
<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>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>p : X → Prop<VAR>s t : Set X<GOAL>s ∩ t ⊆ s ∩ closure (s ∩ t)
<VAR>R✝ : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Ring R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : Fintype R✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Finite R<GOAL>IsField R
<VAR>R✝ : Type u_1<VAR>G : Type u_2<VAR>inst✝⁵ : Ring R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : Fintype R✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : Finite R<VAR>val✝ : Fintype R<GOAL>IsField R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>p : Set β → Prop<GOAL>(∀ s ⊆ range f, p s) ↔ ∀ (s : Set α), p (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>p : Set β → Prop<GOAL>(∀ s ⊆ range f, p s) ↔ ∀ a ∈ 𝒫 range f, p a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>this : b ∈ closure (e '' {x | p x})<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>this : b ∈ closure (e '' {x | p x})<VAR>c : γ<VAR>hc : Tendsto (fun x => f ↑x) (comap (DenseEmbedding.subtypeEmb p e) (𝓝 ⟨b, this⟩)) (𝓝 c)<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>this : b ∈ closure (e '' {x | p x})<VAR>c : γ<VAR>hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)<GOAL>∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>this : b ∈ closure (e '' {x | p x})<VAR>c : γ<VAR>hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)<GOAL>range Subtype.val ∈ comap e (𝓝 b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>inst✝¹ : UniformSpace γ<VAR>e✝ : β → α<VAR>h_e : UniformInducing e✝<VAR>h_dense : DenseRange e✝<VAR>f✝ : β → γ<VAR>h_f : UniformContinuous f✝<VAR>inst✝ : CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<VAR>de : DenseEmbedding e<VAR>de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)<VAR>this : b ∈ closure (e '' {x | p x})<VAR>c : γ<VAR>hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)<GOAL>{x | p x} ∈ comap e (𝓝 b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<GOAL>σₙ R 0 = {0}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>x : R<VAR>hx : x ∈ σₙ R 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>x : R<VAR>hx : x ∈ 0 '' σₙ R 0<GOAL>x = 0
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hxz' : 0 < z - x<GOAL>(f y - f x) / (y - x) < (f z - f x) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hxz' : 0 < z - x<GOAL>(f y - f x) * (z - x) < (f z - f x) * (y - x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r✝ r' : ℝ≥0∞<VAR>s : Set E<VAR>g : F →L[𝕜] G<VAR>h : AnalyticOn 𝕜 f s<VAR>x : E<VAR>hx : x ∈ s<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>hp : HasFPowerSeriesOnBall f p x r<GOAL>AnalyticAt 𝕜 (⇑g ∘ f) x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>hd : finrank K V = d + 1<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>hd : finrank K V = d + 1<VAR>this : Nontrivial V<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>hd : finrank K V = d + 1<VAR>this : Nontrivial V<VAR>hB₂ : IsSymm 0<GOAL>∃ v, IsOrthoᵢ 0 ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>hd : finrank K V = d + 1<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>hd : finrank K V = d + 1<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hx : ¬IsOrtho B x x<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<GOAL>∃ v, IsOrthoᵢ B ⇑v
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>K : Type v<VAR>inst✝³ : Field K<VAR>hK : Invertible 2<VAR>d : ℕ<VAR>ih : ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V}, IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v<VAR>V : Type u<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB₂ : IsSymm B<VAR>this : Nontrivial V<VAR>hB₁ : B ≠ 0<VAR>x : V<VAR>hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1<VAR>hx : ¬IsOrtho B x x<VAR>B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K := domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)<VAR>v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)<VAR>hv₁ : (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'<GOAL>∃ v, IsOrthoᵢ B ⇑v