ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>g : (i : Set β) → i ∈ l → β<VAR>hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i<VAR>hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)<GOAL>∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>g : (i : Set β) → i ∈ l → β<VAR>hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i<VAR>hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)<VAR>i : ↑{i | q i}<GOAL>x ∈ u ((fun i => g (b ↑i) ⋯) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>g : (i : Set β) → i ∈ l → β<VAR>hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i<VAR>hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)<VAR>i : ↑{i | q i}<GOAL>p ((fun i => g (b ↑i) ⋯) i) ∧ (fun i => g (b ↑i) ⋯) i ∈ b ↑i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>[a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b].TFAE
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<GOAL>[toIcoMod hp a b = a, ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b].TFAE
<VAR>α : Type u<VAR>inst✝ : Semiring α<VAR>x : α<VAR>n i : ℕ<VAR>x✝ : i ∈ range n<GOAL>x ^ i * 1 ^ (n - 1 - i) = x ^ i
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑m + ↑n < ℵ₀
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑(m + n) < ℵ₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∃ u, IsOpen u ∧ k ⊆ u ∧ IntegrableOn f u μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∃ u, IsOpen u ∧ ∅ ⊆ u ∧ IntegrableOn f u μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∀ ⦃s t : Set X⦄, s ⊆ t → (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∀ ⦃s t : Set X⦄, (∃ u, IsOpen u ∧ s ⊆ u ∧ IntegrableOn f u μ) → (∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>k : Set X<VAR>hk : IsCompact k<GOAL>∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen u ∧ t ⊆ u ∧ IntegrableOn f u μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<GOAL>IsClosed {x | 0 ≤ x}
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>this : {x | 0 ≤ x} = negPart ⁻¹' {0}<GOAL>IsClosed {x | 0 ≤ x}
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>this : {x | 0 ≤ x} = negPart ⁻¹' {0}<GOAL>IsClosed (negPart ⁻¹' {0})
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a✝ : A<VAR>f✝ : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h✝ : SpectrumRestricts a✝ f✝<VAR>a b : A<VAR>f : S → R<VAR>ha : SpectrumRestricts a f<VAR>h : spectrum S a = spectrum S b<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S b)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹¹ : CommSemiring R✝<VAR>inst✝¹⁰ : NonUnitalRing A✝<VAR>inst✝⁹ : Module R✝ A✝<VAR>inst✝⁸ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁷ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Semifield R<VAR>inst✝⁵ : Semifield S<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra S A<VAR>a✝ : A<VAR>f✝ : S → R<VAR>inst✝ : IsScalarTower R S A<VAR>h✝ : SpectrumRestricts a✝ f✝<VAR>a b : A<VAR>f : S → R<VAR>ha : SpectrumRestricts a f<VAR>h : spectrum S a = spectrum S b<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : NonAssocRing R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<VAR>h_pos : 0 < k<GOAL>choose 0 k = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁶ : Fintype K<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Fintype σ<VAR>inst✝³ : DecidableEq σ<VAR>inst✝² : DecidableEq K<VAR>p : ℕ<VAR>inst✝¹ : CharP K p<VAR>inst✝ : Fintype ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i : ι, (f i).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // ∀ (i : ι), (eval x) (f i) = 0 }
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>d d' : G.Dart<GOAL>d' ∈ filter (fun d' => d'.edge = d.edge) univ ↔ d' ∈ {d, d.symm}
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝³ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<VAR>inst✝² : HasCokernel f<VAR>inst✝¹ : HasCokernel (G.map f)<VAR>inst✝ : PreservesColimit (parallelPair f 0) G<GOAL>(iso G f).inv = cokernelComparison f G
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝³ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>w : f ≫ h = 0<VAR>inst✝² : HasCokernel f<VAR>inst✝¹ : HasCokernel (G.map f)<VAR>inst✝ : PreservesColimit (parallelPair f 0) G<GOAL>cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>inst✝¹⁰ : Zero α<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>inst✝⁴ : OpensMeasurableSpace Y<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetrizableSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<GOAL>Measurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>inst✝¹⁰ : Zero α<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>inst✝⁴ : OpensMeasurableSpace Y<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetrizableSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>Measurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>inst✝¹⁰ : Zero α<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>inst✝⁴ : OpensMeasurableSpace Y<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetrizableSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this✝ : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>this : ∀ (n : ℕ), ∃ g, ∀ (x : X × Y), dist (f x) (↑g x) < u n<GOAL>Measurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>inst✝¹⁰ : Zero α<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>inst✝⁴ : OpensMeasurableSpace Y<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetrizableSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>g : ℕ → SimpleFunc (X × Y) α<VAR>hg : ∀ (n : ℕ) (x : X × Y), dist (f x) (↑(g n) x) < u n<GOAL>Measurable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>α : Type u_9<VAR>inst✝¹⁰ : Zero α<VAR>inst✝⁹ : TopologicalSpace X<VAR>inst✝⁸ : TopologicalSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : OpensMeasurableSpace X<VAR>inst✝⁴ : OpensMeasurableSpace Y<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetrizableSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), 0 < u n<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>g : ℕ → SimpleFunc (X × Y) α<VAR>hg : ∀ (n : ℕ) (x : X × Y), dist (f x) (↑(g n) x) < u n<VAR>A : ∀ (x : X × Y), Tendsto (fun n => ↑(g n) x) atTop (𝓝 (f x))<GOAL>Measurable f
<VAR>q : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
<VAR>a b c d m n k✝ : ℕ<VAR>p q : ℕ → Prop<VAR>k x y : ℕ<VAR>h : x ≤ y / k<GOAL>x * k ≤ y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀✝ : ∀ (b : β), Monotone (swap f b)<VAR>h₁✝ : ∀ (a : α), Monotone (f a)<VAR>h₀ : ∀ (b : β), Monotone (swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>b : β<VAR>hb : b ∈ lowerBounds t<GOAL>BddBelow (image2 f s t)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>(SimpleGraph.induce H.verts G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>(⊤.induce H.verts).Connected
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<GOAL>(∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ) → g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<GOAL>g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h_avg : a • ⨍ (x : α) in t, (f x, (g ∘ f) x) ∂μ + b • ⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ = ⨍ (x : α), (f x, (g ∘ f) x) ∂μ<GOAL>g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h_avg : a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧ a • ⨍ (x : α) in t, (g ∘ f) x ∂μ + b • ⨍ (x : α) in tᶜ, (g ∘ f) x ∂μ = ⨍ (x : α), (g ∘ f) x ∂μ<GOAL>g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h_avg : a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧ a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ<GOAL>g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t✝ : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConvexOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<VAR>this : ∀ {t : Set α}, μ t ≠ 0 → ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ<VAR>t : Set α<VAR>hm : MeasurableSet t<VAR>h₀ : μ t ≠ 0<VAR>h₀' : μ tᶜ ≠ 0<VAR>hne : ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h_avg : a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ = ⨍ (x : α), f x ∂μ ∧ a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ = ⨍ (x : α), g (f x) ∂μ<GOAL>g (a • ⨍ (x : α) in t, f x ∂μ + b • ⨍ (x : α) in tᶜ, f x ∂μ) < a • ⨍ (x : α) in t, g (f x) ∂μ + b • ⨍ (x : α) in tᶜ, g (f x) ∂μ
<VAR>x y : EReal<GOAL>(x * y).toReal = x.toReal * y.toReal
<VAR>p : Nat.Primes<GOAL>(↑p).factorMultiset = PrimeMultiset.ofPrime p
<VAR>p : Nat.Primes<GOAL>factorMultisetEquiv.symm (↑p).factorMultiset = factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
<VAR>p : Nat.Primes<GOAL>(↑p).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(((((kernel.lift (cokernel.π g.unop) (cokernel.π (cokernel.π g.unop).op).unop ⋯ ≫ (Abelian.imageIsoImage g.unop).hom) ≫ image.ι g.unop).op ≫ (cokernelIsoOfEq ⋯).hom) ≫ cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯) (cokernel.π (kernel.ι g ≫ eqToHom ⋯)) ⋯) ≫ cokernel.desc (kernel.ι g ≫ eqToHom ⋯) (inv (eqToHom ⋯) ≫ cokernel.π (kernel.ι g)) ⋯) ≫ cokernel.desc (kernel.ι g) (factorThruImage g) ⋯ = factorThruImage g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>inv (eqToHom ⋯) ≫ factorThruImage g = factorThruImage g
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>descPochhammer R (n + 1) = descPochhammer R n * (X - ↑n)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>n : ℕ<GOAL>descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - ↑n)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a✝ : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hs : ThreeGPFree s<VAR>a : β<VAR>hfa : a ∈ t<VAR>b : β<VAR>hfb : b ∈ t<VAR>c : β<VAR>hfc : c ∈ t<VAR>habc : a * c = b * b<GOAL>a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a✝ : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hs : ThreeGPFree s<VAR>b : β<VAR>hfb : b ∈ t<VAR>c : β<VAR>hfc : c ∈ t<VAR>a : α<VAR>ha : a ∈ s<VAR>hfa : f a ∈ t<VAR>habc : f a * c = b * b<GOAL>f a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a✝ : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hs : ThreeGPFree s<VAR>c : β<VAR>hfc : c ∈ t<VAR>a : α<VAR>ha : a ∈ s<VAR>hfa : f a ∈ t<VAR>b : α<VAR>hb : b ∈ s<VAR>hfb : f b ∈ t<VAR>habc : f a * c = f b * f b<GOAL>f a = f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s A : Set α<VAR>t B : Set β<VAR>f : α → β<VAR>a✝ : α<VAR>hf : IsMulFreimanIso 2 s t f<VAR>hs : ThreeGPFree s<VAR>a : α<VAR>ha : a ∈ s<VAR>hfa : f a ∈ t<VAR>b : α<VAR>hb : b ∈ s<VAR>hfb : f b ∈ t<VAR>c : α<VAR>hc : c ∈ s<VAR>hfc : f c ∈ t<VAR>habc : f a * f c = f b * f b<GOAL>f a = f b
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hab : a ∣ b<VAR>h : b / a = 0<GOAL>b = 0
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : MvPolynomial σ R<GOAL>(-p).degrees = p.degrees