ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>hf : LeftInvOn f' f s<GOAL>f' '' (f '' s) = s
<GOAL>Order.succ ℵ₀ ≤ 𝔠
<VAR>z : ℂ<GOAL>|z.re| < abs z ↔ z.im ≠ 0
<VAR>b : Ordinal.{u_1}<VAR>h : ¬1 < b<VAR>x : Ordinal.{u_1}<GOAL>log b x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>H : p = 0<GOAL>(derivative p).degree = p.degree
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ : List α<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ : List α<VAR>ab : r a b<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>Lex r (a :: l₁) (a :: l₂) ∨ a :: l₁ = a :: l₂ ∨ Lex r (a :: l₂) (a :: l₁)
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsTrichotomous α r<VAR>a : α<VAR>l₁ : List α<VAR>b : α<VAR>l₂ : List α<VAR>ab : r b a<GOAL>Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>M✝ L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>inst✝¹ : HasImage f<VAR>g : underlying.obj (imageSubobject f) ⟶ N<VAR>inst✝ : HasCokernel g<VAR>y : ↑N<VAR>l : ↑L<GOAL>(cokernel.π g) (y + g ((factorThruImageSubobject f) l)) = (cokernel.π g) y
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>M✝ L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>inst✝¹ : HasImage f<VAR>g : underlying.obj (imageSubobject f) ⟶ N<VAR>inst✝ : HasCokernel g<VAR>y : ↑N<VAR>l : ↑L<GOAL>(cokernel.π g) (g ((factorThruImageSubobject f) l)) = 0
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>M✝ L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>inst✝¹ : HasImage f<VAR>g : underlying.obj (imageSubobject f) ⟶ N<VAR>inst✝ : HasCokernel g<VAR>y : ↑N<VAR>l : ↑L<GOAL>(⇑(cokernel.π g) ∘ ⇑g ∘ ⇑(factorThruImageSubobject f)) l = 0
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>M✝ L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>inst✝¹ : HasImage f<VAR>g : underlying.obj (imageSubobject f) ⟶ N<VAR>inst✝ : HasCokernel g<VAR>y : ↑N<VAR>l : ↑L<GOAL>(factorThruImageSubobject f ≫ g ≫ cokernel.π g) l = 0
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>M✝ L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>inst✝¹ : HasImage f<VAR>g : underlying.obj (imageSubobject f) ⟶ N<VAR>inst✝ : HasCokernel g<VAR>y : ↑N<VAR>l : ↑L<GOAL>0 l = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup N'<VAR>inst✝¹ : Module R N'<VAR>S : Submonoid R<VAR>f : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] N'<VAR>σ : Finset M<VAR>hσ : Submodule.span R ↑σ = ⊤<VAR>τ : Finset ({ x // x ∈ σ } →₀ R)<VAR>hτ : Submodule.span R ↑τ = LinearMap.ker (Finsupp.total { x // x ∈ σ } M R Subtype.val)<VAR>π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ σ } M R Subtype.val<GOAL>∃ h s, f ∘ₗ h = s • g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommGroup N'<VAR>inst✝¹ : Module R N'<VAR>S : Submonoid R<VAR>f : N →ₗ[R] N'<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] N'<VAR>σ : Finset M<VAR>hσ : Submodule.span R ↑σ = ⊤<VAR>τ : Finset ({ x // x ∈ σ } →₀ R)<VAR>hτ : Submodule.span R ↑τ = LinearMap.ker (Finsupp.total { x // x ∈ σ } M R Subtype.val)<VAR>π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ σ } M R Subtype.val<VAR>hπ : Function.Surjective ⇑π<GOAL>∃ h s, f ∘ₗ h = s • g
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>W'.Equation ![1, 1, 0]
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝⁷ : Group Γ<VAR>T : Type u_5<VAR>inst✝⁶ : TopologicalSpace T<VAR>inst✝⁵ : MulAction Γ T<VAR>G₀ : Type u_6<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : AddMonoid α<VAR>inst✝² : DistribMulAction G₀ α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : ContinuousConstSMul G₀ α<VAR>s : Set α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Γ : Type u_4<VAR>inst✝⁷ : Group Γ<VAR>T : Type u_5<VAR>inst✝⁶ : TopologicalSpace T<VAR>inst✝⁵ : MulAction Γ T<VAR>G₀ : Type u_6<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : AddMonoid α<VAR>inst✝² : DistribMulAction G₀ α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : ContinuousConstSMul G₀ α<VAR>s : Set α<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 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>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : LinearWeights R L M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>χ : Weight R L M<VAR>h : χ.IsZero<VAR>x✝ : L<GOAL>(toLinear R L M χ) x✝ = 0 x✝
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t : Set A<VAR>f : A →ₐ[R] B<VAR>s : Set A<GOAL>(fun x => x) '' s ⊆ (Subalgebra.comap f (adjoin R (⇑f '' s))).carrier
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t : Set A<VAR>f : A →ₐ[R] B<VAR>s : Set A<GOAL>s ⊆ ⇑f ⁻¹' ↑(adjoin R (⇑f '' s))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>a : α<VAR>f : α → β<GOAL>{a}.Pairwise fun a b => Commute (f a) (f b)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<GOAL>(-A).det = (-1) ^ Fintype.card n • A.det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<GOAL>a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z✝ : C<VAR>f : Y ⟶ X<VAR>inst✝ : HasPullbacks C<VAR>ι : Type u_1<VAR>Z : ι → C<VAR>g : (i : ι) → Z i ⟶ X<GOAL>(ofArrows (fun i => pullback (g i) f) fun i => pullback.snd (g i) f) = pullbackArrows f (ofArrows Z g)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z✝ : C<VAR>f : Y ⟶ X<VAR>inst✝ : HasPullbacks C<VAR>ι : Type u_1<VAR>Z : ι → C<VAR>g : (i : ι) → Z i ⟶ X<VAR>T : C<GOAL>(ofArrows (fun i => pullback (g i) f) fun i => pullback.snd (g i) f) = pullbackArrows f (ofArrows Z g)
<VAR>b x✝ y x : ℝ<GOAL>logb b x⁻¹ = -logb b x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : t ∈ 𝓝[s] a<GOAL>𝓝[s ∩ t] a = 𝓝[s] a
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>n : ℕ<GOAL>(↑n).card = ↑n
<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>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ↥(Lp F p μ)<GOAL>f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable' m (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<GOAL>a + b - (a + c) = b - c
<VAR>u : Level<VAR>e' r : ℤ<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n n' : ℕ<VAR>inst : CharP α n<VAR>e : α<VAR>he : IsInt e e'<VAR>hn : IsNat n n'<VAR>h₂ : IsInt (e' % ↑n') r<GOAL>e = ↑r
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.11729, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = x ≫ S.f<GOAL>k ≫ S.g = 0
<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>k : A ⟶ S.X₂<VAR>x : A ⟶ S.X₁<VAR>hx : k = x ≫ S.f<GOAL>h.liftK k ⋯ = x ≫ h.f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>a : α<GOAL>(∀ ⦃b : α⦄, b ≤ a → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, b < a → a ∈ s → b ∈ s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : Measurable g<GOAL>μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>x : ↑(fundamentalDomain b)<GOAL>(quotientEquiv b).symm x = Submodule.Quotient.mk ↑x
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>x : ↑(fundamentalDomain b)<GOAL>↑x = fract b ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>p.nextCoeff = p.coeff (p.natDegree - 1)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>¬p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.natDegree = 0<GOAL>p.natDegree ≤ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>ι : Type u_2<VAR>f : ι → Filter α<GOAL>(⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>ι : Type u_2<VAR>f : ι → Filter α<GOAL>Directed (fun x x_1 => x ≥ x_1) fun t => ⨅ i ∈ t, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>b : Ordinal.{u_4}<GOAL>0 % b = 0
<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>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<VAR>i : ι'<GOAL>(hv.equiv hv' e) ((hv.equiv hv' e).symm (v' i)) = (hv.equiv hv' e) ((hv'.equiv hv e.symm) (v' i))
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.any p = s.data.any p
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<GOAL>max ↑a ↑b = map₂ max ↑a ↑b
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<VAR>h : ↑a ≤ ↑b<GOAL>max ↑a ↑b = map₂ max ↑a ↑b
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Ultrafilter α<VAR>inst✝ : LinearOrder β<VAR>x y : (↑φ).Germ β<VAR>a b : α → β<VAR>h : ↑b ≤ ↑a<GOAL>max ↑a ↑b = map₂ max ↑a ↑b
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>α β : K<GOAL>house (α * β) ≤ house α * house β
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>α β : K<GOAL>‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<GOAL>ConcaveOn 𝕜 univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f.symm x + b • f.symm y ≤ f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<GOAL>a • f.symm x + b • f.symm y ≤ f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>a • f.symm x + b • f.symm y ≤ f.symm (a • x + b • y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>a • x' + b • y' ≤ f.symm (a • f x' + b • f y')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : ConvexOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>f (a • x' + b • y') ≤ a • f x' + b • f y'
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>x ∈ closure (Set.range Nat.cast)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>∀ ε > 0, ∃ k, dist x ↑k < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ k, dist x ↑k < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>∃ k, dist x ↑k < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>dist x ↑(x.appr n) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>‖x - ↑(x.appr n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>‖x - ↑(x.appr n)‖ ≤ ↑p ^ (-↑n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ Integrable (⇑g) μ
<VAR>α : Type u_1<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : NormalSpace α<VAR>inst✝⁵ : R1Space α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hf : Memℒp f 1 μ<GOAL>∃ g, eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ Memℒp (⇑g) 1 μ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<GOAL>map f (p * q) = map f p * map f q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<GOAL>∀ (k : ℕ), Commute ((C.comp f) (q.coeff k)) X
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>κ : Type u_6<VAR>inst✝ : Fintype κ<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<VAR>this : DecidableEq M<GOAL>((toMatrix b b) f).det = LinearMap.det f
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Module A M<VAR>κ : Type u_6<VAR>inst✝ : Fintype κ<VAR>b : Basis ι A M<VAR>f : M →ₗ[A] M<VAR>this : DecidableEq M<GOAL>((toMatrix b b) f).det = ((toMatrix b.reindexFinsetRange b.reindexFinsetRange) f).det
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>inst✝¹ : RingHomSurjective τ₂₃<VAR>inst✝ : RingHomSurjective τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>hf : range f = ⊤<GOAL>range (g.comp f) = range g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s✝ t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>ι : Sort u_3<VAR>s : ι → Set X<GOAL>𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|a| ≤ |b| + |b + a|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<GOAL>toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<GOAL>toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<VAR>h₃₂ : x₃' - p < x₂'<GOAL>toIcoMod hp x₂ x₃ ≤ toIocMod hp x₂ x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<VAR>h₃₂ : x₃' - p < x₂'<GOAL>x₃' ≤ toIocMod hp x₂' x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<VAR>h₃₂ : x₃' - p < x₂'<VAR>h₃₁ : x₃' ≤ x₁ + p<GOAL>x₃' ≤ toIocMod hp x₂' x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<VAR>h₃₂ : x₃' - p < x₂'<VAR>h₁₃ : x₁ + p < x₃'<GOAL>x₃' ≤ toIocMod hp x₂' x₁
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>x₁ x₂ x₃ : α<VAR>h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃<VAR>x₂' : α := toIcoMod hp x₁ x₂<VAR>x₃' : α := toIcoMod hp x₂' x₃<VAR>h : x₂' ≤ toIocMod hp x₁ x₃'<VAR>h₂₁ : x₂' < x₁ + p<VAR>h₃₂ : x₃' - p < x₂'<VAR>h₁₃ : x₁ + p < x₃'<VAR>hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p<GOAL>x₃' ≤ toIocMod hp x₂' x₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>range l.get? = insert none (some '' {x | x ∈ l})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>range l.get? = insert none (range (some ∘ l.get))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>n : ℕ<GOAL>l.get? n ∈ insert none (range (some ∘ l.get))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>none ∈ range l.get?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>range (some ∘ l.get) ⊆ range l.get?
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>P : Ideal R[X]<VAR>pX : R[X]<VAR>hpX : pX ∈ P<VAR>inst✝³ : Algebra (R ⧸ comap C P) Rₘ<VAR>inst✝² : IsLocalization.Away (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff Rₘ<VAR>inst✝¹ : Algebra (R[X] ⧸ P) Sₘ<VAR>inst✝ : IsLocalization (Submonoid.map (quotientMap P C ⋯) (Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff)) Sₘ<VAR>P' : Ideal R := comap C P<VAR>M : Submonoid (R ⧸ P') := Submonoid.powers (Polynomial.map (Quotient.mk (comap C P)) pX).leadingCoeff<GOAL>(IsLocalization.map Sₘ (quotientMap P C ⋯) ⋯).IsIntegral