ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α ↪ β<VAR>hG : G.LocallyLinear<GOAL>(SimpleGraph.map f G).LocallyLinear
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α ↪ β<VAR>hG : G.LocallyLinear<GOAL>∀ ⦃x y : β⦄, (SimpleGraph.map f G).Adj x y → ∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α ↪ β<VAR>hG : G.LocallyLinear<VAR>a b : α<VAR>h : G.Adj a b<GOAL>∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>hG : G.LocallyLinear<VAR>a b : α<VAR>h : G.Adj a b<VAR>s : Finset α<VAR>hs : G.IsNClique 3 s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>∃ s, (SimpleGraph.map f G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>X : (a : α✝) → Part (β a)<VAR>hX : f X ≤ X<GOAL>Part.fix ⇑f ≤ X
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>X : (a : α✝) → Part (β a)<VAR>hX : f X ≤ X<GOAL>ωSup (approxChain f) ≤ X
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>X : (a : α✝) → Part (β a)<VAR>hX : f X ≤ X<GOAL>∀ (i : ℕ), (approxChain f) i ≤ X
<VAR>α✝ : Type u_1<VAR>β : α✝ → Type u_2<VAR>α : Type u_3<VAR>f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)<VAR>X : (a : α✝) → Part (β a)<VAR>hX : f X ≤ X<GOAL>∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ X
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ comap f I<VAR>x : R<GOAL>((quotientMap I f H).comp (Quotient.mk J)) x = ((Quotient.mk I).comp f) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T S : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>hS : S.IsPositive<GOAL>(T + S).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T S : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>hS : S.IsPositive<VAR>x : E<GOAL>0 ≤ (T + S).reApplyInnerSelf x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T S : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>hS : S.IsPositive<VAR>x : E<GOAL>0 ≤ re ⟪T x, x⟫_𝕜 + re ⟪S x, x⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>n : ℕ<GOAL>‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>n : ℕ<GOAL>‖if Even n then 0 else 1‖ ≤ 1
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>a : M<VAR>b : ↥S<VAR>a' : M<VAR>b' : ↥S<VAR>eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')<GOAL>LocalizedModule.mk a b = LocalizedModule.mk a' b'
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>a : M<VAR>b : ↥S<VAR>a' : M<VAR>b' : ↥S<VAR>eq1 : ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')<GOAL>LocalizedModule.mk a b = LocalizedModule.mk a' b'
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>a : M<VAR>b : ↥S<VAR>a' : M<VAR>b' : ↥S<VAR>eq1 : ↑b • f a' = ↑b' • f a<GOAL>LocalizedModule.mk a b = LocalizedModule.mk a' b'
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s✝ : Set E<VAR>a b m✝ : ℝ<VAR>x y : E<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>m n : ℝ<GOAL>StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>v : V<GOAL>v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i✝ : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i✝)<VAR>h : Baer R Q<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>i : X →ₗ[R] Y<VAR>hi : Function.Injective ⇑i<VAR>f : X →ₗ[R] Q<GOAL>∃ h, ∀ (x : X), h (i x) = f x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i✝ : M →ₗ[R] N<VAR>f✝ : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i✝)<VAR>h✝ : Baer R Q<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>i : X →ₗ[R] Y<VAR>hi : Function.Injective ⇑i<VAR>f : X →ₗ[R] Q<VAR>h : Y →ₗ[R] Q<VAR>H : h ∘ₗ i = f<GOAL>∃ h, ∀ (x : X), h (i x) = f x
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>ι : Type u_2<VAR>inst✝² : DecidableEq ι<VAR>M : ι → Type u_3<VAR>inst✝¹ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝ : (i : ι) → Module R (M i)<VAR>C : (⨁ (i : ι), M i) → Prop<VAR>x : ⨁ (i : ι), M i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : M i), C ((lof R ι M i) x)<VAR>H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)<GOAL>C x
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, Measurable (f i)<GOAL>Measurable fun a => ∏ i ∈ s, f i a
<VAR>n : ℕ<GOAL>image Prod.snd n.divisorsAntidiagonal = n.divisors
<VAR>n : ℕ<GOAL>image (Prod.snd ∘ ⇑(Equiv.prodComm ℕ ℕ).toEmbedding) n.divisorsAntidiagonal = n.divisors
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N✝ N₂ : LieSubmodule R L M<VAR>N'✝ : LieSubmodule R L M'<VAR>hf : Function.Injective ⇑f<VAR>N N' : LieSubmodule R L M<VAR>h : map f N = map f N'<GOAL>⇑f '' ↑N = ⇑f '' ↑N'
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t < 0<GOAL>s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x p₁ p₂ : P<VAR>hx : x ∉ s<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>t : R<VAR>ht : t < 0<VAR>h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))<GOAL>seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))<GOAL>seminormFromConst' hf1 hc hpm (c * x) = f c * seminormFromConst' hf1 hc hpm x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))<GOAL>Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hlim : Tendsto (fun n => seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x))<VAR>hterm : seminormFromConst_seq c f (c * x) = fun n => f c * seminormFromConst_seq c f x (n + 1)<GOAL>Tendsto (seminormFromConst_seq c f (c * x)) atTop (𝓝 (f c * seminormFromConst' hf1 hc hpm x))
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<GOAL>(convexHull R) s = {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<GOAL>s ⊆ {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<GOAL>Convex R {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<GOAL>{x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x} ⊆ (convexHull R) s
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Iic b) = ↑b + 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α →ₛ F<GOAL>integral μ f = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>a : α<VAR>h : IsLUB (Set.range ⇑c) a<GOAL>a = ωSup c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>a : α<VAR>h : IsLUB (Set.range ⇑c) a<GOAL>a ≤ ωSup c ∧ ωSup c ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>c : Chain α<VAR>a : α<VAR>h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1<GOAL>a ≤ ωSup c ∧ ωSup c ≤ a
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x y : K<VAR>h : x * (algebraMap A K) ↑(den A y) = (algebraMap A K) (num A y)<GOAL>x = y
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x y : K<VAR>h : x = y<GOAL>x = mk' K (num A y) (den A y)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : CommSemiring 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>n : ℕ<VAR>f : M →ₗ[R] M₂ →ₗ[R] M₃<VAR>g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃<VAR>x y : M<VAR>z : M₂<GOAL>((fun m => (f m).vecCons (g m)) (x + y)) z = ((fun m => (f m).vecCons (g m)) x + (fun m => (f m).vecCons (g m)) y) z
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : CommSemiring 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>n : ℕ<VAR>f : M →ₗ[R] M₂ →ₗ[R] M₃<VAR>g : M →ₗ[R] M₂ →ₗ[R] Fin n → M₃<VAR>r : R<VAR>x : M<VAR>z : M₂<GOAL>({ toFun := fun m => (f m).vecCons (g m), map_add' := ⋯ }.toFun (r • x)) z = ((RingHom.id R) r • { toFun := fun m => (f m).vecCons (g m), map_add' := ⋯ }.toFun x) z
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<GOAL>∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Subsingleton B<GOAL>∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<GOAL>∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<GOAL>b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<VAR>H : ∑ i : Fin pb.dim, (pb.basis.repr b) i • pb.basis i = b<GOAL>b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<VAR>H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b<GOAL>b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<VAR>H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b<GOAL>Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩)) + Submodule.Quotient.mk 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<VAR>H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b<GOAL>Submodule.Quotient.mk ((pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x) = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩)) + Submodule.Quotient.mk 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis A B<VAR>b : B<VAR>h✝ : Nontrivial B<VAR>H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b<GOAL>Submodule.Quotient.mk ((pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩) + Submodule.Quotient.mk (∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x) = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩)) + Submodule.Quotient.mk 0
<VAR>ι : Type u_1<VAR>κ✝ : Type u_2<VAR>α : Type u_3<VAR>inst✝⁷ : OrderedCommMonoid α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderClosedTopology α<VAR>f✝ g : ι → α<VAR>a a₁ a₂ : α<VAR>κ : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁴ : OrderedCommGroup γ<VAR>inst✝³ : UniformSpace γ<VAR>inst✝² : UniformGroup γ<VAR>inst✝¹ : OrderClosedTopology γ<VAR>inst✝ : CompleteSpace γ<VAR>f : κ → γ<VAR>β : Set κ<VAR>h : ∀ (a : κ), 1 ≤ f a<VAR>hf : Multipliable f<GOAL>∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a
<VAR>ι : Type u_1<VAR>κ✝ : Type u_2<VAR>α : Type u_3<VAR>inst✝⁷ : OrderedCommMonoid α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderClosedTopology α<VAR>f✝ g : ι → α<VAR>a a₁ a₂ : α<VAR>κ : Type u_4<VAR>γ : Type u_5<VAR>inst✝⁴ : OrderedCommGroup γ<VAR>inst✝³ : UniformSpace γ<VAR>inst✝² : UniformGroup γ<VAR>inst✝¹ : OrderClosedTopology γ<VAR>inst✝ : CompleteSpace γ<VAR>f : κ → γ<VAR>β : Set κ<VAR>h : ∀ (a : κ), 1 ≤ f a<VAR>hf : Multipliable f<GOAL>Multipliable fun a => f a
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>denom (x * y) z = (↑(↑↑x 1 0) * (num y z / denom y z) + ↑(↑↑x 1 1)) * denom y z
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>denom (x * y) z = ↑(↑↑x 1 0) * num y z + ↑(↑↑x 1 1) * denom y z
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(↑(↑↑x 1 0) * ↑(↑↑y 0 0) + ↑(↑↑x 1 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 1 0) * ↑(↑↑y 0 1) + ↑(↑↑x 1 1) * ↑(↑↑y 1 1)) = ↑(↑↑x 1 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 1 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))
<VAR>s m n step : Nat<GOAL>range' s (m + 1) step ++ range' (s + step * (m + 1)) n step = range' s (n + (m + 1)) step
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<GOAL>closure ((fun g => ⟨g * (↑(toFun hR g))⁻¹, ⋯⟩) '' (R * S)) = ⊤
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>R S : Set G<VAR>hR : R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure S = ⊤<GOAL>map H.subtype ⊤ ≤ closure ((fun x => H.subtype ⟨x * (↑(toFun hR x))⁻¹, ⋯⟩) '' (R * S))