ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>a b : α<VAR>h : s ∈ 𝓝 b<GOAL>s * {a} ∈ 𝓝 (b * a)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>a b : α<VAR>h : s ∈ 𝓝 b<GOAL>op a • s ∈ 𝓝 (b * a)
<VAR>Δ : SimplexCategory<VAR>f : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)<GOAL>({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (𝟙 Δ)) f = (𝟙 ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)) f
<VAR>Δ : SimplexCategory<VAR>f : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)<GOAL>↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (𝟙 Δ)) f) = ↑((𝟙 ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)) f)
<VAR>Δ : SimplexCategory<VAR>f : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)<VAR>i : (forget SimplexCategory).obj Δ<GOAL>↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (𝟙 Δ)) f) i = ↑((𝟙 ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)) f) i
<VAR>Δ : SimplexCategory<VAR>f : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)<VAR>i : (forget SimplexCategory).obj Δ<GOAL>∑ j ∈ Finset.filter (fun x => x = i) Finset.univ, ↑f j = ↑((𝟙 ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj Δ)) f) i
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<GOAL>({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (f ≫ g)) h = ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map f ≫ { obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map g) h
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<GOAL>↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (f ≫ g)) h) = ↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map f ≫ { obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map g) h)
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<VAR>i : (forget SimplexCategory).obj Z✝<GOAL>↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map (f ≫ g)) h) i = ↑(({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map f ≫ { obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.map g) h) i
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<VAR>i : (forget SimplexCategory).obj Z✝<GOAL>∑ j ∈ Finset.filter (fun x => (f ≫ g) x = i) Finset.univ, ↑h j = ↑(({ toFun := toTopMap f, continuous_toFun := ⋯ } ≫ { toFun := toTopMap g, continuous_toFun := ⋯ }) h) i
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<VAR>i : (forget SimplexCategory).obj Z✝<GOAL>∑ x ∈ Finset.filter (fun x => g (f x) = i) Finset.univ, ↑h x = ∑ x ∈ Finset.filter (fun x => g x = i) Finset.univ, ∑ x ∈ Finset.filter (fun x_1 => f x_1 = x) Finset.univ, ↑h x
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<VAR>i : (forget SimplexCategory).obj Z✝<GOAL>∑ x ∈ Finset.filter (fun x => g (f x) = i) Finset.univ, ↑h x = ∑ x ∈ (Finset.filter (fun x => g x = i) Finset.univ).biUnion fun x => Finset.filter (fun x_1 => f x_1 = x) Finset.univ, ↑h x
<VAR>X✝ Y✝ Z✝ : SimplexCategory<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>h : (forget TopCat).obj ({ obj := fun x => TopCat.of ↑x.toTopObj, map := fun {X Y} f => { toFun := toTopMap f, continuous_toFun := ⋯ } }.obj X✝)<VAR>i : (forget SimplexCategory).obj Z✝<GOAL>(↑(Finset.filter (fun x => g x = i) Finset.univ)).PairwiseDisjoint fun x => Finset.filter (fun x_1 => f x_1 = x) Finset.univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>(∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.RightFraction X Y<GOAL>φ.map L ⋯ = ψ.map L ⋯ ↔ RightFractionRel φ ψ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ ψ : W.RightFraction X Y<GOAL>φ.map L ⋯ = ψ.map L ⋯ ↔ (φ.map L ⋯).op = (ψ.map L ⋯).op
<VAR>ξ : ℚ<VAR>f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)<VAR>s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}<GOAL>s.Finite
<VAR>ξ : ℚ<VAR>f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)<VAR>s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}<VAR>hinj : Function.Injective f<GOAL>s.Finite
<VAR>ξ : ℚ<VAR>f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)<VAR>s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}<VAR>hinj : Function.Injective f<VAR>H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}<GOAL>s.Finite
<VAR>ξ : ℚ<VAR>f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)<VAR>s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}<VAR>hinj : Function.Injective f<VAR>H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}<GOAL>(⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}).Finite
<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<VAR>x✝ : S<VAR>n : ℕ<VAR>x : R<GOAL>eval₂ C X ((monomial n) x) = (monomial n) x
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>‖↑z‖ = ‖z‖
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I : Ideal R<VAR>hI : I.IsMaximal<VAR>this : Field (R ⧸ I) := Quotient.field I<GOAL>⊥.IsMaximal
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 n f s ↔ (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x : WithLp 2 (α × β)<GOAL>‖x‖ = √(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<VAR>s : Set α<GOAL>IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ x ∈ s, r x a) → r b a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>ContinuousAt (gauge s) 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs : s ∈ 𝓝 0<GOAL>Tendsto (gauge s) (𝓝 0) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>(sesqFormOfInner (↑A x)) y = (sesqFormOfInner x) (↑(adjoint A) y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>Us : Set (Opens α)<VAR>x : α<GOAL>x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ZMod N<GOAL>↑(toCircle j) = cexp (2 * ↑π * I * ↑j.val / ↑N)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<VAR>y : ↥S<VAR>z : N<GOAL>f.mk' x y = z ↔ f.toMap x = z * f.toMap ↑y
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ : V<VAR>inst✝ : DecidableEq V<VAR>u v w : V<VAR>p : G.Walk v w<VAR>hc : p.IsTrail<VAR>h : u ∈ p.support<GOAL>(?m.20281.append (p.dropUntil u h)).IsTrail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t✝ : Finset α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a✝ : α<GOAL>a✝ ∈ filter p s ∩ t ↔ a✝ ∈ filter p (s ∩ t)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>hp : 1 ≤ 1<GOAL>(∑ i ∈ s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i ∈ s, f i ^ 1) ^ (1 / 1) + (∑ i ∈ s, g i ^ 1) ^ (1 / 1)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>this : IsGreatest ((fun g_1 => ∑ i ∈ s, (f + g) i * g_1 i) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}) ((∑ i ∈ s, (f + g) i ^ p) ^ (1 / p))<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>this : IsGreatest ((fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}) ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>this : IsGreatest ((fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}) ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))<VAR>φ : ι → ℝ≥0<VAR>hφ : φ ∈ {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}<VAR>H : (fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ = (∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p)<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>hpq : p.IsConjExponent p.conjExponent<VAR>this : IsGreatest ((fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}) ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))<VAR>φ : ι → ℝ≥0<VAR>hφ : φ ∈ {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}<VAR>H : (fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ = (∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p)<GOAL>(fun a => ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m✝ m : (i : ι) → OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<GOAL>(OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m✝ m : (i : ι) → OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<VAR>h : univ.pi s = ∅<GOAL>(OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m✝ m : (i : ι) → OuterMeasure (α i)<VAR>s : (i : ι) → Set (α i)<VAR>h : (univ.pi s).Nonempty<GOAL>(OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>i : M<VAR>hi : i ∉ Finset.image (⇑(weight w)) φ.support<GOAL>(weightedHomogeneousComponent w i) φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>i : M<VAR>hi : i ∉ Finset.image (⇑(weight w)) φ.support<GOAL>∀ d ∈ φ.support, (weight w) d ≠ i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>i : M<VAR>hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w) x = i<GOAL>∀ d ∈ φ.support, (weight w) d ≠ i
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x y : X<VAR>hm : IsMaximal x (x ⊔ y)<GOAL>Iso (x, x ⊔ y) (x ⊓ y, y)
<VAR>α✝ α : Type u<VAR>inst✝ : OrderedCommGroup α<VAR>a b c : α<VAR>bc : a * b ≤ a * c<GOAL>b ≤ c
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f.Monic<VAR>hf' : optParam (f ≠ 0) ⋯<GOAL>minpoly K (powerBasis hf').gen = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (map g g') = range (lTensor N f') ⊔ range (rTensor N' f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (lTensor P g' ∘ₗ rTensor N' g) = range (lTensor N f') ⊔ range (rTensor N' f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ range (rTensor N' f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>Submodule.comap (rTensor N' g) (ker (lTensor P g')) = range (lTensor N f') ⊔ ker (rTensor N' g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>Submodule.comap (rTensor N' g) (ker (lTensor P g')) = Submodule.comap (rTensor N' g) (Submodule.map (rTensor N' g) (range (lTensor N f')))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (lTensor P g') = Submodule.map (rTensor N' g) (range (lTensor N f'))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (lTensor P g') = range (map g f')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (lTensor P g') = Submodule.map (lTensor P f') (range (rTensor M' g))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>ker (lTensor P g') = range (lTensor P f')
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>((fun a => l.set n (f a)) <$> some (l.get ⟨n, h⟩)).getD l = l.set n (f (l.get ⟨n, h⟩))
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂