ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>H : IsNormal f<VAR>o : Ordinal.{u}<VAR>h : o.IsLimit<GOAL>(o.blsub fun x x_1 => f x) = f o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : Ordinal.{u} → Ordinal.{max u v}<VAR>H : IsNormal f<VAR>o : Ordinal.{u}<VAR>h : o.IsLimit<GOAL>∀ a < o, f a < f (succ a)
<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>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(natTransLift r (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫ isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫ (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫ isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫ (functor r).associator (lift r F hF) (shiftFunctor D a)).hom).app ((functor r).obj X) = (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X
<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>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫ isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫ (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫ isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫ F.commShiftIso a ≪≫ isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫ (functor r).associator (lift r F hF) (shiftFunctor D a)).hom.app X = (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X
<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>r : HomRel C<VAR>A : Type w<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift C A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : r.IsCompatibleWithShift A<VAR>inst✝ : F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>𝟙 ((lift r F hF).obj ((shiftFunctor (Quotient r) a).obj ((functor r).obj X))) ≫ (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ 𝟙 ((lift r F hF).obj ((functor r).obj ((shiftFunctor C a).obj X))) ≫ 𝟙 (F.obj ((shiftFunctor C a).obj X)) ≫ (F.commShiftIso a).hom.app X ≫ (shiftFunctor D a).map (𝟙 (F.obj X)) ≫ 𝟙 ((shiftFunctor D a).obj ((lift r F hF).obj ((functor r).obj X))) = (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : M<GOAL>x ∈ span R (Set.range v) ↔ ∃ c, ∑ i : α, c i • v i = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : M<GOAL>x ∈ span R (Set.range v) ↔ ∃ x_1, ∑ i : α, Finsupp.equivFunOnFinite x_1 i • v i = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : M<GOAL>(∃ c, (c.sum fun i a => a • v i) = x) ↔ ∃ x_1, ∑ x : α, x_1 x • v x = x
<VAR>f : ℕ → ℂ<VAR>c s : ℂ<GOAL>LSeries (c • f) s = c * LSeries f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>f : E →ᵃ[𝕜] F<VAR>a b : E<VAR>x : F<GOAL>x ∈ ⇑f '' openSegment 𝕜 a b ↔ x ∈ openSegment 𝕜 (f a) (f b)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<GOAL>m.IsCaratheodory ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Tendsto f l (𝓝[>] a)<GOAL>Tendsto (fun i => max a (f i)) l (𝓝[>] a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Tendsto f l (𝓝[>] a)<VAR>h₁ : Tendsto f l (𝓝 a)<VAR>h₂ : ∀ᶠ (i : β) in l, f i ∈ Ioi a<GOAL>Tendsto (fun i => max a (f i)) l (𝓝[>] a)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜' E<VAR>inst✝⁴ : IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜' f x ↔ ∃ g', restrictScalars 𝕜 g' = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜' E<VAR>inst✝⁴ : IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>DifferentiableWithinAt 𝕜' f univ x ↔ ∃ g', restrictScalars 𝕜 g' = fderivWithin 𝕜 f univ x
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>x✝ : Cᵒᵖ<GOAL>(J.plusMap (η ≫ γ)).app x✝ = (J.plusMap η ≫ J.plusMap γ).app x✝
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>x✝ : Cᵒᵖ<VAR>S : (J.Cover (unop x✝))ᵒᵖ<GOAL>colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap (η ≫ γ)).app x✝ = colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap η ≫ J.plusMap γ).app x✝
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>b.flag k.succ = span R {b k} ⊔ b.flag k.castSucc
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<GOAL>span R (⇑b '' {i | i.castSucc < k.succ}) = span R {b k} ⊔ span R (⇑b '' {i | i < k})
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hI : I ⊆ E<VAR>hX : X ⊆ E<GOAL>(uniqueBaseOn I E).Basis J X ↔ J = X ∩ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hI : I ⊆ E<VAR>hX : X ⊆ E<GOAL>J ∈ maximals (fun x x_1 => x ⊆ x_1) {I_1 | (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X} ↔ J = X ∩ I
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>inst✝¹ : HasWeakSheafify J A<VAR>inst✝ : J.WEqualsLocallyBijective A<VAR>P Q : Cᵒᵖ ⥤ A<VAR>φ : P ⟶ Q<GOAL>Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℤ<GOAL>teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x y : MvPolynomial R ℤ<GOAL>(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) = (map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<VAR>x : R<VAR>h : x ∈ Module.annihilator R M<GOAL>x ∈ Module.annihilator R M'
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<VAR>x : R<VAR>h : ∀ (m : M), x • m = 0<GOAL>∀ (m : M'), x • m = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Surjective ⇑f<VAR>x : R<VAR>h : ∀ (m : M), x • m = 0<VAR>m : M<GOAL>x • f m = 0
<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>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict s + μ.restrict sᶜ = μ
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<VAR>h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)<GOAL>‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Monoid M<VAR>inst✝¹ : LinearOrder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f : R →* M<VAR>x y : R<GOAL>f (x - y) = f (y - x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CokernelCofork f<GOAL>s.ι.app zero = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f₀ f₁ : α → β<VAR>g : α → ℝ<VAR>hf₁_m : AEStronglyMeasurable f₁ μ<VAR>hf₀_i : Integrable f₀ μ<VAR>hg_i : Integrable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a<GOAL>∀ᵐ (a : α) ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f₀ f₁ : α → β<VAR>g : α → ℝ<VAR>hf₁_m : AEStronglyMeasurable f₁ μ<VAR>hf₀_i : Integrable f₀ μ<VAR>hg_i : Integrable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a<GOAL>∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f₀ f₁ : α → β<VAR>g : α → ℝ<VAR>hf₁_m : AEStronglyMeasurable f₁ μ<VAR>hf₀_i : Integrable f₀ μ<VAR>hg_i : Integrable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a<VAR>a : α<VAR>ha : ‖f₀ a - f₁ a‖ ≤ g a<GOAL>‖f₁ a‖ ≤ ‖f₀ a‖ + g a
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : x ≡ y [SMOD U]<VAR>n : ℤ<GOAL>n • x ≡ n • y [SMOD U]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y<VAR>n : ℤ<GOAL>Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)
<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>x : E<GOAL>re ⟪x, x⟫_𝕜 = ‖⟪x, 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>x : E<GOAL>re ⟪x, x⟫_𝕜 = ‖↑(re ⟪x, 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>x : E<GOAL>‖↑(re ⟪x, x⟫_𝕜)‖ = re ⟪x, x⟫_𝕜
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f f' : α → E<VAR>s : Set α<VAR>h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0<VAR>p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }<VAR>i : ℕ<GOAL>edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = edist (f' (↑p.2 (i + 1))) (f' (↑p.2 i))
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : Fin 1 → E<GOAL>(iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : Fin 1 → E<GOAL>(fderiv 𝕜 f x) (m (last 0)) = (fderiv 𝕜 f x) (m 0)
<VAR>n p k : ℕ<VAR>hp : Prime p<VAR>hk : k ≠ 0<GOAL>(p ^ k).minFac = p
<VAR>F : Type u → Type u<VAR>q : QPF F<GOAL>LiftpPreservation ↔ IsUniform
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k →+* K<VAR>φ : K →+* ℂ<VAR>hφ : IsReal φ<VAR>x : k<GOAL>(star (φ.comp f)) x = (φ.comp f) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>affineSpan 𝕜 ((convexHull 𝕜) s) = affineSpan 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>affineSpan 𝕜 ((convexHull 𝕜) s) ≤ affineSpan 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<GOAL>(convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>a b : E<GOAL>edist a b = ↑‖a / b‖₊
<VAR>R S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : FormallyUnramified R S<VAR>inst✝ : EssFiniteType R S<VAR>s : S<GOAL>1 ⊗ₜ[R] s * elem R S = s ⊗ₜ[R] 1 * elem R S
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq m<VAR>v : m → α<VAR>x✝ : m<GOAL>(1 *ᵥ v) x✝ = v x✝
<VAR>n : ℕ<VAR>c : Composition n<VAR>i : ℕ<VAR>h : i < c.length<GOAL>(take (i + 1) c.blocks).sum = (take i c.blocks).sum + c.blocks[i]
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h₀ : HasFDerivAt f f₀' x<VAR>h₁ : HasFDerivAt f f₁' x<GOAL>f₀' = f₁'
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h₀ : HasFDerivWithinAt f f₀' univ x<VAR>h₁ : HasFDerivWithinAt f f₁' univ x<GOAL>f₀' = f₁'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>g : α → γ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzOnWith Kf f s<VAR>hg : LipschitzOnWith Kg g s<VAR>x✝ : α<VAR>hx : x✝ ∈ s<VAR>y✝ : α<VAR>hy : y✝ ∈ s<GOAL>edist ((fun x => (f x, g x)) x✝) ((fun x => (f x, g x)) y✝) ≤ ↑(max Kf Kg) * edist x✝ y✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>g : α → γ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzOnWith Kf f s<VAR>hg : LipschitzOnWith Kg g s<VAR>x✝ : α<VAR>hx : x✝ ∈ s<VAR>y✝ : α<VAR>hy : y✝ ∈ s<GOAL>max (edist ((fun x => (f x, g x)) x✝).1 ((fun x => (f x, g x)) y✝).1) (edist ((fun x => (f x, g x)) x✝).2 ((fun x => (f x, g x)) y✝).2) ≤ max (↑Kf * edist x✝ y✝) (↑Kg * edist x✝ y✝)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<GOAL>P a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<GOAL>P a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<VAR>ha0 : ¬a = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>P a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<VAR>ha0 : ¬a = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>P (normalizedFactors a).prod
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<VAR>ha0 : ¬a = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>P_of_associated : ∀ {x y : α}, x ~ᵤ y → P x → P y<VAR>ha0 : ¬a = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ p ∈ normalizedFactors a, Prime p