ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<VAR>N : ℕ<VAR>hN : N ≤ n<VAR>x : E<GOAL>‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<VAR>N : ℕ<VAR>hN : N ∈ Finset.range n.succ<VAR>x : E<GOAL>‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<VAR>N : ℕ<VAR>hN : N ∈ Finset.range n.succ<VAR>x : E<GOAL>C N ≤ C'
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<VAR>N : ℕ<VAR>hN : N ∈ Finset.range n.succ<VAR>x : E<GOAL>(1 + ‖x‖) ^ k N ≤ (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f✝ : E → F<VAR>hf_temperate : Function.HasTemperateGrowth f✝<VAR>n : ℕ<VAR>k : ℕ → ℕ<VAR>C : ℕ → ℝ<VAR>f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n<VAR>C' : ℝ := max 0 ((Finset.range (n + 1)).sup' ⋯ C)<VAR>hC' : 0 ≤ C'<VAR>N : ℕ<VAR>hN : N ∈ Finset.range n.succ<VAR>x : E<GOAL>k N ≤ (Finset.range (n + 1)).sup k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>l : Filter α<VAR>f g : α → ℝ≥0∞<VAR>hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤<VAR>hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤<VAR>hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal<GOAL>f =ᶠ[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>l : Filter α<VAR>f g : α → ℝ≥0∞<VAR>hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤<VAR>hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤<VAR>hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal<VAR>a✝¹ : α<VAR>hfx : f a✝¹ ≠ ⊤<VAR>hgx : g a✝¹ ≠ ⊤<VAR>a✝ : (f a✝¹).toReal = (g a✝¹).toReal<GOAL>f a✝¹ = g a✝¹
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>g : L →+* M<VAR>f : K →+* L<GOAL>Subfield.map g f.fieldRange = (g.comp f).fieldRange
<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 : ι → Set α<GOAL>(⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>Comp.mk (tsnd f' <$> tfst f x) = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ map f' ∘ pure) x = bitraverse (Comp.mk ∘ map pure ∘ f) (Comp.mk ∘ pure ∘ f') x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Fintype α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.length ≤ Fintype.card α
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<GOAL>MeasurableSpace.pi ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<GOAL>∀ (i : ι), MeasurableSpace.comap (fun b => b i) (inst✝ i) ≤ (OuterMeasure.pi fun i => (μ i).toOuterMeasure).caratheodory
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ((fun b => b i) ⁻¹' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set ((a : ι) → α a)), piPremeasure (fun i => (μ i).toOuterMeasure) (t ∩ (fun b => b i) ⁻¹' s) + piPremeasure (fun i => (μ i).toOuterMeasure) (t \ (fun b => b i) ⁻¹' s) ≤ piPremeasure (fun i => (μ i).toOuterMeasure) t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<VAR>t : Set ((a : ι) → α a)<GOAL>∏ x : ι, (μ x).toOuterMeasure (eval x '' (t ∩ (fun b => b i) ⁻¹' s)) + ∏ x : ι, (μ x).toOuterMeasure (eval x '' (t \ (fun b => b i) ⁻¹' s)) ≤ ∏ x : ι, (μ x).toOuterMeasure (eval x '' t)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<VAR>t : Set ((a : ι) → α a)<GOAL>(μ i).toOuterMeasure (eval i '' (t ∩ (fun b => b i) ⁻¹' s)) + (μ i).toOuterMeasure (eval i '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ i).toOuterMeasure (eval i '' t)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<VAR>t : Set ((a : ι) → α a)<GOAL>∀ j ∈ Finset.univ, j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : MeasurableSet s<VAR>t : Set ((a : ι) → α a)<GOAL>∀ j ∈ Finset.univ, j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b => b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{v}<GOAL>lift.{u, v} a = lift.{u, v} b ↔ a = b
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>μ : Measure α<GOAL>Measure.map Subtype.val (Measure.comap Subtype.val μ) = μ.restrict s
<VAR>c : Char<VAR>cs : List Char<VAR>b e : Pos<GOAL>go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e
<VAR>c : Char<VAR>cs : List Char<VAR>b e : Pos<GOAL>go₁ cs (0 + c) (b + c) (e + c) = go₁ cs 0 b e
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f✝ : X ⟶ Y<VAR>f g : Arrow C<VAR>F : MonoFactorisation f.hom<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<GOAL>(inv sq.left ≫ F.e) ≫ F.m ≫ sq.right = g.hom
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<GOAL>{q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite<GOAL>False
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite<VAR>q : ℚ<VAR>left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}<VAR>hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|<GOAL>False
<VAR>ξ : ℝ<VAR>hξ : Irrational ξ<VAR>h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite<VAR>q : ℚ<VAR>left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}<VAR>hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|<VAR>q' : ℚ<VAR>hmem : |ξ - ↑q'| < 1 / ↑q'.den ^ 2<VAR>hbetter : |ξ - ↑q'| < |ξ - ↑q|<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_nonempty : ∀ (i : ι), (s i).Nonempty<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<GOAL>Subsingleton ι
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<GOAL>¬Nontrivial ι
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<VAR>i j : ι<VAR>h_ne : i ≠ j<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<VAR>i j : ι<VAR>h_ne : s i ∩ s j = ∅<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<VAR>i j : ι<VAR>h_ne : s i ∩ s j = ∅<VAR>hi : s i = ∅<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>s : ι → Set α<VAR>h_disj : Pairwise (Disjoint on s)<VAR>h_clopen : ∀ (i : ι), IsClopen (s i)<VAR>h_nonempty : ∀ (i : ι), s i ≠ ∅<VAR>i j : ι<VAR>h_ne : s i ∩ s j = ∅<VAR>hi : s i = univ<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddCommGroup α<VAR>h : Periodic f c<GOAL>f (c - x) = f (-x)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : v + ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hv : 0 ≤ v<VAR>hq : q ∈ s<VAR>W : Option ι → 𝕜 := fun j => j.elim v w<VAR>P : Option ι → E := fun j => j.elim q p<GOAL>f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : v + ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hv : 0 ≤ v<VAR>hq : q ∈ s<VAR>W : Option ι → 𝕜 := fun j => j.elim v w<VAR>P : Option ι → E := fun j => j.elim q p<VAR>this : f (∑ j ∈ insertNone t, W j • P j) ≤ ∑ j ∈ insertNone t, W j • f (P j)<GOAL>f (v • q + ∑ i ∈ t, w i • p i) ≤ v • f q + ∑ i ∈ t, w i • f (p i)
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>h : c.IsLimit<GOAL>ℵ₀ ≤ c
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<VAR>h : c.IsLimit<VAR>h' : c < ℵ₀<GOAL>False
<VAR>α β : Type u<VAR>n : ℕ<VAR>h : (↑n).IsLimit<VAR>h' : ↑n < ℵ₀<GOAL>False
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<GOAL>Function.Injective (F.stalkToFiber x)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<GOAL>∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → F.stalk ↑y), (Sheafify.isLocallyGerm F).pred fU → ∀ (fV : (y : ↥V.obj) → F.stalk ↑y), (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_4 => ⟨↑x_4, ⋯⟩) w) = fV ((fun x_4 => ⟨↑x_4, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<GOAL>∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<VAR>U' : Opens ↑X<VAR>mU : ↑⟨x, ⋯⟩ ∈ U'<VAR>iU : U' ⟶ U.obj<VAR>gU : F.obj (op U')<VAR>wU : ∀ (x_1 : ↥U'), (fun x_2 => fU ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gU<GOAL>∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>e : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩<VAR>U' : Opens ↑X<VAR>mU : ↑⟨x, ⋯⟩ ∈ U'<VAR>iU : U' ⟶ U.obj<VAR>gU : F.obj (op U')<VAR>wU : ∀ (x_1 : ↥U'), (fun x_2 => fU ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gU<VAR>V' : Opens ↑X<VAR>mV : ↑⟨x, ⋯⟩ ∈ V'<VAR>iV : V' ⟶ V.obj<VAR>gV : F.obj (op V')<VAR>wV : ∀ (x_1 : ↥V'), (fun x_2 => fV ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gV<GOAL>∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>U' : Opens ↑X<VAR>mU : ↑⟨x, ⋯⟩ ∈ U'<VAR>iU : U' ⟶ U.obj<VAR>gU : F.obj (op U')<VAR>wU : ∀ (x_1 : ↥U'), (fun x_2 => fU ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gU<VAR>V' : Opens ↑X<VAR>mV : ↑⟨x, ⋯⟩ ∈ V'<VAR>iV : V' ⟶ V.obj<VAR>gV : F.obj (op V')<VAR>e : F.germ ⟨x, mU⟩ gU = F.germ ⟨x, mV⟩ gV<VAR>wV : ∀ (x_1 : ↥V'), (fun x_2 => fV ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gV<GOAL>∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>U' : Opens ↑X<VAR>mU : ↑⟨x, ⋯⟩ ∈ U'<VAR>iU : U' ⟶ U.obj<VAR>gU : F.obj (op U')<VAR>wU : ∀ (x_1 : ↥U'), (fun x_2 => fU ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gU<VAR>V' : Opens ↑X<VAR>mV : ↑⟨x, ⋯⟩ ∈ V'<VAR>iV : V' ⟶ V.obj<VAR>gV : F.obj (op V')<VAR>e : F.germ ⟨x, mU⟩ gU = F.germ ⟨x, mV⟩ gV<VAR>wV : ∀ (x_1 : ↥V'), (fun x_2 => fV ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gV<VAR>W : Opens ↑X<VAR>mW : x ∈ W<VAR>iU' : W ⟶ U'<VAR>iV' : W ⟶ V'<VAR>e' : F.map iU'.op gU = F.map iV'.op gV<GOAL>∃ W iU iV, ∀ (w : ↥W.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>X : TopCat<VAR>F : Presheaf (Type v) X<VAR>x : ↑X<VAR>U V : OpenNhds x<VAR>fU : (y : ↥U.obj) → F.stalk ↑y<VAR>hU : (Sheafify.isLocallyGerm F).pred fU<VAR>fV : (y : ↥V.obj) → F.stalk ↑y<VAR>hV : (Sheafify.isLocallyGerm F).pred fV<VAR>U' : Opens ↑X<VAR>mU : ↑⟨x, ⋯⟩ ∈ U'<VAR>iU : U' ⟶ U.obj<VAR>gU : F.obj (op U')<VAR>wU : ∀ (x_1 : ↥U'), (fun x_2 => fU ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gU<VAR>V' : Opens ↑X<VAR>mV : ↑⟨x, ⋯⟩ ∈ V'<VAR>iV : V' ⟶ V.obj<VAR>gV : F.obj (op V')<VAR>e : F.germ ⟨x, mU⟩ gU = F.germ ⟨x, mV⟩ gV<VAR>wV : ∀ (x_1 : ↥V'), (fun x_2 => fV ((fun x_3 => ⟨↑x_3, ⋯⟩) x_2)) x_1 = F.germ x_1 gV<VAR>W : Opens ↑X<VAR>mW : x ∈ W<VAR>iU' : W ⟶ U'<VAR>iV' : W ⟶ V'<VAR>e' : F.map iU'.op gU = F.map iV'.op gV<GOAL>∃ iU iV, ∀ (w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj), fU ((fun x_1 => ⟨↑x_1, ⋯⟩) w) = fV ((fun x_1 => ⟨↑x_1, ⋯⟩) w)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>f✝ : α → ℝ<VAR>s✝ : Set α<VAR>x : α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<GOAL>∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (1 + n) = a * a ^ n
<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.RightHomologyData<VAR>inst✝ : S.HasRightHomology<GOAL>S.pOpcycles ≫ h.opcyclesIso.hom = h.p
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>h : Commute f g<VAR>μ : R<GOAL>MapsTo ⇑g ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>h : Commute f g<VAR>μ : R<GOAL>∀ ⦃x : M⦄, (∃ i, x ∈ (f.genEigenspace μ) i) → ∃ i, g x ∈ (f.genEigenspace μ) i
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>h : Commute f g<VAR>μ : R<VAR>x : M<VAR>k : ℕ<VAR>hk : x ∈ (f.genEigenspace μ) k<GOAL>∃ i, g x ∈ (f.genEigenspace μ) i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : LeftOrdContinuous g<VAR>hf : LeftOrdContinuous f<VAR>s : Set α<VAR>x : α<VAR>h : IsLUB s x<GOAL>IsLUB (g ∘ f '' s) ((g ∘ f) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>l₁ l₂ : (i : ι) → G i<VAR>s : Finset ι<GOAL>⟪∑ i ∈ s, (V i) (l₁ i), ∑ j ∈ s, (V j) (l₂ j)⟫_𝕜 = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>MeasurableSet {a | p a ↔ q a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>p q : α → Prop<VAR>hp : Measurable p<VAR>hq : Measurable q<GOAL>MeasurableSet {a | (p a → q a) ∧ (q a → p a)}
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>h : StarConvex ℝ x s<VAR>hne : s.Nonempty<GOAL>ContractibleSpace ↑s
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>h : StarConvex ℝ x s<VAR>hne : s.Nonempty<VAR>p : ↑unitInterval × ↑s<GOAL>↑p.1 • x + (1 - ↑p.1) • ↑p.2 ∈ s
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>h : StarConvex ℝ x s<VAR>hne : s.Nonempty<GOAL>Continuous fun p => ⟨↑p.1 • x + (1 - ↑p.1) • ↑p.2, ⋯⟩
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x✝ : E<VAR>h : StarConvex ℝ x✝ s<VAR>hne : s.Nonempty<VAR>x : ↑s<GOAL>{ toFun := fun p => ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?refine_2 }.toFun (0, x) = (ContinuousMap.id ↑s) x
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x✝ : E<VAR>h : StarConvex ℝ x✝ s<VAR>hne : s.Nonempty<VAR>x : ↑s<GOAL>{ toFun := fun p => ⟨↑p.1 • x✝ + (1 - ↑p.1) • ↑p.2, ⋯⟩, continuous_toFun := ?refine_2 }.toFun (1, x) = (ContinuousMap.const ↑s ⟨x✝, ⋯⟩) x
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) =ᶠ[ae (μ.trim hm)] ↑↑(lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g)